Delivery-Date: 
To: qed@mcs.anl.gov
Subject: little theories and encryption
Date: Mon, 19 Apr 93 17:57:03 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.ca.644:19.04.93.16.57.14"@cl.cam.ac.uk>
Sender: qed-owner@mcs.anl.gov
Precedence: bulk


Without doubt we should attempt to include constructivists and other
philosophies of mathematics, and this does mean that the base logic will have
to be pretty simple.  PRA is possibly too simple -- I would hate to give up
quantifiers.  Isabelle uses intuitionistic higher-order logic (with implies,
forall and equality).  This could be further weakened to be essentially
first-order, but admitting bound function variables in order to handle axiom
schemes and descriptions.  The AUTOMATH-style type theories that are being
studied at the moment also deserve serious consideration.

Mathematics done in simple base logics is not encrypted at all.  Isabelle
supports the illusion that you are working directly in the formalized logic,
be it ZF, HOL, Constructive Type Theory or what have you.  AUTOMATH type
theories also support a natural proof style.

There is a problem, though: many proofs are essentially the same no matter
what sort of framework (constructive, classical, ...) that you are working in.
If we are to support several different schools of mathematics, then there is
the risk that the database will contain many duplicated proofs.  This
certainly happens with Isabelle.  Perhaps 'little theories' could prevent
this; each theorem would be proved in the weakest framework possible for that
particular theorem.  

We need a combination of 'little theories' and a fairly weak base logic,
though perhaps stronger than PRA.  Much work needs to be done towards relating
proofs done in different formal systems.

							Larry Paulson