**Mail folder:**QED**Next message:**Konrad Slind: "Cold water"**Previous message:**Alan Bundy: "Re: Machine math, clarification"**Reply:**Konrad Slind: "Red Herring?"

Date: Thu, 22 Apr 93 19:02:28 CDT From: Robert S. Boyer <boyer@CLI.COM> Message-id: <9304230002.AA19396@axiom.CLI.COM> To: qed@mcs.anl.gov Subject: Red Herring? Reply-To: boyer@CLI.COM Sender: qed-owner Precedence: bulk

I suspect that Tobias.Nipkow@informatik.tu-muenchen.de may be PRACTICALLY wrong when he says Let me comment on Randy's distinction between Logical Frameworks and PRA/FS0 as a Root Logic because I think it is a red herring. Logical Frameworks are intensionally weak logics (no, you cannot prove the Deduction Theorem in Isabelle's representation of first-order logic). You are not meant to reason in them. They merely provide the infrastructure (eg binding mechanisms) for implementing other logics. If you want to do meta-theory, you first define some appropriate Root Logic RL, eg FS0, and then define your actual logic of interest within RL. My suspicion is grounded in the following belief. I believe that it will be necessary, practically speaking, i.e., from the point of view of both cpu time and disk space, to be able to prove the correctness of algorithms such as simplifiers and decision procedures in the root logic and then to `reflect' those proved algorithms, i.e., having proved them correct to `run' them as very efficiently compiled programs and to trust the results thereby computed precisely as much as if a full Hilbert-Goedel or whatever style proof object had been constructed and checked. I say believe. I have no proof of this belief. But please grant me this belief for the moment. If the verification of algorithms is not possible in the root logic for want of inductive or other logical power, then I don't see how (what a puny claim) reflection could be usefully employed in practice. It wouldn't do one any good that I can see to prove the correctness of some algorithm in some random theory one layer removed because the right to reflect algorithms cannot in general be granted for just any logic represented in the root logic, as far as I can see. (I admit that my vision becomes myopic when I start to think about reflection. It is still terribly worrisome to me that a reflection axiom can sometimes strengthen a logic by the addition of its consistency.) What Tobias claims seems perfectly true to me in principle, just not in practice. Maybe God has enough time and disk space to check his mathematics that way, but I believe we humans will have to boot-strap our way up, USING some of the mathematics we have PROVED within the qed system, to the maximum extent logically imaginable, and that includes verifying code, running it, and trusting the results. Bob P. S. I want to agree with Beeson, Mumford, Thayer and others who bring our sharp attention to the premier questions of which parts of mathematics ought to be treated and how that mathematics should be organized and presented. But granting the priority of those questions to the overall success of the project, and while we think about these most important questions, there is still perhaps some profit in also discussing the framing and plumbing of the system, which maybe no ordinary classical mathematician will ever want or need to see.