[FOM] Formalization Thesis
Timothy Y. Chow
tchow at alum.mit.edu
Sun Dec 30 15:10:46 EST 2007
I've been trying to make sense of the objections that have been posed to
the Formalization Thesis so far. There is one strand of argument that
seems to run through several of the responses, which I will call the
"Inexhaustibility Objection." Roughly speaking, the Inexhaustibility
Objection runs as follows:
"For the Formalization Thesis to be at all interesting, you must fix some
particular formal system. But whatever formal system you choose, it is
straightforward to write down truths that are not provable in that system.
For example, if you pick ZFC, then we could pick Con(ZFC) or any number of
more mathematically interesting statements. In addition, if you pick ZFC,
then you commit yourself to translating all mathematics into set theory,
and the process of doing so will inevitably add or subtract some
conceptual content. Mathematics is inexhaustible both in the sense that
its truths are not computably enumerable, and in the sense that people
come up with completely new concepts all the time. Therefore there is no
reason to believe in the Formalization Thesis."
My response to the Inexhaustibility Objection is as follows: The objection
is a reasonable one, but only when directed towards a much stronger
version of the Formalization Thesis than I intended to assert. At the
risk of complicating the discussion even further, let me formulate yet
another version of the Formalization Thesis that I hope will make it
clearer what I am trying to get at:
Formalization Thesis, "Mizar version": The correctness of anybody's claim
to have proven such-and-such a theorem of ordinary mathematics can be
checked by Mizar.
I haven't actually gotten my hands dirty working with Mizar myself, but as
I understand it, it's based on ZFC. Even if I'm mistaken on this point,
let's assume it for the sake of argument.
So how do I defend the Mizar version against the counterexamples involving
theorems that go beyond ZFC? My response is that if there's some theorem
T that requires an additional axiom A beyond ZFC, then it's true that
Mizar can't check it "directly," but Mizar *can* check "if A then T." So
for example Mizar can't check that the continuum hypothesis is independent
of ZFC, but it *can* check that if ZFC is consistent then CH is
independent. I believe that this is a reasonable way to understand what
it means for Mizar to "check the correctness" of theorems of ordinary
mathematics that go beyond ZFC, because typically when people go beyond
ZFC, they make it clear what additional axioms they are assuming.
In this way I am able to handle any straightforward extension of ZFC. I
still can't handle *all truths* of set theory, but then again nobody ever
writes down *all truths* and triumphantly proclaims "Theorem." "All
truths" goes beyond not only ZFC but also beyond all ordinary mathematics
as actually practiced, and hence does not invalidate the Formalization
Thesis.
But what about the alleged conceptual gains and losses when one attempts
to translate arbitrary mathematics into set theory? Here is where the
Mizar version should help clarify my intent. I'm not so concerned with
whether any of the standard dodges for formalizing classes or ordered
pairs or whatnot are "perfect" conceptual translations, *as long as* the
translation is good enough for *checking correctness*. If someone claims
to have proved a theorem about the class of all topoi, then I'm not going
to worry about whether my Mizar-version of the theorem captures every
shade of meaning of the concept "the class of all topoi," as long as the
translation is good enough for people to accept the Mizar-verification as
a definitive verification of the correctness of the original proof (modulo
hardware and software errors).
I hope that this clarifies the statement I intended to make when I
formulated the Formalization Thesis. The Mizar version seems to me to be
a pretty clear and also a pretty weak form of the Thesis, but it is still
not trivial. Someone could still give an example of a theorem whose proof
is accepted as correct, but for which there exists no version that Mizar
can sink its teeth into in order to verify the correctness of the proof.
This is a definite possibility, but can anyone cite an explicit example?
Tim
More information about the FOM
mailing list