[FOM] Formalization Thesis: A second attempt

[Vladimir Sazonov]

----- Original Message ----
> From: Timothy Y. Chow <tchow at alum.mit.edu>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Sent: Sun, May 30, 2010 3:23:47 AM
> Subject: Re: [FOM] Formalization Thesis: A second attempt
> 
> On Thu, 27 May 2010, Vladimir Sazonov wrote:
> > Here I am in a shock since such restricting mathematics to ZFC 
............


Let 
> me once again draw your attention back to one of my main motivating 
> applications, namely explaining why Goedel's 2nd theorem is relevant to 
> Hilbert's program of proving the consistency of mathematics.  It is 
> widely believed that Hilbert's program is essentially hopeless, because of 
> Goedel's 2nd theorem.  Do you share this point of view?  



Yes, of course, if mathematics is identified with, say, ZFC 
(with which I do not agree!). 


However, strictly speaking, I would not consider Goedel's 2nd theorem 
as sufficiently adequate. It quantifies over "all" finite proofs 
with "finite" understood in too wide sense. Let me recall that 
I (as all working mathematicians) consider as mathematical only 
proofs of feasible length (which can be submitted to a journal). 
In this sense this result of Goedel is not about unprovability 
of consistency in the proper sense. This is about existence/non-existence 
of imaginary proofs, not about real (feasible) proofs. 

Anyway, I consider Hilbert's program of proving the consistency 
of mathematics by weak means as something unrealistic. 


If 
> mathematics is as open-ended as you seem to be arguing, then isn't Hilbert's 
> program still wide open?  


Not just wide open, but hardly meaningful at all. Mathematics could be 
not just open-ended but rather "branching"... Anyway mathematics is not 
a science about some unique class of imaginary objects (sets or whatever else). 
I see it as a kind of engineering which creates formal tools for thought 
potentially applicable to any kind of objects (either imaginary or real). 
Can we meaningfully ask whether engineering (of any kind) is consistent? 


Tomorrow someone may complete Hilbert's 
> program by publishing a perfectly acceptable mathematical proof that 
> mathematics is consistent.  The proof will presumably not be 
> formalizable in ZFC, but so what?


It is already done in appropriate extensions of ZFC, like ZFC proves 
consistency of PA or like induction up to epsilon_0 allows to 
prove consistency of PA. New proofs of consistency of ZFC could 
probably be quite interesting. However, (i) I do not think such a proof 
will increase my belief in the consistency of ZFC and (ii) this is 
somewhat outside of my immediate interests. 


Best regards, 

Vladimir