Can we use remote provability to prove the first incompleteness theorem sans $\omega$-consistency?

Question

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$?

Answer 1

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. 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.

Answer 2

This proof is related to this method, though it is basically Rosser's but in a twisted way:-

$\textbf{Define: } \\\begin{align} \kappa \text { is remote } \iff \exists \mathcal s: \ & (\kappa = \min x: \operatorname {Proof}_T(x,\ulcorner \mathcal s \urcorner)) \ \land \\ & \exists y \,(\operatorname {Proof}_T(y,\ulcorner \neg \mathcal s \urcorner ) \land y < \kappa) \end{align} $

Now, $\kappa$ cannot be a standard natural! Since if so, then we'll have $T \vdash \mathcal s$ and so $T \vdash \neg \mathcal s$ because both proofs would have standard codes.. Now, Since $``\kappa \text{ is remote}"$ is an expression in the language of $\sf PA$, then if fulfillable it must have a minimal (by Induction), and of course that minimal must be non-standard! Take $\frak K$ to be the minimal remote number. From the fixed point lemma, we have the sentence $\mathcal g$ defined as:

$\textbf{Define: } \mathcal g \iff \forall x \, (\operatorname {Proof}_T (x,\ulcorner \mathcal g \urcorner ) \to x \geq {\frak K})$

This is a standard sentence, and we have: $$(T \not \vdash \mathcal g) \land (T \not \vdash \neg \mathcal g)$$

If we don't have any remote number. Then let $\mathcal G$ be defined as usual, after Gödel, as:

$\mathcal G \iff \neg \exists x: \operatorname {Proof}_T(x,\ulcorner \mathcal G \urcorner)$

If $T$ is complete then it'll prove $\neg \mathcal G$, and so proves the existence of a code $x$ such that $\operatorname {Proof}_T(x,\ulcorner \mathcal G \urcorner)$, take the minimal of these codes and it would be a remote number, a contradiction.

Note: I used the notation $\ulcorner \neg \mathcal s \urcorner$, but basically I mean by it Rosser's negation function.