[FOM] Formalization Thesis

[Vaughan Pratt]

It would appear that Tim's question has hit one of FOM's more sensitive 
nerves.

I may be repeating points already made, but it seems to me that before 
one can judge such properties of the question as whether it is 
tautological the question should be split into two.

1.  Can mathematics be formalized?

2.  Is there a universal mathematical framework?

Question 1 has surely driven the form of mathematics for millennia. 
Question 2 on the other hand seems to be largely a 20th century 
question.  One might argue that Descartes addressed it three centuries 
earlier with his algebraization of geometry, but that did little for 
topology and number theory.

Tim began with the hypothesis of ZFC as a positive answer to 2.  However 
the pro-tautologists seem to be addressing 1.

The 2+2 = 4 example has been suggested as a possible counterexample to 
question 2.  Its interpretation in terms of long strings of curly 
braces, and its Mizar proof, merely served to knock it out as a 
counterexample, so we must look elsewhere for counterexamples to 2.

It seems even less likely as a counterexample to 1; how much more formal 
can one get than 2+2 = 4?

The question I want to raise in this post is, is 2+2 = 4 even mathematics?

Is a red ball a red ball?  If we interpret the first instance of "red 
ball" as connoting red balls and the second as connoting those entities 
that are both red and a ball, there is more to this question than to "is 
a ball a ball," especially when compared with the corresponding analysis 
of "is a bread knife a bread knife" meaning "is a bread knife something 
that is both bread and a knife?"

If we write 2 and 4 in Roman numerals, namely II and IIII (clock style) 
respectively, and use concatenation to denote addition rather than 
multiplication, we can ask whether IIII equals IIII, reading the first 
as the sum of II and II and the second as the Roman numeral for 4.

Now there is content in this question in just the same sense as we found 
content in "is a red ball a red ball?"  The ball question is surely not 
mathematical in any way, yet the form of the question is the same as for 
the above rendition of "is 2+2 = 4?", with an elided conjunction symbol 
in place of an elided summation symbol.

If we take the number IIII to mean the sum of II and II in the same way 
we take "red ball" to mean the conjunction of "red" and "ball", then 
what makes "is IIII equal to IIII?" mathematical and "is a red ball a 
red ball?" nonmathematical resides only in how we designate their terms: 
II is a mathematical term, "red" and "ball" are nonmathematical.

Is either kind of term more formal than the other?  Hardly: both have 
concrete significance---an Urbis Romana waiter miscomputing II+II can 
forget about his tip---yet both admit formalization, witness the Boolean 
algebra of conjunction.

But the reasoning by which we infer the truth of "is IIII equal to 
IIII?" seems too close to that for "is a red ball a red ball?" to 
justify treating one as mathematical and the other as nonmathematical on 
any basis other than their respective domains of discourse.  But if the 
domains are significant we would then want to make all sorts of 
distinctions, for example that the latter question deals with inanimate 
objects such as balls while "is a tall man a tall man?" deals with 
animate objects.

I submit that the essential content of 2+2 = 4 is not mathematical but 
logical.  The fact that numbers are considered mathematical while 
predicates are not (by mathematicians if not logicians) has little 
bearing on the essential content of 2+2 = 4, which is no more than the 
easily verified IIII = IIII suitably understood.

(Contrary to the widespread impression that Russell and Whitehead prove 
1+1 = 2 on page 362 of Volume I, they only promise it there and do not 
actually prove it until the top of page 83 (2nd. Ed.) of Volume II, 
where they promise three applications for it.  The myriad dense formulas 
of Volumes I and II leading up to that result arguably demonstrate a 
respect for mathematics best characterized as unhealthy.)

Vaughan Pratt