[FOM] Formalization Thesis

[Harvey Friedman]

On 12/26/07 4:35 PM, "William Tait" <williamtait at mac.com> wrote:

> 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.)
> 
> Timothy, this may not be the direction in which you want the
> discussion of the FT to go, but I would be interested in reading
> responses to it.
> 

One way of trying to meet this criteria is to use class theory, and, e.g.,
define what an ordered pair facility is. An ordered pair facility is a
one-one class function F:VxV into V.

Here it is perhaps best to formulate class theory via sets, classes, and
multivariate functions from sets to sets. Or maybe perhaps with more
facilities than this.

A function facility would be a partial function f:VxV into V which does the
right thing. I.e., f(F,x) = F(x), stated abstractly without using the usual
set theoretic treatment of set functions.

With real numbers, there is the standard ploy of looking at, say, nonempty
dense separable complete linear orderings with no endpoints.

Of course, there is the challenge of an exact description of just what I
have been doing in the preceding four (or all five of these) paragraphs.

Harvey Friedman