Let $\mathcal g\_1$ denote the usual Godel sentence defined as: $$ \mathcal g\_1 \iff \neg\exists x:\operatorname {Proof}\_T(x, \ulcorner \mathcal g\_1 \urcorner)$$


Lets suppose that $\sf T$ is consistent (metatheoretically), effectively generated, extends $\sf PA $, and complete.


Accordingly, $T \vdash \neg \mathcal g\_1$, that is, there is a natural $x$ that codes a proof of $\mathcal g\_1$. That is, formally we do have: $$T \vdash \exists x: \operatorname {Proof}\_T(x, \ulcorner \mathcal g\_1 \urcorner)$$


Let's call the smallest such Godel code by $\mathcal g^{\* 1}$


This is necessarily a non-standard natural.


Now we take another sentence $\mathcal g\_2$ that is defined as:


$\mathcal g\_2 \iff \forall x \, (\operatorname {Proof}\_T(x,\ulcorner \mathcal g\_2 \urcorner) \to x > \mathcal g^{\*1})$


This is what I call *remote provability*, so the above is a capture of the informal notion "every proof of this sentence is a remote proof", in other words "if this sentence is provable then it is remotely provable", where a remote proof means one that is coded by a non-standard natural. Actually the above sentence even adds more the claim that $\mathcal g\_2$ can only be remotely provable by exceeding $\mathcal g\_1$ provability.


Since $T$ is complete, then it will prove $\neg \mathcal g\_2$, and lets call the smallest Gödel code of a proof of $\mathcal g\_2$ as $\mathcal g^{\*2}$.


Now we do have $\mathcal g^{\*2} < \mathcal g^{\*1}$.


Let $\mathcal g\_3$ states it can only be remotely provable more than $\mathcal g\_2$ is, that is:


$\mathcal g\_3 \iff \forall x \, (\operatorname {Proof}\_T(x,\ulcorner \mathcal g\_3 \urcorner) \to x > \mathcal g^{\*2})$


And so on.. If we continue this for every concrete natural $n$, then we'll end up having $$ \mathcal g^{\*1} > \mathcal g^{\*2} > \mathcal g^{\*3} > ...$$


But, this cannot happen, since its provable in $\sf PA$ that there is no descending sequence of naturals. I say that because I think $(\exists n: x=\mathcal g^{\*n})$ is expressible in the language of $\sf PA$.


So, this must end up at some natural call it $\lambda$, i.e. we have: $\mathcal g^{\*\lambda+1} \not < \mathcal g^{\*\lambda}$.


But, by then we'll have: $T\not \vdash \neg \mathcal g\_{\lambda+1}$, proving the first incompleteness theorem.



> 
> Had this idea been explored before?
> 
> 
> 



> 
> Can we express the predicate *"being a $\mathcal g^{\*n}$ number"* in the language of $\sf PA$?
> 
> 
> 



Can we use remote provability to prove the first incompleteness theorem sans $\omega$-consistency?
It doesn't contradict PA to have such a descending sequence. For example, you could instead simply keep substracting one from $g^{\*1}$, and this would be provably descending, but there is no contradiction in that — it doesn't mean somehow that at some stage, substracting one gives a larger number.


The point is that such descending sequences could be part of a nonstandard finite sequence, making your $\lambda$ nonstandard. But you have been considering only the standard part of the sequence, and you lack a uniform argument that handles the sequence in its entirety. For example, in the steps where you argue it is descending, it is important that the sentences themselves are standard and have standard proofs.


This issue seems to break your argument.


Meanwhile, let me add that since you've asked several questions about avoiding $\omega$-consistency in the incompleteness theorem, the Gödel-Rosser version of the incompleteness completely avoids Gödel's now-extraneous $\omega$-consistency assumption. Also, there are proofs of the incompleteness theorem using the undecidability of the halting problem that avoid $\omega$-consistency.


Let me add that there is some affinity of your idea with the proof I give of the universal algorithm result. See my paper [The modal logic of arithmetic potentialism and the universal algorithm](https://arxiv.org/abs/1801.04599). In the main argument, one searches for the smallest proof of a certain statement. And having found it, one searches for a proof of a related next statement, using a strictly smaller fragment of PA — the new proof is necessarily larger. And then so on. In this way, a (possibly nonstandard) finite sequence is generated, and it is consistent with PA that the sequence is any sequence at all. What I find related to your idea here is that the proofs are necessarily getting longer, while the fragment of PA that is used is getting smaller. This is what ensures that the process stops growing at some (possibly nonstandard) stage.


