Delivery-Date: 
From: boyer@CLI.COM (Robert S. Boyer)
Date: Tue, 20 Sep 94 09:47:03 CDT
Message-Id: <9409201447.AA09823@rita>
To: nqthm-users@CLI.COM, mind@aisb.ed.ac.uk, indus@cs.uiowa.edu, 
    qed@mcs.anl.gov
Subject: Kunen's Checking of the Paris-Harrington Ramsey Theorem in Nqthm
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

Ken Kunen (kunen@cs.wisc.edu) has recently checked the Paris-Harrington Ramsey
theorem using Nqthm.

Historically, one reason this Paris-Harrington Ramsey theorem has been found
especially interesting is that it was shown that it cannot be proved in
elementary number theory.  (As we know from Goedel's famous theorem, not all
truths of elementary number theory, if it is consistent, can be proved in
elementary number theory, e.g., the consistency of elementary number theory.)
However, this particular Paris-Harrington Ramsey theorem turns out to be a
theorem of Primitive Recursive Arithmetic + induction up to the ordinal
epsilon-0.  (It was induction up to this same ordinal that Gentzen used to
prove the consistency of elementary number theory.)  Nqthm supports induction
up to epsilon-0, and in this proof-checking effort, Ken Kunen made the first
real use of that inductive power in Nqthm.  Lest anyone misconstrue this
message, let me emphasize that the proof-checking effort I am describing does
not also include a checking of the unprovability of the Paris-Harrington Ramsey
theorem in elementary number theory.

The Nqthm script for this Paris-Harrington theorem may be obtained as the file
/pub/nqthm/nqthm-1992/examples/kunen/paris-harrington.events by anonymous ftp
from ftp.cli.com.  About 11,000 lines.  Takes about 12 minutes to check on a
fast Sparc.

A paper on this work may be found as http://www.cs.wisc.edu/~kunen/kunen.html
under Mosaic.

Bob

P. S. To obtain Nqthm-1992, connect to Internet site ftp.cli.com by anonymous
ftp, giving your email address as the password, `get' the file
/pub/nqthm/nqthm-1992/README, and follow the instructions therein.