Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 20 Apr 1993 18:35:57 +0100
Received: by antares.mcs.anl.gov id AA19606 (5.65c/IDA-1.4.4 for qed-outgoing);
          Tue, 20 Apr 1993 12:24:38 -0500
Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP 
          id AA19599 (5.65c/IDA-1.4.4 for <qed@mcs.anl.gov>);
          Tue, 20 Apr 1993 12:24:36 -0500
Received: from malabar.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA00496;
          Tue, 20 Apr 93 13:24:31 -0400
Posted-Date: Tue, 20 Apr 93 13:24:28 -0400
Received: by malabar.mitre.org (5.61/RCF-4C) id AA05106;
          Tue, 20 Apr 93 13:24:28 -0400
Date: Tue, 20 Apr 93 13:24:28 -0400
From: jt@linus.mitre.org
Message-Id: <9304201724.AA05106@malabar.mitre.org>
To: qed@mcs.anl.gov
Subject: illusiions
Sender: qed-owner@mcs.anl.gov
Precedence: bulk



OK, I agree that illusions are "part of the trade." That is not my
objection.  (Although please find a better expression than illusion.)
However, for a non-constructivist analyst such as myself, it seems
very convoluted to encode everything in an unfamiliar and unintuitive
(for me) logic.  What is the point? To facilitate translatability?  I
don't believe that this is possible in any way which I would find
acceptable. For instance, constructivists typically don't accept the
clasical intermediate value theorem for continuous functions. So a
translation of the classical intermediate value theorem will have no
intuitive content at all. 


Javier