I was just thinking about unprovability. I just wanted to know if it is possible to make a concrete boundary between provable problems and unprovable problems in a certain axiomatic system.

We know that there is a statement that is true yet unprovable. Then is it possible that a statement is true and unprovable, but the unprovability is unprovable?

We can extend it to a question of "unprovability of unprovability of unprovability", or any finite number of times, or even $\omega$ times....

I have no clue. Has there been any research on this kind of topic?

  • 1
    $\begingroup$ I read somewhere that Goedel proved that there are unprovable statement, and Turing proved that the only way to know if a statement is provable or not is to prove / disprove it. So i Think that no, if a statement is unprovable then you won't be able to show that it actually is. $\endgroup$
    – Surb
    Sep 15 '14 at 13:21
  • 1
    $\begingroup$ Possible duplicate of math.stackexchange.com/questions/17212/… ? $\endgroup$ Sep 25 '14 at 22:42
  • $\begingroup$ Please note that while the 'axioms' of "provability" in Milo's answer look highly desirable, it is in fact impossible for them to simultaneously hold for any formal system that can interpret arithmetic (can express and prove all the arithmetical statements that PA can, suitably translated). This shows that there is no way to carry out Milo's arguments unless the formal system is so weak as to be unable to handle arithmetic, which may be rather disappointing. But that is just how it is. $\endgroup$
    – user21820
    May 4 '16 at 2:28
  • $\begingroup$ Note also that there are self-verifying theories (due to Willard) that have subtraction and division instead of multiplication, which not only allows it to prove its own consistency (as internally stated), but also retains some simpler arithmetic facts that PA can prove. $\endgroup$
    – user21820
    May 4 '16 at 2:32

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$.


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.)

  1. $\nn \nvDash □ □ \bot$ otherwise we can extract a proof of $□ \bot$ over $\pa$ and then a proof of $\bot$, which contradicts consistency of $\pa$.

  2. $\nn \nvDash □ \neg □ \bot$ otherwise we can extract a proof of $\neg □ \bot$ over $\pa$, which contradicts Godel's incompleteness theorem.

  3. $\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.

  4. 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$.

  5. 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:

  1. $\pa \nvdash \neg □_\pa \bot$.

  2. $\zf \nvdash \neg □_\zf \bot$.

But by the very axiomatization of $\zf$ we also have:

  1. $\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:

  1. $\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:

  1. If $P$ is provable, then "$P$ is provable" is provable (from (A)).
  2. If "$P$ is provable" is unprovable, then $P$ is unprovable (contrapositive of (1)).
  3. If "$P$ is unprovable" is unprovable, then "$P$ is provable" is unprovable (from (B)).
  4. 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

  1. ""$P$ is unprovable" is unprovable" is provably true.
  2. "$P$ is unprovable" is unprovable. (from (D))
  3. "$P$ is unprovable" is provable (from 5, 4, and (C), noting that 4 is provable since we just proved it).
  4. "$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.

  • 1
    $\begingroup$ Thank you for your answer. Actually, I like your argument, but I'm quite confused. It seems valid, but I'm not sure if there's no logical hole. $\endgroup$
    – Henry
    Sep 25 '14 at 10:44
  • $\begingroup$ I made an edit to add a more formal thing at the end; do you think the proof I give that 2-fold unprovability implies 3-fold is questionable? So long as the system is "self-aware" in that it can take a proof or disproof of P and demonstrate that P is provable, I see no room for doubt there (and certainly, that this holds is much weaker than what Godel assumes). I expanded the second section; it now seems clear that the claims I make have the same requirements as Godel's theorem, which, more or less, addresses any system of logic in general use. $\endgroup$ Sep 25 '14 at 22:25
  • $\begingroup$ I don't understand why if there is a proof of 2-fold unprovability, it means existence of a proof of unprovability. As I understood, similar argument still applies to unprovable case (if S is a statement that can be disproved by a counter-example, existence of unprovability proof means no counter-example, so this is a proof of S???) This is weird. I think according to the argument, we can see if something is true, but that doesn't necessarily mean there is a "proof". $\endgroup$
    – Henry
    Sep 26 '14 at 12:09
  • $\begingroup$ I turned the argument at the start into as rigid a proof as can be done without delving into the particulars of axiomatic systems - but if you accept premises A, B, and C, the result does follow. It's true that you can't show a statement to be unprovable if an easily verified counterexample would exist - but just because you can't show that it's unprovable doesn't mean that it's provable. It's possible that we can't see whether something is true, unprovable, false, or anything. $\endgroup$ Sep 26 '14 at 17:19
  • 1
    $\begingroup$ @user21820 I appreciate your answer and see the flaw in mine; I am thinking about how to remedy this, given that my answer was not intended to be so formal, but seems to have overlooked something serious. Do you know if the claim in my answer, that no statement can be proven (in a given system) to be unprovably unprovable (with regards to the same system) is even true? $\endgroup$ May 2 '16 at 3:32

