**Mail folder:**QED**Next message:**Robert S. Boyer: "Feferman FSO reference"**Previous message:**guttman@linus.mitre.org: "Re: Verification systems "**Reply:**John Harrison: "Re: Answer to a question, and further speculation on a QED foundation"**Reply:**David McAllester: "Answer to a question, and further speculation on a QED foundation"

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.