From owner-qed Sat Aug 13 17:45:52 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id RAA05265 for qed-out; Sat, 13 Aug 1994 17:45:13 -0500 Received: from cli.com (cli.com [192.31.85.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id RAA05259 for ; Sat, 13 Aug 1994 17:45:08 -0500 Received: from rita (rita.cli.com) by cli.com (4.1/SMI-4.1) id AA15488; Sat, 13 Aug 94 17:44:35 CDT From: boyer@CLI.COM (Robert S. Boyer) Received: by rita (4.1) id AA25833; Sat, 13 Aug 94 17:44:34 CDT Date: Sat, 13 Aug 94 17:44:34 CDT Message-Id: <9408132244.AA25833@rita> To: qed@mcs.anl.gov Subject: Re: set theory Sender: owner-qed@mcs.anl.gov Precedence: bulk John McCarthy replies: I was proposing set theory as an intermediary that would permit a theorem proved in one system to be translated to other systems and used there without being proved again. 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? It is indeed useful to consider the idea that "other systems represent restrictions of set theory to a particular collection of formulas". But how this could be done in a way satisfactory to constructivists, I am not sure. A troublesome aspect is that even axiom-free first order logic uses the law of the excluded middle freely, whereas, as best I understand it, constructivists object to the use of the law of the excluded middle except in contexts in which all predicate and function symbols are recursive, e.g., I believe it is a constructivist theorem that every integer is either a prime or not a prime, because there is an effective check for primality. There are versions of first order logic (such as Kleene's presentation of natural deduction) which make it syntactically easy to tell when a given first order logic proof is constructive (in Kleene's case, never more than one formula on the righthand side of the sequent arrow). So perhaps there is an agreeable universal calculus that is, on the one hand, strong enough to contain first order logic and set theory but which is also, on the other hand, a calculus with a subset of proofs easily recognizable as constructive and strong enough to contain all the work of constructivism. Bob