[FOM] Formalization Thesis

[Timothy Y. Chow]

In 2005, I started a thread entitled "Formal sentences capture informal 
ones" in the USENET newsgroup sci.logic, with the suggestion that the 
following statement, or something like it, should be given a name---e.g.,
"the Formalization Thesis":

   Every theorem of ordinary mathematics is faithfully expressed by a 
   formal theorem of ZFC.

Here, 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.  I am also not focusing on theorems, in 
contradistinction to definitions or conjectures or proofs; indeed, I *do* 
want to include these things, and I chose "theorems" above only because it 
makes for a snappier statement (e.g., the term "formal conjecture of ZFC" 
is not standard, and would require some explanation).  What I am focusing 
on is the notion that formal sentences "correctly capture" statements of 
mathematics that are made informally in natural language.

I use the word "Thesis," as the Formalization Thesis is reminiscent of the 
Church-Turing Thesis, which also equates an informal notion ("effective 
procedure" or "algorithm") with a formal one.  The Formalization Thesis is 
often tacitly invoked in much the same way that the Church-Turing Thesis 
is sometimes invoked.  That is, authors often give informal proofs and 
then make a claim of the form, "It is clear that the above argument can be 
converted into a formal proof in such-and-such a system," relying on the 
reader's "experience" in formalizing informal mathematics to avoid 
explicitly writing down a very long and tedious verification.  Similarly, 
authors often describe algorithms informally, relying on the reader's 
programming experience to avoid writing down a long piece of code in a 
machine-readable programming language.

I advocate giving a *name* to the Formalization Thesis because I believe 
that doing so would be a valuable expository move.  For example, there has 
been some discussion in the literature (e.g., by Detlefsen I think) about 
whether Hilbert's program can still be salvaged in the light of Goedel's 
second theorem.  The debate, as I understand it, centers on a particular 
instance of the Formalization Thesis, namely whether the formal sentence 
Con(PA) (in any one of its usual incarnations) correctly captures the 
meaning of the statement "PA is consistent."  Giving the Formalization 
Thesis a name seems to me to allow the arguments on both sides of this 
debate to be formulated with greater succinctness and clarity than is 
currently the case.

I also think that giving the Formalization Thesis a name would have helped 
me when first studying Kunen's set theory textbook, especially when I was 
trying to understand what he meant by a "reasonable" representing formula 
and when I was studying the proof of the reflection theorem for ZFC.

In the aforementioned sci.logic thread, Torkel Franzen and Aatu 
Koskensilta raised some objections.  Rereading the discussion now, I 
confess that I still do not fully understand the objection, but it is 
something to the effect that the Formalization Thesis as I stated it was 
not sufficiently precise to be of any value.  I would therefore like to 
ask FOM readers:

(1) Is the Formalization Thesis, as I've formulated it, approximately as 
precise as the Church-Turing Thesis?  If not, can the precision problem be 
fixed easily with a simple rewording?

(2) Assuming that the answer to (1) is yes, does it seem useful, from a 
pedagogical and expository point of view, to give the Formalization Thesis 
a name?

Tim