A try to capture the informal notion of "this sentence is not provable in less than $n$-many steps" where $n$ is a concrete natural.


Use the diagonal lemma to coin the following sentences, per each concrete natural $n$:


$\zeta\_n \iff \ulcorner \zeta\_n \urcorner \text { is not provable in }< S\_n(0)\text{-many steps}$


Where $S\_n(0)$ is the $n^{th}$ successor of zero.



> 
> Is there a proof that there must be some concrete $n$ such that $\zeta\_n$ is false!
> 
> 
> 


If that can exist then neither $\zeta\_n$ nor $\neg \zeta\_n$ would be provable in the underlying theory if that theory is consistent. That is, it demonstrates incompleteness without the need of the assumption of $\omega$-consistency. That is, similar to the Rosser sentence in that respect.



Can this provide an example of incompleteness under the assumption of mere consistency?
No, quite the opposite in fact. Namely, if we have PA as the background theory, or some other minimal theory of arithmetic, and this theory is consistent, then all the sentences $\zeta\_n$ are true!


Let me assume that each $\zeta\_n$ asserts of itself that it has no proof in PA (or some other fixed sufficient background theory) in less than $n$ steps. Let us assume this counting is done in a systematic definite manner, perhaps simply by using Gödel codes, so that there are only finitely many such proofs for any given $n$.


The sentence $\zeta\_n$ cannot be provable in fewer than $n$ steps, since if it were, then we could prove this fact, that there was such a proof. But this would be proving the opposite of the assertion made by $\zeta\_n$ itself, and so we will have proved a contradiction, contrary to consistency.


Thus, no $\zeta\_n$ is provable by a short proof. And so every sentence $\zeta\_n$ is true.


But let me draw out a further consequence of this interesting situation. Precisely because there is in fact no short proof of $\zeta\_n$, this is something that admits of concrete proof in PA. We can simply enumerate all the proofs using fewer than $n$ steps, and prove of each of them that it is not a proof of $\zeta\_n$ (since in fact it is not). Thus, every $\zeta\_n$ is provable in PA, but only by a very long proof and not by any short proof.


Thus we have a speed-up phenomenon for proofs. Assuming consistency, no sentence $\zeta\_n$ has a short proof in PA, but they all have long proofs in PA. But they have short proofs in PA+Con(PA), because we just explained the argument above, and this can be formalized in PA.


I have recently noticed that one can use these observations to provide an alternative simple proof of the second incompleteness theorem (and so this restores somewhat your broader aim by another means). Namely, if PA proved Con(PA), then that proof would have some definite length. Consider $\zeta\_n$ where $n$ is much larger than this, and where $n$ has a comparatively short description. Above we showed how to provide a short proof from PA+Con(PA) that $\zeta\_n$ is true. By combining that argument with the given proof of Con(PA) in PA, we would obtain a short proof of $\zeta\_n$ in PA itself, which we have argued is impossible. So PA does not prove Con(PA).


I wrote on this in May 2023 in an essay on my substack, [Infinite Liars](https://www.infinitelymore.xyz/i/122078297/the-second-incompleteness-theorem). See also my [Twitter thread](https://twitter.com/JDHamkins/status/1654099992263503872) in which I describe the proof of the second incompletness theorem this way.


Meanwhile, the consideration of the sentences $\zeta\_n$ and the basic speed-up phenomenon seems to be due to:


* *Pudlák, Pavel*, On the length of proofs of finitistic consistency statements in first order theories, Logic colloq. ’84, Proc. Colloq., Manchester/U.K. 1984, Stud. Logic Found. Math. 120, 165-196 (1986). [ZBL0619.03037](https://zbmath.org/?q=an:0619.03037). [Citeseer pdf](https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=54952ff2ef51c3bea49b4dfaffd656a372f048db)


