# What does a nonstandard proof of Con(PA) look like?

As in Godel's incompleteness theorem natural numbers encode proofs of theorems. Due to Godel's completeness theorem there is a natural number (in some nonstandard model) that proves $Con(PA)$.

What number is it? What can we say about it?

-

You can say the same sorts of things that you can say about any other coded proof. In particular, the number is a code for a sequence $\langle \phi_1, \ldots, \phi_k\rangle$ of formulas such that $\phi_k$ is $\text{Con}(PA)$, and every formula in the sequence is either an axiom or is obtained from two previous formulas by modus ponens.

There are two keys ways in which the nonstandardness is relevant:

• Because the model really is not wellfounded, the "proof" coded by a nonstandard number may also not be well founded. In other words we may have a formula in the proof that is obtained by modus ponens from two formulas obtained by modus ponens, each of which was obtained by modus ponens, etc., so that if we trace backwards we never reach an axiom in a finite number of steps. Of course PA proves "every formula in a coded proof is obtained by a finite number of applications of modus ponens" but in a nonstandard model this can be a nonstandard finite number of applications.

• Because the induction axiom in PA is a scheme, and because the scheme is represented as an infinite sequence of formulas indexed with natural numbers, in a nonstandard model there are nonstandard instances of the scheme which can be used as axioms. Thus, even if the proof happened to be well founded (in other words, if every formula in the proof is obtained from axioms in a standard-finite number of applications of modus ponens), some of the axioms that are used may not really be axioms of PA, because they are nonstandard instances of an axiom scheme.

What we can say is that, since PA is consistent, the coded proof of $\text{Con}(PA)$ cannot be a standard number. Thus one of the two bullets above has to occur.

-
The induction axiom scheme isn't the only possible source of nonstandard formulas in a proof. You could have nonstandard instances of propositional axioms (tautologies) or of quantifier axioms. –  Andreas Blass Nov 23 '12 at 3:49

I don't know of any specific properties of the "number" that encodes the proof, but a basic analysis of the order type of a countable non-standard model can be quite illuminating.

The first thing to consider is that in the model, all the elements which are the result of the successor function on 0 behave exactly like their counterparts in the standard model. In other words - the standard model is embedded in this model. Further, it is easy to show that it is a prefix of the non-standard model. We shall call these the "naturals".

Since this non-standard model has an element which doesn't behave like any natural number (the Con(PA) proof), it has at least one element which is larger (using the order relation) than all the "naturals".

Now we partition the model according to the equivalence relation "A is reachable from B using a finite number of successor function (or vice versa)", (equivalently - the difference between the two is a "natural number"). Each equivalence class has the order property of either N (the first one - which is the "naturals"), or of Z (all the rest), and are "continuous chunks" of the order (since the axioms require that each element has a successor larger than it; that only 0 doesn't have a predeccesor; and that the there aren't any elements between X and S(X)). Therefore, we can regard the order relation as a relation also between different equivalence classes (since it will hold for all choices of representatives of the classes).

By adding any "non standard" number to itself, it is easy to show that there are an infinite number of different equivalence classes (obviously countable - since the model is countable). Using induction, we are able to show that each two numbers have an "average" - and by averaging out numbers from different equivalence classes, we get an equivalence class between the two classes. Therefore the order relation, regarded upon the classes, is a countable implementation of DLO (Dense Linear Order).

A result of Cantor shows that every countable model of DLO is isomorphic to the rationals. Therefore the order type of the model is equivalent to $\mathbb{N} + \mathbb{Z} \times \mathbb{Q}$.

-