Which "natural" mathematical statements are known to be independent of the axioms of arithmetic, in the sense of Goedel's theorem?

logic/natural.independence New

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

Problem

Which "natural" mathematical statements are known to be independent of
the axioms of arithmetic, in the sense of Goedel's theorem?  Was
Chaitin's diophantine example the first?

In article <11167@quartz.BBN.COM>, dm@bbn (Dave Mankins) writes:
>Up until Chaitin's recent work, the kinds of statements that Goedel's
>theorem says exists (truths that can't be derived from a given
>axiomatic system) have always seemed like they would be pretty exotic.
>
>Now he has a reasonable-sounding question you can imagine a
>mathematician asking --- whether a given diophantine equation has a
>finite or infinite number of roots --- that is independent of his
>axiomatization of arithmetic.

[ Editor: the first sentence is the editor's. ]

Show solution

Chaitin's is not the first, unless you specifically define exotic with
his result in mind.

The Matiyasevich theorem, which the above depends on, is from 1970.  The
version for exponential diophantine equations (eg, FLT) was proven in
the early 60s by Robinson, Davis and Putnam.  The known diophantine
equations for which independence obtains are horrendously complicated,
so these are not considered "natural".  FLT is natural, of course, but
no one knows its status.

The Paris-Harrington theorem, derived in 1977--a simple strengthening
of the Ramsey theorem--is generally acknowledged as the first "natural"
PA independence result.  A year ago I posted the example of the
Goodstein numbers, from around 1980.

-- Matthew P Wiener <weemba@garnet.berkeley.edu>

[ Editor: see logic/goodstein for Goodstein sequences. ]

There has been a lot of work on independence results from various
theories, including PA, and various extensions of PA which are
properly subtheories of second-order arithmetic.  The relevant place
to look is in Contemporary Mathematics, Vol 65, entitled "Logic and
Combinatorics".  It's from a symposium on this very subject.

Also, there's the book "Harvey Friedman's Work on the Foundations
of Mathematics" from North-Holland, I think.

-- Chet Murthy <murthy@cs.cornell.edu>

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.

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>