# [FOM] Formalization Thesis

Timothy Y. Chow tchow at alum.mit.edu
Sun Jan 13 15:09:30 EST 2008

```On Sat, 12 Jan 2008, Andrew Boucher wrote:
> automated proof-checking in general, which I would certainly not hold
> concerning "2 + 2 = 4".

Fair enough.  I did later try to clarify the Formalization Thesis by
giving the "Mizar version."  Mizar is based on ZFC + a universe axiom, so
I'm not completely changing my claim by talking about Mizar.  Experts on
Mizar can tell me if I'm wrong, but I'm presuming that Mizar does encode
natural numbers using von Neumann ordinals, and has some set-theoretic
definition of addition.  So "2 + 2 = 4" in Mizar is fairly close to what
you wrote down as a potential counterexample to a "faithful expression" of
"2 + 2 = 4".

It may be silly to speculate on the results of polling mathematicians or
people in the street, but I can't resist the temptation anyway.  I don't
know what you mean exactly by a "man in the street," but I cannot imagine
anyone having even the faintest understanding of what the question *is*,
unless they have advanced mathematical training.  So if they did indeed
all vote one way, I would be more inclined to attribute the result to some
artifact of the way the poll was conducted, rather than on any fact about
what people in the street really believe about the question.

More interesting is what working mathematicians would say.  They would
probably not understand the question either at first, and would want to
know what "faithfully expresses" is supposed to mean.  If we were to
clarify it as I did, by running Mizar and asking them if they believe that
Mizar verified that 2 + 2 = 4, then I would guess that most of them would
vote that Mizar did in fact verify that 2 + 2 = 4.  More generally, my
experience with working mathematicians who have some idea what "ZFC" is
is that they usually think of ZFC as being a foundation for all of
mathematics.  Thus they implicitly take the Formalization Thesis for
granted.  On the other hand, you might be right, and maybe they parrot
this claim about ZFC simply because they haven't thought it through, and
if they were confronted with concrete examples and were thereby forced to
think the matter through, then they might change their tune.

In any case, I think the "Mizar version" of the Formalization Thesis is a
better expression of my intent than my original version was, and it sounds
like we're in agreement that "2+2=4" is not a counterexample to that
version.

Tim
```