# [FOM] Formalization Thesis

giovanni sambin sambin at math.unipd.it
Fri Jan 4 09:30:42 EST 2008

At 19:42 -0500 3-01-2008, joeshipman at aol.com wrote:
>I repeat my earlier challenge: can anyone who disputes Chow's
>Formalization Thesis respond with a SPECIFIC MATHEMATICAL STATEMENT
>which they are willing to claim is not, despite its expressiblity in
>English text on the FOM discussion forum, "faithfully representable" or
>"adequately expressible" as a sentence in the formal system ZFC?
>
>I don't want an argument that such a statement exists, and I don't want
>a METAmathematical statement, I want an actual English sentence within
>quotation marks that is claimed to be mathematical but not formalizable
>in Chow's sense.
>
>>-- JS

Simply  ALL statements of any constructive approach to mathematics
cannot be formalized in ZFC, because of its underlying classical
logic. Even if their expression looks the same, their meaning is
different.

The often silent assumption that mathematics must be only the
classical one amounts almost to begging the question: isn't classical
mathematics exactly what can be formalized in ZFC? How can we
characterize classical mathematics otherwise? We need to have
classical logic, but we also need to have sets, and moreover they
must be closed under powerset, union, pair, etc. What is the
difference between ZFC and this "informal" mathematics?

Granting that also constructive approaches are part of mathematics
provides with an endless number of examples of statements not
formalizable in ZFC. Changing ZFC to IZF shows that one needs at
least TWO formal systems. And in any case one has the same problem
with IZF, since there are constructive foundations (like topos
theory, type theory, or predicative set theories) which are not
properly expressed by IZF.

Interesting specific examples include all foundational principles
which are debated among constructivists, like FT (=Fan Theorem), Bar
Induction, internal Church Thesis, Axiom of Choice,... But also, I
repeat, any statement of constructive mathematics, like "any
continuous real valued function which is negative in a and positive
in b has a zero between a and b". Their expression in ZFC simply is
*not* what one means it to be constructively.

In conclusion, and shortly: perhaps the thesis that math can be
formalized in ZFC applies to classical set theory, but 1. this is
certainly not all of mathematics and in any case 2.  one has to
specify what classical set theory is.

Best wishes for 2008!

Giovanni Sambin