# [FOM] Formalization Thesis

messing messi001 at umn.edu
Thu Dec 27 09:26:51 EST 2007

```I am afraid that I do not understand Bill Tait's comments concerning the
formalization thesis.  As Tim Chow formulated it in yesterday's posting,
it said:

Every theorem of ordinary mathematics is faithfully expressed by a
formal theorem of ZFC.

Tait writes:

One challenge to the Formalization Thesis, or maybe better, to a
satisfactory formulation of it, arises from the 'reduction to sets' of
various types of objects: ordered pairs, functions, ordinal numbers,
cardinal numbers, real numbers, etc. In each case, the reduction adds
structure to the type that is not part of its real meaning. In fact,
this was Dedekind's challenge. (And, as Benacerraf pointed out, there

1) The term 'reduction to sets' is, I presume, to be understood as
saying for example that the notion of the ordered pair (x,y) is defined
to be {{x},{x,y}} and similarly for the notions of ordinal nyumbers,
cardinal numbers, real numbers, ....

2) The phrase "the reduction adds structure to the type that is not part
of its real meaning", seems to me to false.  It presupposes that we,
either individually or collectively, "know" the REAL MEANING of a
mathematical concept.  This is a psychological point of view which I
find is entirely out of step with the actual way in which mathematicians
think.

3) The Formalization Thesis asserts that theorems or definitions or
conjectures or ... can be faithfully represented in ZFC.  It does not
state that there is an unique way to faithfully represent theorems or
....  For example in Bourbaki's initial treatment of logic and set
theory there were, in set theory, two predicate symbols: the membership
predicate and the ordered pair predicate.  The ordered pair predicate,
let me write it as OP, was introduced via OPxy is a set and there was
the axiom (OPxy = OPx'y') ===> (x = x' and y = y').  It seems to me
meaningless to ask whether the definition of ordered pair given above in
1) is a more faithful rendering of the notion of ordered pair than the
OP definition.  All that matters is that both function in actual
mathematics as practised by human beings or in some sort of idealized
machine language in precisely the same way.  To take another example, if
we define a cardinal number to be the samllest ordinal in the set of all
ordinals which are pairwise in bijective correspondence or if we define,
again a la Bourbaki, a cardinal number is a set which is, using the
Hilbert epsilon symbol, of the form epison_x(there exists a bijection x
---> y), and this set is written #(y) and called the cardinal number of
y.  All that matters is that there exists a bijection between y and y'
if and only if #(y) = #(y').

4) One might "object" to the Bourbaki definitions as being instances of
reification, but it seems to me that this is an aesthetic position and
not at all a mathematical one.

5) Finally I certainly believe that the Formalization Thesis is correct,
although whether it can be proved in some meta-language, would seem to
me, not a priori impossible, but would certainly require a preliminary
task of formalizing the notions of mathematical concepts, statements,
..., which, it seems to me, is a quite daunting undertaking.
```