Delivery-Date: 
From: dam@edu.mit.ai (David McAllester)
Date: Sun, 18 Apr 93 18:34:15 EDT
Message-Id: <9304182234.AA00906@spock>
To: boyer@com.cli
Cc: qed@gov.anl.mcs
In-Reply-To: Robert S. Boyer's message of Sun, 18 Apr 93 12:36:45 CDT <9304181736.AA13372@axiom.CLI.COM>
Subject: Answer to a question, and further speculation on a QED foundation
Sender: qed-owner@gov.anl.mcs
Precedence: bulk

Although I am sympathetic to the idea that we can all accept primitive
recursive arithmetic (PRA) I am little troubled by using it as the
foundation of QED.  Consider the mean value theorem (MVT) of calculus.
I agree that this thoerem can be encoded as "P is a proof in ZFC of
ZFC-MVT" where ZFC-MVT is some formal statement of the mean value
theorem in the langauge of set theory.  I am concerned about the
difficulty of using this entry in the QED library.  It seems
"encrypted". I need to talk to its author and have them explain how
they represent formulas as numbers.  Although I can imagine "plain
text" annotations and translation algorithms entered in the QED
library, it seems like a lot of extra work.

Perhaps there is a compromise position.  We could agree on a language
without agreeing on an inference system.  For example, we could agree
to use the language of set theory (perhaps annotated with some
standard syntactic sugar like tuples, structures and
lambda-expressions).  We could have a long list of axioms and
inference principles not all of which are accepted by all players.
Each "theorem" could be annotated with the axioms and principles
needed to prove it.  This annotation could, of course, be derived
automatically from a given proof.  This allows "skeptical players" but
avoids the use of metatheorems.  I would think that PRA corresponds
to a very restricted set of set theoretic inference principles.

	David