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?