[FOM] Could PA be inconsistent?
William Tait
wwtx at earthlink.net
Fri May 14 12:26:06 EDT 2004
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.
More information about the FOM
mailing list