[FOM] Formalization Thesis

[joeshipman@aol.com]

Despite the quibbling over words, I think I understand what Chow meant 
by his "Formalization Thesis".  I would express his thesis as follows:

"Any interesting mathematical statement X can be adequately represented 
by a statement Y in the language of set theory (or class theory)".

ZFC does not need to enter into it at this stage, since we are talking 
about what can be expressed not what can be proved -- however, a 
possible interpretation of "adequately" above is that a ZFC-proof of Y 
would be acceptable to most mathematicians as also being a "proof of X".

The representing statement may be inelegant or may involve arbitrary 
conventions (such as the Kuratowski ordered pair or the Von Neumann 
representation of integers as ordinals), so that it may be inferior in 
certain senses to the original mathematical statement; Chow's word 
"faithfully" is, I think, intended to connote what it does in the 
context of group representations, namely "without losing any essential 
structure" -- ADDING structure in order to accomplish the formalization 
is OK.

I believe that this version is sharp enough that those who disagree 
with it need to back up their disagreement with a counterexample, that 
is, a statement X which is indisputably mathematical (not 
metamathematical) but which they do not think can be adequately 
represented by any set-theoretical (or class-theoretical) statement Y. 
Chow can then defend his thesis by proposing such a Y, and we can then 
discuss whether Y adequately represents X.

I believe that my own proposed interpretation of "adequately" works 
well, but I want to distinguish between the notions of formalization of 
a statement and formalization of a proof. One reason for this is that I 
have proposed, on this forum, a stronger thesis, which refers to proofs 
and not just to formalizations. I called it "Zermelo's thesis", and 
would state it approximately as follows:

Any mathematical argument acceptable as a valid proof to the community 
of mathematicians is capable of being formalized in ZFC (augmented, in 
rare cases, by large cardinal axioms).

"Zermelo's thesis" resembles Church's thesis from the theory of 
computation; however the evidence is stronger for Church's thesis, 
because we have plenty of effective tools for reducing informally 
specified algorithms to Turing machine code, while "proof assistant" or 
"mathematician's helper" projects are still a long way from comparable 
usefulness. (I distinguish here between "Church's Thesis", formalizing 
the informal notion of algorithm, and the "Church-Turing Hypothesis" 
formalizing what is "computable" by real physical systems -- the latter 
is an assertion about physics which is potentially falsifiable).

-- JS
________________________________________________________________________
More new features than ever.  Check out the new AOL Mail ! - 
http://webmail.aol.com