[FOM] Formalization Thesis

[Timothy Y. Chow]

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