Delivery-Date: 
To: Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>
Cc: qed@mcs.anl.gov
Subject: Re: Boyer's Hypothesis
In-Reply-To: Your message of Mon, 26 Apr 93 11:47:31 +1000. <0fqnwnqKmlE2MUS1dr@arp>
Date: Mon, 26 Apr 93 04:01:25 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:074970:930426030144"@cl.cam.ac.uk>
Sender: qed-owner@mcs.anl.gov
Precedence: bulk


Zdzislaw Meglicki writes (re. Analytica):

> What QED could add to a system like that would be a sound logical
> foundation. I.e., every one of the facts stored in its equally
> formidable data base would itself be a theorem with an accompanying
> proof. Although the proofs should not go all the way down to the
> underlying logic - rather, they should try to reduce problems to already
> proven theorems, the way it is done in man-made mathematics - by
> combining proofs of theorems on lower levels it should ultimately be
> possible to reconstruct mechanically the whole proof tree with its
> leaves at the level of the basic logic (although I am not sure why
> anybody would ever want to do that - apart from just demonstrating that
> it can be done).

I don't question that it will be necessary to organize the system
hierarchically. However it may be inevitable that theorems become
more complicated when stated rigorously. If you think sufficiently
precisely about some mathematical concepts there can be layers of
detail that are very difficult to hide. (The status of partial functions
applied to terms outside their domains is a particularly interesting
example, I think.)

John Harrison (jrh@cl.cam.ac.uk).