How Might PA be Inconsistent?

The recent discussion of Edward Nelson's claim to have a found a proof that Peano arithmetic, $PA$, is inconsistent has been very interesting in many ways. The proof has turned out to contain a major flaw and Professor Nelson has very graciously withdrawn the claim. I was not able to follow the alleged proof because I don't know enough about Chaitin's Theorem, or about the properties of the system $Q_0^{\ast}$ being examined. But the episode set me thinking about what might lie behind an inconsistency in $PA$, despite the fact that we have many standard mathematical proofs that $PA$ is consistent (indeed, true).

For readers who are a bit rusty on the properties of first-order arithmetic, here is some background and attempted explanation. $PA$ is a basic mathematical theory which functions, for mathematical logicians, roughly as E. Coli functions for microbiologists. $PA$ is a theory expressed in a first-order formalized language $L_A$ (with identity) with

four primitive non-logical symbols: $0$, $S$, $+$, $\times$

Each of these is, in effect, functional. Along with the variables, $x_1, x_2, \dots$, one can define the terms of the language by saying that $t$ is a term if $t$ is $0$, or a variable, or is obtained by applying $S$, $+$ or $\times$ to previous terms. (This is a recursive definition.) Because $L_A$ has only one primitive predicate symbol, namely $=$, the atomic formulas of $L_A$ are equations, of the form

$t = u$,

where $t$ and $u$ are terms. For reasons of metalogical simplicity, it is usual to assume that the only logical primitives, beyond $=$, are $\neg$, $\rightarrow$ and $\forall$. Other truth-functional connectives can be defined (e.g., $\phi \vee \theta$ is short for $\neg \phi \rightarrow \theta$) and $\exists x \phi$ is short for $\neg \forall x \neg \phi$.

The $L_A$-formulas are defined, again recursively, by saying that $\phi$ is a formula of $L_A$ just if either $\phi$ is an atomic formula (i.e., an equation) or is obtained from previous formulas by applying connectives or a quantifier (i.e., $\forall x$).

The axioms of $PA$ are then specified as the following six individual axioms, and one axiom scheme.

Individual Axioms of $PA$:
$PA1$. $S(x) \neq 0$.
$PA2$. $S(x) = S(y) \rightarrow x = y$.
$PA3$. $x + 0 = x$.
$PA4$. $x + S(y) = S(x + y)$.
$PA5$. $x \times 0 = 0$.
$PA6$. $x \times S(y) = x \times y + x$

and

Induction Scheme: $IND_{\phi}$
$[\phi(0) \wedge \forall x(\phi(x) \rightarrow \phi(S(x)))] \rightarrow \forall x \phi(x)$

where $\phi(x)$ is a formula of $L_A$. The formula $\phi(x)$ may contain other free variables (called "parameters"). $\phi(0)$ means the result of substituting the term $0$ for all free occurrences of $x$ in $\phi$.

The axioms of $PA$ are then the above six and all instances of the Induction Scheme. In addition, there are underlying purely logical axioms, for example,

$\phi \rightarrow (\theta \rightarrow \phi)$
$\forall x \phi \rightarrow \phi(x/t)$

and, usually, one or two inference rules (e.g., Modus Ponens: from $\phi$ and $\phi \rightarrow \theta$, infer $\theta$). A derivation of $\phi$ in $PA$ is a finite sequence $(\theta_1, \dots, \theta_n)$ such that $\theta_n$ is $\phi$, and each, for $i \in \{1, n\}$, $\theta_i$ is either a logical axiom, or an axiom of $PA$, or is obtained by Modus Ponens on some previous $\theta_k$ and $\theta_p$. If there is a derivation of $\phi$ in $PA$, then $\phi$ is a theorem of $PA$, and we write:

$PA \vdash \phi$

Our specification of the axioms $PA$ is parasitic on our prior understanding of the set $N$ of natural numbers and their properties with respect to successor, addition and multiplication. So, one can define an $L$-interpretation $\mathbb{N}$ by specifying that $dom(\mathbb{N}) = N$, and that $0$ refers to $0$, $S$ refers to successor and that $+$ and $\times$ refer to plus and times.

