Delivery-Date: 
To: qed@mcs.anl.gov
Subject: Re: illusion
In-Reply-To: Your message of Tue, 20 Apr 93 12:03:43 -0400. <9304201603.AA05059@malabar.mitre.org>
Date: Tue, 20 Apr 93 17:43:33 +0100
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:097400:930420164359"@cl.cam.ac.uk>
Sender: qed-owner@mcs.anl.gov
Precedence: bulk


When I remarked "Isabelle supports the illusion that you are working directly
in the formalized logic", I meant that users could work without knowing how
their object-logic was encoded in Isabelle's meta-logic.  The illusion is
maintained through many mechanisms, e.g. the parser/prettyprinter translates
the internal encodings into a readable notation.

The encodings are rather straightforward.  They resemble the ones Church used
to encode higher-order logic into the typed lambda calculus.  Church's
encodings are now generally accepted as the very definition of higher-order
logic.

It may seem dangerous to speak of illusions when we are after certainty; a
fault in the parser/prettyprinter could be nearly as harmful as a fault in the
inference mechanisms themselves.  But illusions are a tool of our trade. 
Inside the computer there is nothing but bit patterns.  Every theorem prover
encodes its logic ultimately in terms of bits.  Even programmers rely upon the
illusion that terms and formulae are present.

							Larry Paulson