Can Godel's incompleteness theorems be in some sense circumvented this way?

Question

New foundations "NF" (formulated in the language of $\small \sf FOL(\in)$), can define a kind of ordered pair relation $``\rho"$ such that we can have a set $E$ of those pairs where NF proves the existence of an ordered pair $(V,E)$ and at the same time NF proves each sentence $\alpha'$ that replaces each formula $x \in y$ in an axiom $\alpha$ of NF by the formula $\exists q \in E (\rho(q,x,y))$, and bound all variables in $\alpha$ by $V$. $\alpha'$ to be referred to as the $(V,E)$ version of the original axiom $\alpha$. In nutshell NF proves all $(V,E)$ versions of axioms of NF, and NF proves the existence of $(V,E)$ as a set in its universe of discourse (i.e. in all of its models).

The definition of $\rho$ is:

Define: $\rho(q,x,y) \equiv_{df} q=(\{x\},y)$

Where $``(-,-)"$ is the Kuratwoski implementation of ordered pairs.

$x,y$ to be called the first and second $\rho$-projections of $q$.

The open expansion of the above definition is stratified, and so the set $E$ defined as the set of all $\rho$ pairs whose first $\rho$-projection is an element of their second $\rho$-projection, is provable (by NF) to exist in $V$.

This supply the pseuo-appearance of NF proving the existence of a model of it, thus proving its own consistency, thereby being inconsistent. However this is not the case, for although $(V,E)$ do in fact models all axioms of NF, yet NF does not have a single statement describing that (even though the number of axioms of NF can be finite), so NF doesn't see $(V,E)$ as a model, even though in some external sense $(V,E)$ is a model of NF.

My question: can in a similar way a set theory $T$ prove the existence of a structure $(M,R)$ such that $T$ proves all $(M,R)$ versions of axioms of a set theory $T^+$ that is strictly stronger than $T$?

If that can happen, then in some sense Godel's incompleteness theorems would look like as if it is circumvented! I don't mean by this that it is actually circumvented, but rather I mean that some theories can advance some syntactical provability that looks like proving something that one wouldn't think it possible given the usual connotation associated with Godel's incompleteness theorems

Answer 1

The role of NF here seems to me a red herring. ZFC (say) already exhibits a similar phenomenon: there is a single formula $\varphi$ such that in every model $M$ of ZFC, $\varphi^M$ is a model of ZFC. PA exhibits a similar phenomenon. I'll talk about both of these below, and also end by addressing an issue in your post.

(Granted, this does omit the "strictly stronger" aspect of your question, but I think it sufficiently de-mystifies the situation that it's worth posting as an answer.)

---

Specifically, suppose $M\models$ ZFC. We break into cases. If $M\models$ Con(ZFC), then $L^M$ also satisfies Con(ZFC), and so "the $L$-least constructible model of ZFC" defines a unique model of ZFC in any model of ZFC+Con(ZFC).

Now what if $M\models\neg$Con(ZFC)? Let $n$ be (in $M$) the least natural number such that the conjunction of the first $n+1$ axioms of ZFC is inconsistent (note that the existence of such an $n$ relies only on the fact that ZFC proves that the naturals satisfy I$\Sigma_1$).

By the reflection theorem, this $n$ is nonstandard (I've seen overspill invoked at this point but as far as I can tell it's unnecessary). From this it's easy to check that externally anything $M$ thinks is a model of the first $n$ axioms of ZFC is actually a model of full ZFC. The formula "the $L$-least constructible model of the first $n$ axioms of ZFC" then defines a unique structure in $L^M$, which - again, externally - satisfies the ZFC axioms.

Combining these, we have our $\varphi(x)$:

"If ZFC is consistent then $x$ is the $L$-least constructible model of ZFC, and otherwise $x$ is the $L$-least constructible model of the first $n$ axioms of ZFC where $n$ is the least natural number such that the first $n+1$ axioms of ZFC are inconsistent."

Note: we used the assumption of the consistency of ZFC in the assertion that $n$, if it exists in our model, is nonstandard; this is why the above does not go through in ZFC alone. The same issue appears in the PA situation below.

---

A similar situation holds for PA. Like ZFC, PA proves (nonuniformly) the consistency of each of its finite subsets, and also the existence (if PA is inconsistent) of a minimal $n$ such that the first $n$ axioms of PA are inconsistent. Combining these, any model of PA either thinks already that PA is consistent or thinks that a definable fragment of PA which externally contains PA is consistent.

We have to operate on the level of theories as opposed to models since PA can't actually talk about (infinite) structures. However, I think this actually makes things better: it shows that the issue is really syntactic, and talking about models - while simpler in many ways - possibly adds a bit of mystery where there shouldn't be any.

---

Now what about NF in particular?

I really only see one interesting point about NF in this context: its finite axiomatizability. You acknowledge this, but claim it doesn't matter:

This supply the pseuo-appearance of NF proving the existence of a model of it, thus proving its own consistency, thereby being inconsistent. However this is not the case, for although $(V,E)$ [does] in fact [model] all axioms of NF, yet NF does not have a single statement describing that (even though the number of axioms of NF can be finite).

But this doesn't work - the culprit is the passage where you claim without proof that facts pass over to $(V,E)$ appropriately. Presumably you want to say that for each $\psi$ in the usual axiomatization of NF, NF proves the specific instance "$(V,E)$ satisfies $\psi$." However, this can't be true: since NF is finitely axiomatizable, some finite subset $\{\psi_1,...,\psi_n\}$ of the usual axiomatization already proves all of NF. Now replacing NF with the conjunction $\psi$ of these axioms right from the start, we'd get an impossible situation if everything you've written is correct:

• Since $\{\psi\}$ is an alternate axiomatization of NF, everything NF proves is also provable from $\psi$.

• Since NF proves that $(V,E)\models\psi$ we have $\{\psi\}\vdash(V,e)\models\psi$.

• But this violates Godel since NF also proves the soundness theorem.

So the transferring of facts to $(V,E)$ has to be more complicated than it may at first appear.

You haven't presented an argument for the relevant transfer, so I can't diagnose where it breaks down, but I suspect the culprit is the definition of "$\models$" which is more problematic than it may first appear. For example, the usual definition would be in terms of Skolem functions, and so we'd want to argue that if $\forall x\exists y(\theta(x,y))$ is true in our model then there is some $f$ in our model such that our model's $(V,E)$ satisfies $\forall x(\theta(x,f(x))$. But getting that $f$ would seem to require choice, which is inconsistent with NF. Of course this can't be the whole story since we can get choice by adding urelements. But it does underscore that there may be subtleties with how we define satisfaction, and per the above we know that there have to be unobserved subtleties somewhere here.