>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.