Can this serve as an alternative proof of Gödel's first incompleteness theorem?

178 Views Asked by At

let $s$ be a standard sentence in the language of $T$. Let $E(s)$, called extension of $s$, be the sentence form: $$ \forall x \forall y \, (\operatorname {Proof}_T(x,v) \land y= \min z: \operatorname {Proof}_T(z,\ulcorner s \urcorner) \to x \geq y)$$

Now, let $\operatorname {Diagonal} (E(s))$ stand for the Godel code of the diagonal sentence of the sentence form $E(s)$

Now, define:

$\operatorname {Dgn}(x,y) \iff \exists s: y=\ulcorner s \urcorner \land x= \operatorname {diagonal}(E(s)) $

$remote(y) \iff \exists x \exists k \exists z: \operatorname {Dgn}(x,y) \land k=\min n: \operatorname {Proof}_T(n,y) \land z=\min m: \operatorname {Proof}_T(m,x) \land z < k $

Define: $x ={\frak K} \iff x = \min k : \exists y \, (remote(y) \land \operatorname {Proof}_T(k,y))$

take:

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

But if $T \vdash \neg \sigma$, then we'll have both $remote(\ulcorner \sigma \urcorner)$ and $\sigma$ having a proof that is strictly smaller than $\frak K$, a contradiction!

Thus $\sigma$ is undecidable in $T$.

QED

The idea is that if $remote(y)$, then every code of a proof of $y$ cannot be standard, since if so, then we must have the minimal proof of the diagonal of its extension being bigger than the minimal proof of it. So $\frak K$, the minimal a proof of a remote sentence can be, must be non-standard. The rest is clear!

The reason why $\operatorname {Dgn}$ is defined in arithmetic is because there is an exact syntactical way of producing $E(s)$ from $s$ and of producing $\operatorname {Diagonal}(E(s))$ from $E(s)$, so there is an arithmetical formula such that for any standard sentence $s$ we can input its Godel code and get the Godel code of the diagonal of its extension. We know how this behaves exactly for all standard codes of proofs, and so by definition of $remote$ sentences none of those can have proofs coded with standard naturals. Since, we can demonstrate there is at least one remote standard sentence (e.g., the Gödel sentence), then we do have a minimal of their proofs!