[FOM] Formalization Thesis
Timothy Y. Chow
tchow at alum.mit.edu
Wed Dec 26 12:40:44 EST 2007
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
More information about the FOM