Alternative proof of Godels first incompleteness theorem

**Define:** $\mathcal F(x)$ is the sentence form:

"*$x$   is the Gödel code of a sentence whose negation is provable in   $T$   or is the extractee of such a number*"

**Define:** a Gödel number $n$ is called the *extractee* of a Gödel number $m$ if and only if there is a sentence form $\mathcal G(x)$ such that $n=\ulcorner \mathcal G(x) \urcorner$ and $m=\ulcorner \mathcal G(\ulcorner \mathcal G(x)\urcorner)\urcorner$.

We work under the usual Godel assupmptions of $T$ being a first order theory capable of representing all computable functions.

We'll use the notation presented in the Wikipedia [page][2] on Rosser's trick.

By "$S$ is provable in $T$" (or "$T$ proves $S$") we specifically mean $\exists x: \operatorname {Proof}_T(x,\ulcorner S \urcorner)$

While if "its negation is provable in $T$", we me specifically mean: $\exists x: \operatorname {Proof}_T(x,\operatorname {neg} (\ulcorner S \urcorner))$

The usual metatheoretic syntactical notion of $T$ proving $S$, shall be denoted as $T \vdash S$, in order to discriminate it from the theoretic provability statements mentioned above.

An important feature of $\exists x: \operatorname {Proof}_T(x,y)$ (which is the same formula $\mathcal {Bew}(y)$ of Gödel's) is as proved by Gödel if $T \vdash S$ then $ T \vdash \exists x: \operatorname {Proof}_T(x,\ulcorner S \urcorner)$ . This is because any syntactic proof of $S$ would have a corresponding Gödel number, the existence of which causes $\exists x: \operatorname {Proof}_T(x,\ulcorner S \urcorner)$ to be satisfied.

Now, to capture the above definitions:

$\textbf{Define: } \\\begin{align} \mathcal F(x) \iff &\exists p: \operatorname {Proof}_T (p,\operatorname {neg}(x)) \lor \\& \exists q \exists y: \operatorname {Proof}_T (q,\operatorname {neg}(y)) \land x=\zeta (y)\end{align}$

Where $\zeta: \mathbb N \to \mathbb N $ is the function defined by: $\zeta(\ulcorner \mathcal G (\ulcorner \mathcal  G(x) \urcorner )\urcorner) = \ulcorner \mathcal G(x) \urcorner $

$\textbf{Claim: }$

Assume $T$ is effectively generated, complete, and fulfills the following Consistency statement: $$\forall y \,  \big{(}  \exists x \, [\operatorname {Proof}_T (x,y)] \uparrow \exists  z \, [ \operatorname {Proof}_T(z,\operatorname {neg}(y))]\big{)}$$

Where "$\uparrow$" is the Sheffer stroke. 

Then the sentence $\mathcal F( \ulcorner \mathcal F\urcorner)$ is neither provable (syntactically or theoretically)  nor its negation is provable (syntactically or theoretically) in $T$?

$\textbf{Proof:}$

If $T \vdash \mathcal F( \ulcorner \mathcal F \urcorner)$,

then $T$ proves $\mathcal F( \ulcorner \mathcal F \urcorner)$, [Gödel]

then $\neg\mathcal F( \ulcorner \mathcal F \urcorner)$  is not provable in $T$,   [Consistency of $T$] 

$ \ulcorner  \mathcal F\urcorner$ is the extractee of  $\ulcorner \mathcal F( \ulcorner \mathcal F\urcorner)\urcorner$ [definition of extraction],

then $T \vdash \neg \mathcal F( \ulcorner \mathcal F\urcorner)$ [definition of $\mathcal F(x)$],

a contradiction. 

If $T \vdash \neg \mathcal F( \ulcorner \mathcal F\urcorner)$,

then $\neg \mathcal F( \ulcorner \mathcal F\urcorner)$ is provable in $T$, [Gödel]

 $\ulcorner \mathcal F\urcorner$ is the extractee of  $\ulcorner   \mathcal F( \ulcorner \mathcal F\urcorner)\urcorner$, [definition of extraction]

then $T \vdash \mathcal F( \ulcorner \mathcal F \urcorner)$, [definition of $\mathcal F(x)$]

a contradiction. 

This is a clean direct simple proof, no need for diagonalization, it straightforwardly establish the result. 

If we use Rosser's trick and further improve on this proof by redefining $\mathcal F(x)$ in terms of strong provability in $T$, as:

"*$x$   is the Gödel code of a sentence whose negation is strongly provable in $T$ or is the extractee of such a number*"

Where strong provability is defined as:

 $S$ is strongly provable in $T$ if and only if there is a Gödel code of its proof in $T$ that is strictly smaller than any Gödel code of a proof of its negation in $T$

Formally:

$ S \text { is strongly provable in } T \iff \\ \exists x: \operatorname {Proof}_T(x, \ulcorner S \urcorner ) \land  \forall y (\operatorname {Proof}_T (y, \operatorname {neg}(\ulcorner S \urcorner)) \implies x < y ) $

Then the above proof would be carried out just under the assumption of the usual syntactical consistency of $T$.