# Is truth outrunning provability equivalent to undecidability of some statement in a theory?

The Wikipedia exposition of Boolos's proof of Godel's first incompleteness theorem assumes that the first incompleteness theorem is equivalent to non-existence of an algorithm that outputs all true sentences of arithmetic and contains no false ones. Also by the end of this proof, it states that "truth outruns proof".

What is the proof of this equivalence?

Godel's incompleteness as usually stated is not about unprovability of a true sentence, it's rather about presence of undecidable statements in the language of the respective theory; that is, there is a statement that the theory in question neither proves nor disproves. And that doesn't seem at first glance to be equivalent to truth outrunning provability.

I mean if theory $$T$$ is incomplete, then of course we'll have the situation where a true statement is unprovable in it, but the converse doesn't seem to necessarily hold. I mean in principle we may have a theory that doesn't prove every true sentence to be true, yet it can decide on all sentences of it, i.e. it can prove some true sentence (i.e. satisfied by a standard model of arithmetic) to be false. Otherwise the usual Godel proof won't be needing the assumption of $$\omega$$-consistency to establish the first incompleteness theorem. Since, even without it we do have the usual Godel argument proving the existence of a true sentence, namely the Godel sentence, that the theory doesn't prove. It is known that the $$\omega$$-consistency assumption is not needed for that part of Godel's proof, it is only needed to establish the unprovability of the negation of the Godel sentence. All in all, it appears to me, that "truth outrunning proof" is weaker than "the theory cannot prove nor disprove some sentence". So, they are not clearly equivalent.

What I mean is that even if one proves that "truth outruns proof", still that doesn't mean that he proved the incompleteness result. So, I don't see how Boolos's argument proves the first incompleteness result. Did he demonstrate the existence of an undecidable statement?

• Godel's proof relies on encoding "what it means for a given statement to be provable in T" as a statement in "T". It applies only to theories which are capable of such an encoding, which are a subset of incomplete theories.It uses the diagonal argument to construct the famous "I am unprovable" statement.Both that statement and its negation are unprovable, and consistent with the theory.But only its truth is faithful to the initial interpretation of statements of T as encoding facts of the about the provability of T. Its negation would correspond to nonstandard, infinitary models of arithmetic. Commented Aug 26, 2023 at 20:33
• As for Boolos's statement, if something is provably true, then a brute force algorithm going trough the deductions of T will (eventually) prove it true. There is (for all effective theories) an algorithm that enumerates all provably true sentences, and no unprovable ones. We may combine Boolos's statement of the non-existence of an algorithm for all true sentences, with the existence of an algorithm for all provable ones. Thus, the set of provable sentences is strictly smaller than the set of true ones. Commented Aug 26, 2023 at 21:24
• @user3257842, I think you are speaking of "proof" in the meta-theoretic sense usually denoted by $\vdash$. But if matters are as such then what's the need for $\omega$-consistency in Godel's original proof of first incompleteness? You see, without $\omega$-consistency, it is possible to have $T \vdash \neg \sigma$, where $\sigma$ is the Godel sentence. But, the Godel sentence is true, and so $T$ would be proving it false? So, your claim that all provably false sentences are false is not correct. It is only correct if we assume $\omega$-consistency. But, Boolos's proof doesn't assume that. Commented Aug 27, 2023 at 10:57
• @user3257842, I think what you expressed by saying that all provably true sentences by theory $T$ are true in the standard model and all provably false senences by $T$ are false in the standard model, this is saying that $T$ is sound. This is known to be false if $T$ is assumed complete and fulfilling Godel's criteria of representing all computable functions. I think this is called the "weak" first incompleteness theorem, and it is easily provable. Again, this is not the known first incompleteness theorem. It's just a weak version of it. Commented Aug 27, 2023 at 11:06
• @user3257842, if Boolos's proof assumes soundness, then yes it'll prove the first incompleteness. Which is in reality the weak first incompleteness. But, from the Wikipedia article on Boolos's proof there is no assumption of soundness nor of $\omega$-consistency. There is only an assumption of equivalence of "truth outruns proof" and incompleteness, but is there a proof of that assumption when $T$ is not sound for example? Commented Aug 27, 2023 at 11:20

This article answers the above question to the negative. It shows that Boolos's proof is not Rosserable! And that it is equivalent to the same assumptions underlying Godel's original proof, that of a theory being consistent with it's own consistency statement, or simply of a theory not proving it's own inconsistency, a result due to Isaacson.

https://arxiv.org/abs/1612.02549