[FOM] Formalization Thesis

[messing]

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
is in general some arbitrariness about what structure is added.)

Let me make several comments:

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.