From lusk Wed Jun 1 05:33:17 1994 Received: from sphinx.nmt.edu (sphinx.nmt.edu [129.138.6.92]) by antares10.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id FAA11447 for ; Wed, 1 Jun 1994 05:30:40 -0500 Received: (from yodaiken@localhost) by sphinx.nmt.edu (8.6.8.1/8.6.6) id EAA07799; Wed, 1 Jun 1994 04:30:54 -0600 Message-Id: <199406011030.EAA07799@sphinx.nmt.edu> From: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Date: Wed, 1 Jun 1994 04:30:54 -0600 In-Reply-To: pjr@cs.uq.oz.au "Qu-Prolog 3.2 and Ergo 4.0" (Dec 20, 7:35am) reply-to: yodaiken@nmt.edu X-Mailer: Mail User's Shell (7.2.5 10/14/92) To: pjr@cs.uq.oz.au, qed@mcs.anl.gov Subject: Re: Qu-Prolog 3.2 and Ergo 4.0 On May 25, 5:46pm, Randall Holmes wrote: Subject: Re: Notes >If a single object language were wanted, I would suggest constructive >type theory, with a "filter" (the double negation interpretation) >provided so that it would look like classical type theory, which is >not far from standard mathematical practice. > >Another candidate for an object language: Mac Lane set theory (Z with >delta-zero comprehension (all quantifiers bounded) -- equivalent to >ZFC with all quantifiers bounded in comprehension and replacement. >equivalent in strength to the theory of types and adequate for >classical math short of higher set theory). Constructive Mac Lane set >theory with filter? Why? It is my impression that our goal is not to settle questions about the foundations of mathematics, but to mechanize some significant part of "working" mathematics. I'm perfectly willing to accept that standard mathematical practice is sound. It follows that I have no need to adopt the program of foundational mathematics. Why not mechanize algebra, rather than logic or set theory? Here, we have a model in the symbolic algebra programs such as Mathematica and Axiom. In fact, it would be useful to build a theorem prover that would add "deduction" to the capabilities of an existing theorem prover. Ed Clarke and his students have done some work in this direction. Proposition: The purpose of the QED project is to mechanize the algebra of proofs in working mathematics. For this purpose, the language of ordinary mathematics suffices and there is no need to adopt any meta-mathematical framework. Perhaps someone with a less limited understanding than my own can explain why this proposition is incorrect. Philosophical aside. The idea that one can and should develop a mathematical system from a small set of axioms and deduction rules in place of an untidy mix of principles derived from physics and arithmetic is not necessarily a correct idea.