[FOM] Formalization Thesis

[Timothy Y. Chow]

On Sat, 12 Jan 2008, Andrew Boucher wrote:
> Somehow you are now jumping to conclusions about skepticism about 
> 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