Answer to a question, and further speculation on a QED foundation

Robert S. Boyer <boyer@CLI.COM>
Date: Sun, 18 Apr 93 12:36:45 CDT
From: Robert S. Boyer <boyer@CLI.COM>
Message-id: <9304181736.AA13372@axiom.CLI.COM>
To: qed@mcs.anl.gov
Subject: Answer to a question, and further speculation on a QED foundation
Reply-To: boyer@CLI.COM
Sender: qed-owner
Precedence: bulk
Josh Guttman asks, in response to a remark by David McAllester,

   Do Boyer and Moore think of NQTHM as foundational in the sense of
   having a single intended model?

I feel a little bit queasy talking about `intension' in view of the
fact that all the consistent, recursively axiomatizable theories I
know about that include the primitive recursive functions admit
multiple models.  But that reservation made, I would agree entirely
with David: I do think of the recursive functions I define with
Moore's and my prover Nqthm (A Computational Logic Handbook, Boyer and
Moore, Academic Press, 1988) as having, intuitively, all of the
specificity of ordinary programs.  Technically, as Guttman rightly
points out, we leave room in our system for the addition of new data
types, and via that mechanism one could in principle go on to
axiomatize such theories as set theory, perhaps even using Matt
Kaufmann's skolemizer.  And we also leave room via our
CONSTRAIN/FUNCTIONALLY-INSTANTIATE mechanism for proving very limited
types of theorems about classes of functions rather than specific
functions.  But if we are talking about ordinary, typical Nqthm use,
and within the spirit of informality, then I think that David is
entirely right.

I think McAllester is helpfully trying to put us at one end of the
typical theorem-prover map, on the other end of which one might find a
resolution theorem-prover to which one might well come from time to
time with an entirely fresh new set of axioms describing whatever one
wants -- groups, fields, rings.  Nqthm has not been used much in this
way, though I suppose it is capable of checking any first order,
resolution style proof.  But probably much poorer than many provers at
finding such a proof.

To connect back to some points in the QED manifesto, I think of Nqthm
as being one of those provers with `too much code to trust'.  There
are perhaps 5,000 to 10,000 lines of Nqthm that one would have to
prove correct in order to have the sort of confidence in the proofs it
finds that one might have in, say, a typical resolution style proof,
which can be checked with a very tiny checker.

On the other hand, a certain subset of the Nqthm logic is in the
spirit of Primitive Recursive Arithmetic (PRA).  It seems to me
crucial that if the QED project is to have the support of the now very
wide constructivist community, then underlying QED must be some such
logic to which everyone can agree.  In the past, the ordinary
mathematical community has probably regarded constructivism as being
of marginal significance.  Perhaps the typical math department has at
most only one or two people who think about such issues as
constructivism.  But the impact of computing on logic (and vice versa)
has had the effect that it would not surprise me if today half of the
people working on things like mechanical proof checking are of a
somewhat constructivist bent.  A too clasically powerful base logic
would thus from the start perhaps leave out many potentially major
contributors to the QED project.

The key point, I think that classicist David Hilbert would say, is
that WE CAN ALL AGREE to present and discuss essentially all important
logics and theories in a `finitistic' format, such as PRA admits.  (I
wouldn't be so bold to make such a sweeping claim if I weren't more or
less trying to repeat a point that Feferman has been making in recent
years in presenting his PRA-powerful logic FS0.)  We can all agree to
PRA proofs of many important metatheorems and of most automated
reasoning techniques (which typically are merely pieces of applied
proof theory).  And the constructivists can even agree to propositions
such as that some string, say, P, is a proof of a theorem TH in ZF set
theory.  But if we wire ZF or something classically quite strong at
the bottom of the QED edifice, the constructivists can't play.

I should temper my gospel fervor enthusiasm for PRA by observing that
while I agree with Tait (Finitism, J. of Philosophy, 1981, 78,
524-546) that PRA is THE NECESSARY AND SUFFICIENT logic for talking
about logics and proofs, there exists at least someone who refuses to
believe in PRA (Yessenin-Volpin, The Ultra-Intuitionistic Criticism
..., Intuitionism and Proof Theory, North-Holland, 1970, pp. 3-45).
But this fellow also refuses to believe in 10^12, which seems to fly
in the face of teraflops and terabyte memories.

Bob

There is no safety in numbers, or in anything else.  Thurber.