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:

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


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

Universal algorithm end-extension

You can find my simplified proof in the article:

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.

  • 2
    $\begingroup$ Thanks! Curiously, nobody elaborated this viewpoint at mathoverflow.net/questions/458983/… $\endgroup$ Nov 30, 2023 at 13:33
  • 2
    $\begingroup$ Your article doesn't actually use the terms "ill-founded" or "well-founded". What equivalent terms are you using there? $\endgroup$ Nov 30, 2023 at 14:20
  • 4
    $\begingroup$ The article is almost entirely about non-standad models! In the standard model, the universal algorithm outputs the empty sequence. The algorithm outputs a provably finite sequence because the number k in the proof is dropping, and since PA proves the numbers are well-ordered, this can drop only (nonstandardly) finitely many times. $\endgroup$ Nov 30, 2023 at 14:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.