Can unprovability unprovable? Is there an $\omega$-fold unprovability?
Provability Logic
It might be much clearer to rewrite all this about "provability" in the provability logic where "$P$ is provable" is denoted by "$□ P$", where "$□$" is a modal operator. Then given any first-order theory $T$ that is strong enough to perform string manipulation or equivalent (such as PA with some suitable encoding) and has decidable proof validity, $T$ will satisfy the Hilbert-Bernays provability conditions as well as the modal fixed-point theorem: $\def\imp{\rightarrow}$ $\def\eq{\leftrightarrow}$ $\def\nn{\mathbb{N}}$ $\def\pa{\mathrm{PA}}$ $\def\zf{\mathrm{ZF}}$
(D1) If $T \vdash P$ then $T \vdash □ P$, for any sentence $P$ over $T$.
(D3) $T \vdash □ P \imp □ □ P$, for any sentence $P$ over $T$.
(D2) $T \vdash □ P \land □ ( P \imp Q ) \imp □ Q$, for any sentences $P,Q$ over $T$.
(F) Given any $1$-propositional-parameter sentence $P$ over $T$ such that every occurrence of the parameter in $P$ is bound by some $□$, there is a sentence $Q$ over $T$ so that $T \vdash Q \eq P(Q)$.
Lob's theorem and Godel's second incompleteness theorem
Now note that using these you can prove Lob's theorem in both external and internal form for any sentence $P$ over $T$:
(L*) If $T \vdash □ P \imp P$ then $T \vdash P$.
(L) $T \vdash □ ( □ P \imp P ) \imp □ P$.
Proof: See the Wikipedia article.
From these applied to $P = \bot$ we immediately get Godel's second incompleteness theorem (in both external and internal form):
(GI*) If $T$ is consistent then $T \nvdash \neg □ \bot$.
(GI) $T \vdash \neg □ \bot \imp \neg □ \neg □ \bot$.
Two theorems about internal unprovability
We also get the following two theorems.
(U*) If $T$ is consistent, then $T \nvdash \neg □ P$ for every sentence $P$ over $T$.
Proof: Take any sentence $P$ over $T$. Then $T \vdash □ ( \bot \imp P )$ by (D1), and hence $T \vdash □ \bot \imp □ P$ by (D2). If $T \vdash \neg □ P$ then $T \vdash \neg □ \bot$, contradicting (GI*). Therefore $T \nvdash \neg □ P$.
(U) $T \vdash \neg □ \bot \imp \neg □ \neg □ P$ for every sentence $P$ over $T$.
Proof: $T \vdash \neg □ P \imp \neg □ \bot$ as shown above, and hence $T \vdash □ ( \neg □ P \imp \neg □ \bot )$ by (D1). Thus $T \vdash □ \neg □ P \imp □ \neg □ \bot$ by (D2). Also $T \vdash □ \neg □ \bot \imp □ \bot$ by (GI). Therefore by combining we get $T \vdash \neg □ \bot \imp \neg □ \neg □ P$. Note that from this we also get $T \vdash \neg □ P \imp \neg □ \neg □ P$.
Remarks
The first theorem shows that $T$ is unable to prove within itself that any sentence is unprovable over $T$, unless $T$ is inconsistent in which case of course $T$ proves and disproves everything. The second theorem shows that $T$ itself 'knows' that if itself is consistent (or that there is some unprovable sentence) then it cannot prove any sentence unprovable over itself! This answers your question if you are referring to internal unprovability.
Explicit example of unprovably independent sentence
The above is done within $T$, but if we go outside we can say even more, namely that we can actually show an explicit example of an unprovably independent sentence when we are in the meta-system and studying $T$. Note that this does not contradict the fact that $T$ does not know any such sentence, basically because $T$ 'knows less than' the meta-system; all reasonable meta-systems 'know' the collection of sentences that $T$ does not prove, but $T$ does not.
Given any sentence $P$ over $T$, although $T$ always proves $P \lor \neg P$, it may not prove $□ P \lor □ \neg P$, nor can it always prove $□ P \lor □ \neg P \lor □ \neg ( □ P \lor □ \neg P )$, because there is the distinct possibility that $\neg □ \neg ( □ P \lor □ \neg P )$. To see why, notice the following. (In our meta-system where we assume the existence and properties of $\nn$. Also, let "$□$" denote provability over $\pa$ if not specified.)
$\nn \nvDash □ □ \bot$ otherwise we can extract a proof of $□ \bot$ over $\pa$ and then a proof of $\bot$, which contradicts consistency of $\pa$.
$\nn \nvDash □ \neg □ \bot$ otherwise we can extract a proof of $\neg □ \bot$ over $\pa$, which contradicts Godel's incompleteness theorem.
$\nn \nvDash □ \neg ( □ □ \bot \lor □ \neg □ \bot )$ otherwise we can obtain a proof of $\neg □ □ \bot$ over $\pa$ which gives a proof of $\neg □ \bot$, again contradicting Godel's theorem.
Therefore $\nn \nvDash □ C \lor □ \neg C \lor □ \neg ( □ C \lor □ \neg C )$ where $C = □ \bot$, and hence $\pa$ cannot prove it because $\nn \vDash PA$. Similarly if $C = \neg □ \bot$, which is true in $\nn$.
Also $\nn \vDash \neg □ \neg ( □ C \lor □ \neg C )$, but (by U* and our assumption that $\nn$ satisfies $\pa$) $\pa$ cannot prove it!
This shows that there is a sentence $C$ that is true in $\nn$ but that $\pa$ does not prove "$C$ is provable or $(\neg C)$ is provable or that ( $C$ is independent ) is provable or that ( $C$ is independent ) is unprovable". Any such $C$ is of course unprovable in $\pa$ (by D1).
Therefore this is a strong positive answer to your question if you are asking for a sentence that is externally true and independent but internally unprovably independent.
Further remarks
Let us fix $\zf$ as our meta-system. We shall from now on use "$□_T$" to denote provability over $T$, since it differs from $T$ to $T$.
By (GI) we know that:
$\pa \nvdash \neg □_\pa \bot$.
$\zf \nvdash \neg □_\zf \bot$.
But by the very axiomatization of $\zf$ we also have:
- $\zf \vdash \neg □_\pa \bot$.
There is no contradiction here, because $\zf$ is strictly stronger than $\pa$, since it was made to assume the existence of a model of $\pa$, but it shows that we need to state precisely what we are talking about provability over.
Furthermore, $\pa$ can reason a bit about proofs over $\zf$, since proofs are just strings, so we have:
- $\pa \nvdash \neg □_\zf \bot$, since $\pa \vdash □_\pa \bot \imp □_\zf \bot$.
It has been pointed out in the comments that there is a major flaw in this answer, as it was intended to outline a proof in less than formal terms, but in doing so missed a point of significant importance. Though the work below follows from the four axioms I posit below, there is no evident way to formalize a notion of provability that satisfies the axioms below. This should trouble us, because having "provability" just be a word not corresponding to any formal notion is problematic.
The comments contain further discussion and this answer contains a formal treatment of the question.
First, let's examine what it would mean for a problem to be 2-fold unprovable. By your notation, call a problem n-fold unprovable if there is no proof that the problem is (n-1)-fold unprovable or not (where 0-fold unprovable is taken to mean "provable"). Here, a statement which is 1-fold unprovable is one which is independent of a system.
We take "provable" to mean "there is a proof or disproof of $P$".
(A) If $P$ is provable then "$P$ is provable" is provable.
This seems clear, since, knowing that a proof of $P$ exists, we can certainly find it by enumerating all the proofs (if the axioms are recursively enumerable), and thus prove that $P$ is provable.
(B) $P$ is provable if and only if $\neg P$ is provable.
Clearly, if a proof or disproof of $P$ exists, we can easily disprove or prove $\neg P$.
(C) If $P$ is provable and $P\rightarrow Q$ is provable, then $Q$ is provable.
Which is clear, given how proofs are constructed. We also need
(D) If $P$ is provably true, then $P$ is true.
From here, we can argue:
- If $P$ is provable, then "$P$ is provable" is provable (from (A)).
- If "$P$ is provable" is unprovable, then $P$ is unprovable (contrapositive of (1)).
- If "$P$ is unprovable" is unprovable, then "$P$ is provable" is unprovable (from (B)).
- If "$P$ is unprovable" is unprovable, then $P$ is unprovable (syllogism of (3) and (2))
Which is clearly a problem, since we can quickly reach a contradiction if we take
- ""$P$ is unprovable" is unprovable" is provably true.
- "$P$ is unprovable" is unprovable. (from (D))
- "$P$ is unprovable" is provable (from 5, 4, and (C), noting that 4 is provable since we just proved it).
- "$P$ is unprovable" is provable and "$P$ is unprovable" is unprovable (6 and 7)
A contradiction. As we accept A, B, and C, it must be that the given (5) implies a contradiction and is thus false, meaning that one can never prove that $P$ is 2-fold unprovable - thus if a statement is 2-fold unprovable, it is also 3-fold unprovable, since no proof that it is 2-fold unprovable could exist. Indeed, every higher ordinal befalls the same argument.
So, we might consider that there are potentially 4 classes of statements:
- Those with a proof
- Those with a disproof
- Those that can be proved to have neither proof nor disproof.
- Those of which nothing can be said. (i.e. 2-fold unprovable ones, but nothing can be said, because any proof that a statement belongs to this class is inconsistent by above argument)
The problem is that we can never actually choose an example of a statement in some formal system and show, using that same system, that a statement is in the last class. Using a similar statement to Godel - though not providing any construction thereof, and assuming that a similar construction to Godel's would suffice - one might question that statement
This statement is unprovable or false.
It could not be proven false (as it is true if there is a proof that it is false), nor proven true (as it asserts no such proof exists), nor proven independent (as that would prove the statement as well), nor proven 2-fold independent (as such a proof would show it to be independent). This is paradoxical, but demonstrates that there must be some statements which cannot be demonstrated to be in any class - implying that there are 2-fold unprovable statements.
A more concrete, but perhaps less satisfying, proof that statements of the fourth class exist if we consider turing machines. Consider that, if a turing machine halts, we can prove that it halts - we just run it and, at the end, observe that it halted. The converse is that, if there is no proof of whether turing machine halts, then it must not halt - meaning that, similarly to before, if there is a proof that there is no proof that a turing machine halts, we can prove that the machine does not halt. Thus, one can never prove that "T halts" is unprovable*.
Now, if we assume that the theory we are talking about satisfies the constraints of Godel's theorem. The constraints can be expressed as "The axiomatic system can simulate Turing machines and Turing machines can enumerate the axioms". So, that means, for any machine $T$, we could create a machine which enumerates every theorem of a system and looks for a proof of "$T$ halts" or "$T$ doesn't halt" - and, if our system always proves "true" or "false" (since, "undecidable" was ruled out in the previous paragraph), it would be guaranteed to eventually find one. This would implies the halting problem is decidable. It is not. Ergo, some statements cannot be proven to be true, false, or undecidable.
These proofs work intuitively; there are formal systems that defy them (for instance, every statement in the theory of true arithmetic is either true or false - but it has infinitely many axioms). This is hard to avoid since "unprovability" is, of course, relative to a given formal system, and it is possible "P is unprovable is unprovable in system A" is a theorem of a different system B. However, any system that satisfies the conditions of Godel's proof will, in itself, have 2-fold unprovable statements, and these statements will also be 3-fold unprovable and so on.
* Other statements, like the Goldbach conjecture, would work similarly: If they are false, there would be a counterexample, and we could use this to disprove the conjecture. This does, paradoxically, mean that if no proof or disproof of it exists in a system which models it, then it is true. However, this does not mean that it must be possible to prove or disprove it - it could be unprovable. It's just that we could never prove that it is unprovable within that same system, because that's equivalent to showing no counterexamples. Indeed, if it is unprovable, then it is 2-fold unprovable, 3-fold unprovable and so on- absolutely nothing might be said of it.
[This is not an answer to the question. It was supposed to be a response to a comment by Milo under his answer, but since it is too long and may be interesting to others, I'm putting it here.]
Different Provability Notions
Milo suggested that perhaps we can consider a different kind of "provable" than the usual one, in the hope that there might be one that satisfies all the properties he would like to have, namely (A) to (D) in his post. I commented that I think there cannot be any such notion, but here is an analysis of the suggested kind where "unprovable" includes some notion of consistency. I'll freely use what I have defined and proven in my other answer.
Let's reserve "provable" for the standard notion. We shall work in a fixed theory $T$ that is strong enough to interpret arithmetic. Let "$! P$" denote "$□ P \lor □ \neg P$" ($P$ is internally either provable or disprovable), and "$? P$" denote "$\neg □ \bot → \neg □ P \land \neg □ \neg P$" (if there is internal consistency then $P$ is internally independent), which is equivalent to "$□ P \lor □ \neg P → □ \bot$". Then these are actually useful. For example $PA \vdash{} ? R$ where $R$ is the Rosser sentence (over $PA$), by formalizing the entire Rosser trick in PA itself. I also think that $ZF \vdash{} ? AC$ (based on https://math.stackexchange.com/a/1596529), which would be a highly non-trivial example. Furthermore we always have $! P \lor{} ? P$.
Now let us see what (A) to (D) would, should or cannot be. It turns out that only (A) and (B) have some sort of true interpretation, but even then they aren't exactly very useful.
(A) should be "$! P →{} ! ! P$", which is true because $□ P → □ □ P$ and $□ \neg P → □ □ \neg P$ by (D3), and $□ □ P →{} □ ! P$ and $□ □ \neg P →{} □ ! P$ by (D1,D2).
(B) should be "$! P ↔{} ! \neg P$", which is obviously true.
(C) would be "$! P \land{} ! ( P → Q ) →{} ! Q$", which is invalid when $(P,Q) = (\bot,\neg □ \bot)$, since PA would prove $□ \neg P$ and $□ ( P → Q )$ but not $! Q$. (C) should have been (D2).
(D) says "$□ P → P$", which is even more invalid than "$□ □ P → □ P$". Even if we change it to (D*) "$\neg □ \bot \land □ P → P$", it is still invalid. To see why, (D*) gives $\neg □ \bot \land □ □ \bot → □ \bot$ and hence $□ □ \bot → □ \bot$, so by (L*) we get $□\bot$, which is about as false as it can get.
Some Correct Claims
Although Milo's arguments are flawed, there are a number of related claims that are in fact correct for any sentence $P$ over $T$:
(1) If $T$ is consistent, then $T \nvdash \neg □ P$.
Same as (U*).
(2) If $T$ is arithmetically sound or ω-consistent, then $T \nvdash □ \neg □ P$.
Proof: If $T \vdash □ \neg □ P$, then $T \vdash □ \bot$ by (U), and since $T$ is arithmetically sound or ω-consistent we can extract a proof of $\bot$ over $T$, which is impossible. Therefore $T \nvdash □ \neg □ P$.
(3) $T \vdash \neg □ \bot → \neg □ \neg □ P$.
Same as (U).
Internal Independence
Can any more can be said about internal independence, which we have denoted by "$?$", in similar manner as with "$□$"? I don't know; there does not seem to be any simple but non-trivial fact involving it, and I don't expect any either.