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 ; 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 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?