Delivery-Date: 
From: dam@ai.mit.edu (David McAllester)
Date: Tue, 20 Apr 93 11:04:50 EDT
Message-Id: <9304201504.AA01103@spock>
To: Larry.Paulson@cl.cam.ac.uk
Cc: qed@mcs.anl.gov
In-Reply-To: Lawrence C Paulson's message of Mon, 19 Apr 93 17:57:03 +0100 <"swan.cl.ca.644:19.04.93.16.57.14"@cl.cam.ac.uk>
Subject: Different Schools
Sender: qed-owner@mcs.anl.gov
Precedence: bulk


   Mathematics done in simple base logics is not encrypted at all.  Isabelle
   supports the illusion that you are working directly in the formalized logic ...

ok, I believe this.  I had not thought to use a metasystem such as Isabelle
as the base logic. (Is "metasystem" an acceptable term for Isabelle?)

   There is a problem, though: ... If we are to support several different schools
   of mathematics, then there is the risk that the database will contain many
   duplicated proofs.

I will stop using the term "encrypted" and simply note that if the
data base uses different languages from different schools then we may
end up writing lots of translators.  This is true even if each school
defines their logic in the same simple base logic (metasystem).  A many
language approach might be ok.  However there is the problem of
confidence (we must trust the methods of the different schools) and
the problem of intertranslation.  It seems that the use of a base
logic as a metasystem does not avoid these problems.

It seems to me that there is still a case for defining a highly
expressive lingua franca.  As I noted earlier, a lingua franca, such
as the language of set theory, need make no commitment to any
particular set of inference principles.  The lingua franca could be
neutral as to whether reasoning should be constructive.

	David