From owner-qed Sat Aug 13 18:02:18 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id SAA05463 for qed-out; Sat, 13 Aug 1994 18:01:52 -0500
Received: from SAIL.Stanford.EDU (SAIL.Stanford.EDU [36.28.0.130]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id SAA05458 for <qed@mcs.anl.gov>; Sat, 13 Aug 1994 18:01:47 -0500
Received:  by SAIL.Stanford.EDU (5.57/25-eef) id AA07521; Sat, 13 Aug 94 16:01:43 -0700
Date: Sat, 13 Aug 94 16:01:43 -0700
From: John McCarthy <jmc@sail.Stanford.EDU>
Message-Id: <9408132301.AA07521@SAIL.Stanford.EDU>
To: boyer@CLI.COM
Cc: qed@mcs.anl.gov
In-Reply-To: <9408132244.AA25833@rita> (boyer@cli.com)
Subject: Re: set theory
Reply-To: jmc@cs.stanford.edu
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

Bob Boyer worries:

     I hope I am not being utterly naive in replying that the
     problem I see is that once one records a result as theorem
     of set theory, it loses its significance to constructivists.
     Who knows, they might ask, what troublesome aspects of set
     theory, such as the power set axiom or the law of the
     excluded middle, was used in support of such a result, given
     merely that it is a theorem of set theory?

1. If the result came originally from a "constructively correct"
theory, then going through set theory shouldn't harm it.

2. If the result was derived in set theory and people are motivated to
take the trouble, they can label the result with what was used in
deriving it.

3. Actually, for AI reasons, I don't give much weight to constructive
correctness.

4. Is there another proposal for an intermediate language?