[FOM] Formalization Thesis

[giovanni sambin]

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