[FOM] Formalization Thesis
joeshipman at aol.com
Fri Dec 28 19:27:40 EST 2007
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
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).
More new features than ever. Check out the new AOL Mail ! -
More information about the FOM