From owner-qed Thu Oct 27 10:03:27 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA24767 for qed-out; Thu, 27 Oct 1994 10:03:16 -0500
Received: from cli.com (cli.com [192.31.85.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id KAA24762 for ; Thu, 27 Oct 1994 10:03:11 -0500
Received: from rita (rita.cli.com) by cli.com (4.1/SMI-4.1)
id AA16270; Thu, 27 Oct 94 10:02:39 CDT
From: boyer@CLI.COM (Robert S. Boyer)
Received: by rita (4.1) id AA13660; Thu, 27 Oct 94 10:02:38 CDT
Date: Thu, 27 Oct 94 10:02:38 CDT
Message-Id: <9410271502.AA13660@rita>
To: jmc@cs.stanford.edu
Cc: qed@mcs.anl.gov
Subject: Re: Semantics
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
jmc: > Exercise: Put the above discussion into PRA. See if another PRA
jmc: > fan can figure out what the hell you are talking about from reading it.
To put your argument "into PRA" in the natural way, what one would
probably do would be first to write in PRA a proof-checker for FOL and
then simply check for a specific, given proof object, that, say, ZF |-
Freiling's-Axiom -> ~CH. The traditional function of PRA is not to
carry the mathematics but to carry the metamathematics (the proof
theory), including to check concrete proof objects.
Historically clouding the issue is the fact that in recent years, some
people such as Harvey Friedman have shown, to the surprise of many,
that one actually can use PRA for powerful "higher level" mathematics
not just for a fragment of elementary number theory. (This involves
coming up with unusual ways to represent higher level things.) See,
for example, the appendices to the second edition of Takeuti's book
Proof Theory. But I don't believe anyone argues that PRA is the right
theory in which to explore questions about uncountable cardinals.
But this newly recognized power of PRA is not the purpose for which
PRA was invented by Skolem or advocated by Hilbert-Bernays for
metamathematics. PRA is very similar to the theories behind Skolem's
arithmetic, Goodstein's recursive arithmetic, and your logics for
Lisp: a simple logic for such very finite things as arithmetic and
symbol manipulation. And a logic that almost everyone believes. E.g,
in Goodstein's case (his book Recursive Number Theory), if I recall
correctly, the only rules of inference are (a) permitting the
definition of recursive functions, (b) inferring that two recursive
functions that satisfy the same defining equations are equal
everywhere, (c) instantiation, and (d) substitution of equals for
equals.
So your proposed "exercise" is about as odd as someone proposing the
same exercise for a Lisp-logic instead of PRA after reading one of
your early 60's papers such as "Towards a Mathematical Science of
Computation" or "A Basis for a Mathematical Theory of Computation".
By the way, if one does a good job in defining PRA in the style of an
nice applicative programming language with good data structures,
including lists and symbols, then reading the concrete proof object
might actually be a real pleasure and easy for many to follow.
Especially if the proof-checker includes obviously correct but
powerful decision procedures for fragments of FOL, e.g., as in Ed
Nelson's checker qed, so that the proof object is not too long or too
tedious.
Bob