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?