Root Logics

• Mail folder: QED
• Next message: Alan Bundy: "Re: Machine math, clarification"
• Previous message: beeson@cats.UCSC.EDU: "Re: Root Logics"
• In-reply-to: Randy Pollack: "Root Logics"

From: Tobias.Nipkow@informatik.tu-muenchen.de
To: qed@mcs.anl.gov
In-reply-to: Randy Pollack's message of Thu, 22 Apr 1993 17:13:21 +0200 <11595.9304221513@whalsay.dcs.ed.ac.uk>
Subject: Root Logics
Message-id: <93Apr22.183218met_dst.8079@sunbroy14.informatik.tu-muenchen.de>
Date: 	Thu, 22 Apr 1993 18:32:07 +0200
Sender: qed-owner
Precedence: bulk

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.

So the question is: should a project like QED implement the Root Logic
directly or should it use Logical Frameworks technology? Given the scale of
the envisaged effort, QED would probably need to be built from scratch,
probably using ideas from Logical Frameworks. More modest systems like HOL
can and have been implemented in Isabelle with only a small loss in
functionality and efficiency.

Of course none of this answers the real question as to what the Root Logic
should be.

Tobias