[FOM] Formalization Thesis

[Andrej Bauer]

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?

And I suppose you are not willing to accept statements in non-classical
mathematics that directly contradict ZFC? Such a statement S has to be
translated indirectly as "ZFC contains a model in which S is valid". But
is that a _faithful_ translation of the mathematical content?

Examples:
1. All real functions are continuous.
2. The set {0} is not equal to the set {x : R | x * x = 0}.
3. There are countably many countable subsets of N.

A mathematician can never truly appreciate the mathematical content of
such statements by always looking at them through ZFC. You really need
to let go of models in order to feel the Power of the Dark Side.

And just a quick comment: Timothy picked ZFC as an example. People who
actually work on formalization know that having powerful type-theoretic
infrastructure is absolutely necessary to keep things organized (imagine
having 3000 lemmas...). So they use type theory instead. For example,
pairs are typically a primitive notion, because that is just more
convenient. Because most modern proof asistants (Coq, Isabelle) can
easily encode ZFC, as well as ZFC + your favorite large cardinals, as
well as intuitionistic mathematics, temporal logic, etc., it would be
better to discuss the formalization thesis in terms of such type
theories. I am just pointing out that the practice of formalization
requires a great deal of "logic engineering" (that logicians are not
used to) that is invisible in ZFC.

Andrej Bauer