[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.

  • 1
    $\begingroup$ You write "(2) If $T$ is arithmetically sound or $\omega$-consistent, ..." but why not just say "If $T$ is $\Sigma_1^0$ sound, ..."? $\endgroup$ May 29 '16 at 12:12
  • $\begingroup$ @ThomasKlimpel: Well indeed (first-order) $Σ_1$-soundness will do, since either of arithmetical soundness or $ω$-consistency is enough to guarantee $Σ_1$-soundness. But when I wrote my post I was thinking that we expect a meaningful system to be sound for all arithmetical formulae. Alternatively we might want $ω$-consistency in the sense that every provable existential arithmetical sentence has a standard natural number witness. Since both are incompatible, I mentioned either as being sufficient. $\endgroup$
    – user21820
    May 29 '16 at 14:57
  • $\begingroup$ My above comment had a typo; it should have said "incomparable"... $\endgroup$
    – user21820
    Jul 28 '16 at 5:57

"Provability" is always relative to some axiomatic system $T$ and the answer to your question can be either trivial or very complicated depending on which system are you considering for the proof of the unprovability. Let's see how.

In what follows I am assuming that (1) you want to consider a statement $A$ in some powerful theory $T$ that can formalizes most part of mathematics such as $ZFC$ and (2) you want to consider provability or unprovability of $A$ in the theory $T$, (3) you want to consider provability or unprovability of "$A$ is unprovable in $T$" in the meta-theory that is $T$ itself or possibly reasonable extensions of $T$.

  1. It is not so obvious which statements actually express that "$A$ is provable in $T$", but there is one statement that do express it and you may be wanting to consider: the arithmetical statement constructed by Gödel numbering and coding of the system $T$. Let's call it $P_T(A)$.
  2. Gödel proved that if $A$ is unprovable in the system $T$ (and therefore $T$ is consistent) then $\neg P_T(A)$ can never be proved in $T$ (Second incompleteness Theorem). So there are no statements $A$ such that $A$ is unprovable $T$ and its unprovability expressed with the Godel formula $\neg P_T(A)$ can be proved in $T$ itself.
  3. Given a statement $A$, altough $\neg P_T(A)$ is never provable for a consistent $T$ (as stated above) it is still possible that $\neg P_T(A)$ can be proved in a stronger system, for example in the system $T'=T+\text{Con}(T)$ (where $\text{Con}(T)$ is the Godel formula expressing the consistency of $T$ as an arithmetical statement) or maybe $T''=T+\text{Con}(T)+\text{Con}(T+\text{Con}(T))$ or other reasonable consistent extensions of $T$, and there would be no way to decide in general which of these extensions (if any) would eventually be able to prove it.
  • $\begingroup$ Your point (1) has an error. It is not relevant whether $T$ is strong enough, but whether the theory in which you want to write $P_T$ is strong enough (to do coding of strings). $T$ does not need to be strong at all, but only needs to have decidable proof validity. $\endgroup$
    – user21820
    May 2 '16 at 2:55
  • $\begingroup$ By what I said, it is clear that only point (2) needs $T$ to be strong enough to do standard string manipulation (equivalently arithmetic), otherwise $P_T$ either has no meaning or cannot even be stated. Regarding point (3), it's kind of trivial if you have Con(T), because it explicitly states "$\neg P_T(\ulcorner \bot \urcorner)$". So I'm not sure why you mention further extensions? $\endgroup$
    – user21820
    May 2 '16 at 3:14
  • $\begingroup$ @user21820 you are right about (1), "strong" refers to the ability to prove arithmetical theorems, what I needed to say instead is that $T$ can actually express arithmetical statemets (I fixed it, thank you). I don't understand the problem with (3): af far as I can see it is entirely possible that $T'=T+\text{Con}(T)$ is not able to prove $\neg P_T(A)$ for some specific statement $A$ while $T''=T'+\text{Con}(T')$ can prove it (as an example just consider $A=\neg P_{T'}(\text{Con}(T'))$ assuming $T$ and $T'$ are consistent). $\endgroup$ May 2 '16 at 6:09
  • $\begingroup$ (1) Your statement is still incorrect. As I said, it is **the theory in which you want to write $P_T$, not $T$ itself. For example $T$ could be the theory of dense linear orders, but $P_T$ still can be expressed in $PA$, and in fact $PA \vdash \neg P_T(\ulcorner \bot \urcorner)$. (2) This is the one that needs $T$ to be strong enough. (3) Yes what you say in your comment is true but your answer does not say that at all! $\endgroup$
    – user21820
    May 2 '16 at 7:37
  • $\begingroup$ I have edited to make explicit some assumptions I am making in my answer. In my comment on (3) I was just answering to the remark "it's kind of trivial if you have Con(T)", I still don't understand why it is trivial to consider extensions of T including Cont(T) as an axiom. $\endgroup$ May 2 '16 at 11:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.