From lusk Wed Jun 8 03:38:14 1994 Received: from sphinx.nmt.edu (sphinx.nmt.edu [129.138.6.92]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id DAA21227 for ; Wed, 8 Jun 1994 03:36:26 -0500 Received: (from yodaiken@localhost) by sphinx.nmt.edu (8.6.8.1/8.6.6) id CAA25809; Wed, 8 Jun 1994 02:36:49 -0600 Message-Id: <199406080836.CAA25809@sphinx.nmt.edu> From: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Date: Wed, 8 Jun 1994 02:36:49 -0600 In-Reply-To: kunen@cs.wisc.edu (Ken Kunen) "formalizing mathematics" (Jun 7, 8:31am) reply-to: yodaiken@nmt.edu X-Mailer: Mail User's Shell (7.2.5 10/14/92) To: kunen@cs.wisc.edu (Ken Kunen), qed@mcs.anl.gov Subject: Re: formalizing mathematics On Jun 7, 8:31am, Ken Kunen wrote: Subject: formalizing mathematics >You can't really modularize mathematics, as Victor Yodaiken seems to suggest: >>> Why not mechanize algebra, rather than logic or set theory? > >If you want to verify a large chunk of mathematics, not just an >isolated result here and there, you need to formalize something like ZFC. At the risk of making my own ignorance even more painfully clear, I have to admit that I don't see why this must be true. >But to verify many of the standard results in real analysis, for >example, we have to be able to talk about real numbers, and sets of real >numbers, and sequences of real numbers, and functions on the real numbers..... >So, we need a theory strong enough to construct these objects. It appears to me that your argument can be correct only if there is some essential difference between the symbolic integration of a formula (something that Mathematica/Maple etc. do routinely without an underlying formalization) and the symbolic verification of a formula. Is that correct? If so, what is the difference? >That is one advantage of set theory. We can start with simple >basic principles, and any "untidy mix" of functions, sequences, numbers, >pairs, etc., can all be constructed within the theory, as needed. In this case, what do I gain by actually going through with the construction, let alone embedding it into a theorem prover? If the purpose of QED is to prove interesting mathematical theorems, rather than to verify that mathematics can be constructed from ZFC or PRA or whatever, then why not bypass foundations altogether? This is not a rhetorical question. It is impractical to insists that the theorem prover will prove, say, the Krohn-Rhodes theorem by invoking the formalization of simple groups from sets. One supposes that the proof will rely on a large database of established lemmas and proof methods. Outside of metamathematics, these lemmas and proof methods are not in question. So why must they be derived from basic principles for our theorem prover?