If Peano Arithmetic cannot prove some true statements about the numbers, is that a defect of PA, and why do...

logic/peano.arithmetic New

New entry, edited from material collected for the archive and not yet in a released version.

Problem

If Peano Arithmetic cannot prove some true statements about the
numbers, is that a defect of PA, and why do logicians care about such a
weak system?

In article <1249@castle.ed.ac.uk> sean@castle.ed.ac.uk (S Matthews) writes:
>If PA cannot prove a true propostion about the numbers that is a problem
>with PA, not with the numbers as such.  Axiomatic systems can be a
>distraction from the real business.  Do you imagine that Hardy or Gauss
>worried about whether their proofs are expressable in PA.

[ Editor: problem statement reconstructed from the postings. ]

Show solution

I think this remark misses the point of things like PA.  I don't think
the inventors of PA were trying to come up with a formal system in
which to do what number theorists call number theory.

Look at the way PA is used by the people who are most concerned with
it, namely logicians.  Take for example the role played by PA in
Goedel's incompleteness theorems.  These theorems show that certain
things CANNOT be done if your formal system is AT LEAST as strong as PA
(and the axioms are recursively enumerable, which I think includes all
the formal systems anyone will ever look at even in principle).  Since
PA plays the role of a LOWER bound on the strength of theories, its
weakness is an ADVANTAGE rather than a disadvantage.  In fact, it makes
an even better theorem to weaken the lower bound to a FINITELY
axiomatizable theory (which can be done).

-- Ian Sutherland <ian%oravax.uucp@cu-arpa.cs.cornell.edu>