dam> I would define this position [the "LCF suffices" position] as
dam> stating that a verification system should only accept a theorem when
dam> a full proof in the base logic has been generated and verified.
I believe McAllester is envisioning fully expanded proof trees in the
base logic (and this is the LCF view), and that he is concerned that
such things are infeasible. Indeed we know that many operations on
proof trees frequently cited in informal mathematics are infeasible,
e.g. the deduction theorem is exponential for minimal implicational
logic. Still, we can retain the point of view that only a proof in
some given base logic is evidence for a theorem in that logic without
necessarily committing to fully expanded proof trees.
This is informal talk, so consider a formal system (call it a
"framework") for presenting formal systems and derivations in those
systems. Feferman's FS0 has been discussed on this list, as has the
Edinburgh Logical Framework (ELF). Different frameworks give
different notions of "formal system" that can be represented, but many
formal systems can be represented in many frameworks, so we don't have
to be specific. Now what is a proof in a represented formal system?
It is a term of the framework having some type or satisfying some
predicate. But this term may not be a fully expanded proof; it may be
constructed in some non-canonical way. For a simple example
Ackerman(10) is not a canonical natural number, and it is infeasible
to write in canonical form (SSS.........0), but it is easily seen to
be a natural number because, by construction, the Ackerman function,
when applied to a natural number, produces a natural number.
Similarly, the deduction theorem is a function from proof trees to
proof trees having type something like
Ded_Thm: forall Gamma, A, B.
provable(Gamma,A)(B) => provable(Gamma)(A->B)
where => is an arrow of the framework, and -> is an arrow of the
represented logic. Just as the Ackerman function allows us to know
that some infeasible objects actually are natural numbers, so the use
of (non-canonical) operations on proof trees allows us to construct
proofs whose canonical form is infeasible, and to know (in the
framework logic) that these really are proofs of some given judgement.
Reflection is one way to get non-canonical proof objects, but a
theoretically heavy way, that merges what I have called the framework
and the represented logic.
I believe John Harrison's argument in his recently cited paper is that
in a suitably chosen logic we don't need to use non-canonical proof
objects. For example, the deduction theorem is an atomic rule in HOL,
not an infeasible operation. I don't personally think we can really
formalize large parts of mathematics using fully expanded proof trees
without encountering feasibility problems, but Harrison's challenge to
give an example of such a problem is one I cannot meet at the moment.
McAllester suggests that the four color theorem (i.e. the Appel-Haken
"proof" of the four color theorem) is an answer to Harrison's
challenge, but I do not think so. For example, in Martin-L\"of Type
Theory we might write some programs (lambda terms), prove that they
correctly test some number-theoretic properties (show these programs
have some specified types), and run them to test that some particular
numbers have these properties. Along with the theorem that those
properties of those numbers imply the four color theorem, we get a
proof in the Type Theory of the four color theorem. Such a
construction is clearly big, but not clearly infeasible. The proof of
the four color theorem suggests that a base logic should have some
"internal" notion of computation, not necessarily that we will have to
accept some kind of evidence other than proof.
BTW, I have a paper that is a little more specific about non-canonical
proof objects in an LCF-like setting. It is available by ftp and WWW
from:
file://ftp.cs.chalmers.se/pub/users/pollack/extensibility.ps.gz
-- Randy Pollack
--------------------------------------------------------------------
Randy Pollack Phone: (+46) (0)31 772 1046
Chalmers University of Technology Fax : (+46) (0)31 16 56 55
S-412 96 Goteborg, SWEDEN Email: pollack@cs.chalmers.se
URL: http://www.cs.chalmers.se/~pollack/
--------------------------------------------------------------------