[FOM] Formalization Thesis
Timothy Y. Chow
tchow at alum.mit.edu
Thu Dec 27 17:01:25 EST 2007
Catarina Dutilh wrote:
>So, unless one can make sense of the idea of 'expressing faithfully' in a
>precise way, the Formalization Thesis thus stated does not seem to be
Well, can you tweak it to *make* it "sufficiently precise"?
Let me give some examples of what I mean by "expressing faithfully."
Consider the independence of the continuum hypothesis. Goedel proved that
if ZFC is consistent, then ZFC does not prove ~CH. Cohen proved that if
ZFC is consistent, then ZFC does not prove CH. These results have been
widely interpreted as demonstrating that the continuum hypothesis cannot
be settled by currently accepted "ordinary mathematics."
However, for us to interpret the Goedel/Cohen results in that way, we must
make the tacit assumption that the formal sentence "CH" faithfully
expresses the continuum hypothesis, or at least expresses it well enough
for us to believe that any ordinary mathematical proof of the continuum
hypothesis (or its negation) could be transformed into a formal proof of
CH (or ~CH) from the axioms of ZFC.
Similarly, Goedel's second incompleteness theorem is widely regarded as
having killed Hilbert's program, but this belief relies on the tacit
assumption that the formal sentence "Con(PA)" adequately expresses the
consistency of PA.
Also the projects to produce machine-checkable proofs of famous theorems
(Avigad's proof of the prime number theorem, Hales's Flyspeck project,
etc.) all tacitly assume that the formal theorem that the computer is
checking is an accurate representation of the informal theorem in
Does this clarify what I intend by "expressing faithfully"? How would you
phrase it better?
More information about the FOM