[FOM] Formalization Thesis

[Timothy Y. Chow]

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 
>sufficiently precise.

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 
question.

Does this clarify what I intend by "expressing faithfully"?  How would you 
phrase it better?

Tim