[FOM] Could PA be inconsistent?

[William Tait]

On May 13, 2004, at 6:18 PM, Martin Davis wrote:

> There are now two threads going on FOM contemplating this possibility. 
> No one has mentioned that we possess proofs that PA is consistent. 
> These proofs can be carried out in quantifier-free primitive recursive 
> arithmetic with induction permitted on a primitive recursive 
> well-ordering of the natural numbers of order type epsilon-0. These 
> proofs (Gentzen, Ackermann, G\"odel) have gone unchallenged for 
> decades.

Goedel's proof used, not induction up to epsilon_0, but only induction 
up to omega but involving primitive recursive functions of all finite 
types (his theory T). The trouble is that, understanding these relative 
consistency proofs is understanding that reasoning in PA, reasoning in 
PRA with induction up to epsilon_0 and reasoning in Goedel's theory T 
are all `essentially' the same. Of course, one might take as further 
evidence for the consistency of PA that no inconsistency has appeared 
or seems likely in these other systems as well; but this evidence seems 
not to touch on the possibility of an inconsistency involving induction 
applied to formulas at least 10^{10} symbols long.