This gives the interpreted language $(L_A, \mathbb{N})$. It is precisely this interpreted language that we have in mind when writing the axioms formally as opposed to informally. The constraint is that we formalize the informally expressed truths into truths of this language, and keep the interpretation fixed. One can verify that each axiom of $PA$ is true in $\mathbb{N}$. (The verification is in a sense circular. For example, the meta-theoretic assumption required to verify that $\forall x(S(x) \neq 0)$ is true is precisely the fact that $0$ is not a successor of any number. But this is no different from showing that the truth of "snow is white" follows from the assumption that snow is white. To show each axiom true, we assume that very axiom.) Since the inference rules are sound, it follows that each theorem of $PA$ is true. Consequently, since $0 = 1$ is not true, it follows that $0=1$ is not a theorem of $PA$. So, $PA$ is consistent. This reasoning can itself be formalized by adding a new truth predicate symbol to the language $L_A$ and setting out the required properties of truth. This leads to the area of axiomatic truth theories.

How might $PA$ be inconsistent? Here are four guesses:

1. Perhaps there is something wrong with the successor axioms (i.e., $PA1$ and $PA2$).
2. Perhaps there is something wrong with the defining clauses for $+$ and $\times$ (i.e., $PA3-PA6$: these are examples of definition by primitive recursion).
3. Perhaps there is something wrong with the induction scheme.
4. Some combination of the above.

The successor axioms force any model of them to be infinite. If $X$ is a set containing say $a$, and $f : X \rightarrow X$ is injective and such that $f(x) \neq a$ (for all $x$), then $X$ must be infinite. From the point of view of the theory itself, the infinity is only "potential" (the axioms $PA1$ and $PA2$ themselves does not assert the existence of an infinite object: rather, the semantic meta-theory asserts the existence of an infinite object---i.e., a model---satisfying them). So, presumably, for an inconsistency to arise with the successor axioms, there must be some problem with potential infinity. However, I really cannot see a genuine argument here, other than a dogmatic rejection of even potential infinity. (The objects in question are mathematical abstract objects, not concrete tokens.)

Perhaps defining arithmetic operations by primitive recursion is problematic, and potentially inconsistent. (There is a standard mathematical proof that it isn't: Dedekind's recursion theorem.) Perhaps because primitive recursions exhibit a kind of "circularity"? (Roughly, $f(n+1)$ is defined in terms of $f(n)$.) But, again, I cannot see a genuine problem, as the circularity is only apparent: a primitive recursive definition of a function $f$ allows one to compute $f(n)$, for any argument $n$, requiring only the values for smaller numbers.

What has been most often suggested is that the induction scheme might lead to an inconsistency somehow. Aside from general ultra-finitist concerns (which I think are based merely on type/token confusion), it's unclear what exactly might happen to generate an inconsistency. What seems a likely proof idea is that one could find a formula $\phi(x)$ and a term $t$ (no matter how specified) such that one can show:

Inductive Inconsistency of $PA$ with respect to $\phi(x)$ and $t$:
(i) $PA \vdash \phi(0)$
(ii) $PA \vdash \forall x(\phi(x) \rightarrow \phi(Sx)))$
(iii) $PA \vdash \neg \phi(t)$

To explain why we have not "observed" an inconsistency, it might be the case that the shortest derivation $d$ of $0=1$ remains incredibly huge. The reason is that the derivation would have to generate a canonical term $SSS....S0$ (say representing the number $n$), and prove $t = SSS...S0$, and apply Modus Ponens $n$ times to get $\phi(t)$, contradicting (iii). But the size of $n$ might be astronomical.

Perhaps an example is a theory $T$ with axioms:

1. $x + 0 = x$.
2. $x + S(y) = S(x + y)$.
3. $x \times 0 = 0$.
4. $x \times S(y) = x \times y + x$
5. $2^{0} = S0$.
6. $2^{S(x)} = 2 \times 2^{x}$
7. $F(0)$
8. $F(x) \rightarrow F(S(x))$
9. $\neg F(2^{2^{2^{2^{2}}}})$

(where $2$ is defined to mean $SS0$)
I think a similar example was first given by Rohit Parikh in the 1970s, though I haven't seen the original. So, this example might be quite different from Parikh's. If I've worked this out right, then $T$ is inconsistent, but the shortest derivation of an inconsistency has length at least $2^{65,536}$ symbols. (On the other hand, I may be wrong in specifying this: there may be a clever trick which allows one to get round the specification of a canonical numeral $SS...S0$ with $2^{65,536}$ occurrences of $S$.)

George Boolos, in a 1987 paper, "A Curious Inference", gave an example of a theory similar to the one above which is inconsistent, where the number of symbols in the shortest such derivation is an exponential stack of $65,536$ 2s. (Actually, Boolos gave a valid inference whose shortest derivation is of this length, but one can easily convert it to an example of such a theory by negating the conclusion formula.)