From owner-qed Sat Aug 13 09:36:55 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id JAA29285 for qed-out; Sat, 13 Aug 1994 09:34:37 -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 JAA29279 for ; Sat, 13 Aug 1994 09:34:29 -0500 Received: from rita (rita.cli.com) by cli.com (4.1/SMI-4.1) id AA15180; Sat, 13 Aug 94 09:33:56 CDT From: boyer@CLI.COM (Robert S. Boyer) Received: by rita (4.1) id AA25801; Sat, 13 Aug 94 09:33:56 CDT Date: Sat, 13 Aug 94 09:33:56 CDT Message-Id: <9408131433.AA25801@rita> To: qed@mcs.anl.gov Subject: set theory Sender: owner-qed@mcs.anl.gov Precedence: bulk John McCarthy writes: I suspect that set theory can serve as a universal language. While I believe that proposition is true in a technical sense, I think it is false in a more important logistical sense. I believe that a substantial percentage, maybe even a majority, of the people who are interested in mechanical proof checking are of a rather constructivist bent, with marginal interest in a set theory based results. Consider, for example, the large group of proof checkers that are based upon the de Bruijn and Martin-Lof style of logics. I think I can count at least six major, on going, multi-person-year efforts with such a footing. I suspect that this may be larger than the number of on going set theory based projects. The decision to study these logics is often not a decision taken likely, but rather is often based upon philosophical convictions, including doubts about set theory. So I think a decision to use set theory as the foundation to be a poor logistical decision because it leaves so many likely participants "out". I believe that that a very high percentage of practically important mathematics, including essentially all that is need for proof theory (metamathematics Hilbert-Bernays style) and practical computer science, can be checked in a system or systems much weaker than set theory. One does not need set theory, for example, to support McCarthy's mathematical theory of computation, ("A Basis for a Mathematical Theory of Computation", in Computer Programming and Formal Systems, eds. P. Braffort and D. Hershberg, North-Holland, 1963). And I hope that we may be able to agree on some weaker systems whose proof-checked results almost the whole community is willing to depend upon. In fact, I have read, the work in "reverse mathematics" of the last several decades suggests that almost all of the mathematics used in engineering can be done in logics much weaker than set theory. Certainly, a set theory checker will be an important component of a mechanically proof-checked encyclopedia of mathematics because set theory is the universal carrier of the bulk of modern mathematics, a vehicle gladly, if informally, used by almost all practicing mathematicians. It may even be that almost all of the entries in such an encyclopedia will be set theory based, in the absence of any other framework for the whole of contemporary mathematics. But that doesn't mean that set theory should be the foundation. Apologies to those to whom I am repeating myself, Bob