[FOM] None

[Harvey Friedman]

Reply to Makkai 4:55PM 6/22/03.

>
>As to the language, first, the *object-*language has to be fully
>explicit: it has to be  *formal*. (The metalanguage is quite optional, of
>course: one is free to discuss metalinguistically the System in any way
>one wants to.) Secondly, and just as importantly, the language has to be
>*right*, that is, expressive: merely *coding* what we have in mind is no
>good; we have to *say* what we mean. I would like to refer to what was
>said in this paragraph as *Frege's imperative".

Incidentally, coding-free is also the motto of Strict Reverse Mathematics

>
>I will now take a more radical point of view: I'll admit *only* urelements
>as elements of sets; in other words, "set" from now means "abstract set".
>
>We are at a decisive juncture: we have to answer "Frege's imperative" (see
>above). In fact, the best way of explicating the idea of "abstract set" is
>to place it into a (potentially) formalized language.

I know some axiomatizations of set theory in which all elements of 
sets are urelements.

The first one uses a primitive pairing function on the urelements. 
The second one is a binary relation theory, rather than a set theory, 
and doesn't use any primitive pairing function.

Here is the first one, T1. The language has two sorts of variables: 
lower case letters over urelements. Upper case letters over sets. 
<x,y> for the ordered pair of x,y, which is a urelement.

1. <x,y> = <z,w> iff x = z and y = w.
2. the set of all elements of any given set satisfying any given 
condition in the language is a set.
3, Two sets have the same elements if and only if they are equal.
4. given a set, and given a way of associating to any element, a 
unique set, we can take the union of all the sets so associated to 
form a set.
5. there is a nonempty set which is closed under ordered pairing.
6. given a set, there is a set of ordered pairs such that any subset 
of the given set is the set of first coordinates of elements of the 
set.
7. every set can be well ordered.

This system is mutually interpretable with ZFC.

I leave the second formalization with binary relations to the reader.

How does this fit into the discussion?

Harvey Friedman