[FOM] Formalization Thesis

[catarina dutilh]

I guess the issue is that the Formalization Thesis as you stated it conflates two different claims, which I think are best stated separately:
 
 
Expressibility Thesis (ET): Every theorem of ordinary mathematics is faithfully expressed in the language of ZFC (or the appropriate formal language).
 
Provability Thesis (PT): If ET obtains, then the expression of every theorem of ordinary mathematics in the language of ZFC is also a theorem of ZFC.
 
 
So the problem is not so much with the phrase 'faithfully expresses', but what it means for this relation of faithful expression to obtain. I am not saying that this cannot happen, in fact I agree that it often seems to happen, in the sense that there is wide agreement in the scientific community to the effect, for example, that the formal sentence "Con(PA)" adequately expresses the consistency of PA (and this holds of many other mathematical statements). But this is not a formal issue, it is a conceptual issue; the verification of ET would require that the translation of every theorem of ordinary mathematics into a formal language must be performed on a one-by-one basis. Also, I suspect that this is not an objective matter: there would probably be disagreement as to whether statement T' in the language of ZFC (or other) is or is not a faithful translation of theorem T of ordinary mathematics.
 
Once ET is verified (*if* it can be done), then PT is indeed a formal issue, namely whether the faithful expression of a given theorem T in the formal language can also be derived within the appropriate formal theory (i.e. from its axioms by applications of its rules of inference). But expressibility and provability are two different issues, and as I said, the expressibility side of the issue seems to be the real challenge.

Another issue is whether the *proofs* of those theorems in ordinary mathematics can be given an equivalent formulation in the formal theory, and in particular whether all the inferential moves allowed in ordinary mathematics have a counterpart in the inferential moves allowed in the formal theory. Clearly, equivalence of proofs would be a much stronger requirement, and my guess is that any experienced logician can give counterexamples to this equivalence, i.e. proofs that are valid within ordinary mathematics but which do not correspond to valid proofs in the formal language, even assuming that ET and PT hold of the theorems in question.
 
best
 
Catarina
 


----- Original Message ----
From: Timothy Y. Chow <tchow at alum.mit.edu>
To: fom at cs.nyu.edu
Sent: Thursday, December 27, 2007 11:01:25 PM
Subject: Re: [FOM] Formalization Thesis

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
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom


      ____________________________________________________________________________________
Never miss a thing.  Make Yahoo your home page. 
http://www.yahoo.com/r/hs