Con(PA) via non-well-foundedness?

Question

Lumsdaine made the following interesting comment:

if Con(PA) fails in a non-standard model, it means it contains a “proof of non-standard length” of a contradiction from PA. With a little work, one can externalise that to some non-well-founded “proof tree”, which has at each node a possibly-non-standard formula (which in turn externalises to some not-necessarily-well-founded syntax tree), where each step will genuinely follow from earlier steps by some standard rule of proof, but the whole tree will be non-well-founded, and hence not an actual proof.

Has this viewpoint on Goedel's theorem and Con(PA) been developed more fully elsewhere? I am told that a study of well-foundedness by Mints is relevant:

• G.E. Mints, Finite investigations of transfinite derivations, J Math Sci 10, 548–596 (1978). https://doi.org/10.1007/BF01091743

I did not find a direct connection to Con(PA) there. Could somebody elaborate on this approach to understanding incompleteness via non-well-foundedness?

Answer 1

This is a completely standard perspective in work on models-of-PA, a view that informs dozens of arguments. That is simply the nature of nonstandard models, that things they think are well founded are often not actually well founded.

For example, this way of thinking underlies the work on the universal algorithm.

Theorem. (Woodin) There is a Turing machine program $p$ with the following properties:

1. When it is run, it never halts, but during computation it places finitely many numbers in sequence on the output tape.
2. Furthermore, PA proves this. So in any model of PA, the program will produce a (possibly nonstandard) finite sequence.
3. In the standard model, the program runs forever but never places any numbers as output — it outputs the empty sequence.
4. In any model $M$ of PA, if the sequence output by $p$ is $s$, then for any finite extension $t$ of $s$ in $M$, there is an end-extension model $N$ of $M$, such that when $p$ is run inside $N$, it outputs $t$.

You can find my simplified proof in the article:

• Joel David Hamkins, The modal logic of arithmetic potentialism and the universal algorithm, 2018, arxiv:1801.04599.

The proof involves looking for proofs of inconsistency, necessarily nonstandard, and makes fundamental use of the fact that they are ill-founded in order to achieve the universal end-extension property.

Illustrating the method. Perhaps it is helpful to illustrate with one of the argument methods. Suppose that $M$ is a nonstandard model of PA+Con(PA), with nonstandard number $k$. Consider the theory $\text{PA}_k$, consisting of the first $k$ axioms as enumerated inside $M$ in the usual way of describing the theory. Since $k$ is nonstandard, this list will include many nonstandard axioms, things that $M$ thinks are axioms of PA, but which aren't actually assertions at all, just as mentioned in the OP.

Since $M$ thinks that $\text{PA}_k$ does not prove $\text{Con}(\text{PA}_k)$, it follows that $M$ thinks $\text{PA}+\neg\text{Con}(\text{PA}_k)$ is consistent. And so inside $M$ we can form a complete consistent Henkin theory extending this theory. The equivalence classes of constants gives a model $N$ of this theory. And since $M$ can form that interpreted model, it follows that $M$ is isomorphic to an initial segment of $N$ by the map sending $x$ to the value of the term $\overbrace{1+\cdots+1}^x$ in $N$. (Note that $x$ could be nonstandard in $M$, and this term would be a nonstandard term, in the same manner mentioned in the question, but $M$ knows nothing about that distinction.)

So $N$ is an end-extension of $M$ and a model of $\text{PA}_k+\neg\text{Con}(\text{PA}_k)$. Since every standard axiom of PA appears at a standard stage of the enumeration and $k$ is nonstandard, it follows that the full standard theory of PA is included in this theory. So $N$ is a model of PA in which $\neg\text{Con}(\text{PA}_k)$, that is, in which PA becomes inconsistent with the $k$th axiom.