[FOM] Formalization Thesis: A second attempt
Vladimir Sazonov
vladimir.sazonov at yahoo.com
Sun May 30 19:23:45 EDT 2010
----- 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
More information about the FOM
mailing list