Red Herring?

• 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.