Can this Rosser-like trick also work as a proof of the first incompleteness theorem?

Question

The context of this question is related to proving the first incompleteness by alternative ways related to Rosser's trick. So, for a proof by negation, we assume that $T$ is complete, and fulfills Gödel's criteria of effectively capturing all computable functions, etc..

Can $T$ decide on sentence $\sigma$ defined below?

$\sigma \iff \\\forall k (\operatorname {Proof}_T(k, \ulcorner \sigma \urcorner) \to \\\forall s: \exists x [\operatorname {Proof}_T(x,\ulcorner s \urcorner) \land x \leq k] \lor \exists y [\operatorname {Proof}_T(y, \operatorname {neg} (\ulcorner s\urcorner)) \land y \leq k])$

In English this reads as: This sentence is only provable at lengths such that every sentence is either provable or disprovable below (non-strictly) it.

The idea is that, as defined, $\sigma$ can only be provable by proofs having non-standard Gödel codes, meaning that if $T$ is complete then $\sigma$ must be false, i.e. we have $T \vdash \neg \sigma$.

So, if we assume $T$ to be complete, then this criterion, I think, would separate standard from non-standards, so if a code of a proof doesn't fulfill that feature, i.e. not every sentence is decidable below it, then this code is standard!

However, I'm not sure of this later feature, that's why I'm not sure of the decidability of $\neg \sigma$ in $T$.

Of course this can be settled brutally by defining a minimal for such proofs, i.e. for example define:

${\frak K} = \min k : \forall s \, (\exists x [\operatorname {Proof}_T(x,\ulcorner s \urcorner) \land x \leq k] \lor \exists y [\operatorname {Proof}_T(y, \operatorname {neg} (\ulcorner s\urcorner)) \land y \leq k])$

Then define the diagonal $\pi$ as:

$\pi \iff \forall x (\operatorname {Proof}_T(x,\ulcorner \pi \urcorner) \to x \geq {\frak K})$

And clearly $\pi$ would be undecidable in $T$.

What is the status of $\sigma $ in $T$ should we assume that $T$ is complete and fulfill Gödel's criteria.

Answer 1

I see two major issues with the proposal.

First, if $\sigma$ is refutable, then in the standard model the biconditional will be vacuously true, since there will be no $k$ for which $\text{Proof}_T(k,\ulcorner\sigma\urcorner)$. This seems to trivialize the idea.

But second, even if one were to fix that somehow, the more serious point is that PA proves that there can be no number $k$ that serves as a bound for the size of a code of a proof of every sentence $s$ or its negation. The reason is that any proof a sentence must mention that sentence, and from this it follows (using any of the standard proof predicates) that the code of any proof will be at least as great as the code of the sentence being proved. Because you are asking for $k$ to have the property that it bounds the proofs of every sentence or its negation, this is impossible — there can be no number $k$ with the property mentioned on the RHS of your biconditional.

From this point of view, any $\sigma$ that fulfills the biconditional will itself have to be refutable.