[FOM] Formalization Thesis: A second attempt

[Timothy Y. Chow]

Back in December 2007, I proposed something that I called the 
"Formalization Thesis" that generated a lot of discussion.

http://cs.nyu.edu/pipermail/fom/2007-December/012371.html

Looking back at it now, I see that my initial attempt to state the Thesis 
was poorly worded, causing a lot of people to misunderstand it.  A recent 
discussion on MathOverflow.net (drawn to my attention by Olivier Gerard's 
FOM post on April 27) has persuaded me once again of the value of giving a 
name to this Thesis.

http://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent/24919#24919

With the benefit of the feedback from the first FOM discussion, let me now 
propose what I think is a better statement of the Formalization Thesis:

  Given any precise mathematical statement, one can exhibit a formal 
  sentence S in the first-order language of set theory with the property 
  that any mathematically acceptable proof of the original mathematical 
  statement can be mimicked to produce a formal proof of S from the axioms 
  of ZFC.

As I said in my original FOM post, my focus is not so much on ZFC 
particularly; that is, I will not quibble with someone who wishes to 
replace "ZFC" with another system that is somewhat weaker or stronger.

As you can see, I have avoided the problematic term "faithfully expressed" 
that generated so many objections previously.  My question now is, does 
anybody here disagree with the Formalization Thesis as stated above?  For 
those who agree with the Thesis itself, do you agree with me that giving 
the Formalization Thesis a name would help clarify discussions of the sort 
taking place on MathOverflow?

Tim