the base logic
Pat Lincoln <lincoln@csl.sri.com>
Date: Tue, 13 Apr 93 19:36:19 -0700
From: Pat Lincoln <lincoln@csl.sri.com>
Message-id: <9304140236.AA08110@xenon.csl.sri.com>
To: qed@mcs.anl.gov
In-reply-to: David McAllester's message of Tue, 13 Apr 93 15:14:54 EDT <9304131914.AA00347@spock>
Subject: the base logic
Sender: qed-owner
Precedence: bulk
> From: dam@ai.mit.edu (David McAllester)
> ...I am confident that I could write
> a simple routine that would translate definitions and theorems from any
> of these languages into Ontic.
> ...Also, the ability
> to translate between foundational languages could bypass the need for
> a single base logic.
Something that should be considered with regard to this approach is
the difficulty of translating proofs between dissimilar systems.
Difficult theorems and their proofs in some theory could be encoded so
that "THEOREM is proved by PROOF in THEORY" is a (relatively) easily
checked theorem of the base logic of QED, as the manifesto suggests
for nonconstructive set theory. This `one level removed' approach
does move the problem of translation between systems into a more
formal arena, but it doesn't really finesse the problem of translating
proofs since it requires writing a proof checker for each theory in
QED. It also suggests a paradigm of interaction where one proves
their theorems in Ontic, PVS, Otter, BMTP, etc, in the usual way, and
then translates the completed proof, theorem, and theory into QED for
a kind of validation. Some social process must check the translation
as well as the QED proof checker. Such a use of QED makes the choice
of base logic less important since end users never need peek under the
hood of their axiom system (at the translation of those axioms into
QED base logic). However, this approach seems less exciting than what
the Manifesto describes, and is not as bootstrappable as the direct
method David suggests.
Patrick Lincoln