[FOM] No coding in ZC???

[Harvey Friedman]

On 2/27/06 9:48 AM, "Arnon Avron" <aa at tau.ac.il> wrote:

Friedman wrote:

>> Without a doubt, the right vehicle is ZC = Zermelo set theory
>> with the axiom of choice. You do lose some very interesting things,
>> but there is no coding involved.
> 
> No coding involved? Really? So here are some points to think about:
> 
> 1) There is no question that when core mathematicians speak on
>  a triple (a,b,c) they have in mind the set {{a},{a,{{b},{b,c}}}}.
> 
> 2) Similarly, ask any mathematician what is the sum of
>  {{}} and {{},{{}}} and he will tell you in less then a
>  second that it is {{},{{}},{{},{{}}}}
>    
> 3) Each positive rational number is (as any pupil in school knows)
>  a certain infinite collection of objects of the form
>  {{{{a},{a,b}}},{{{a},{a,b}},{{c},{c,d}}}}
> 
> 4) Since ZFC is the golden standard of the whole of mathematics,
>  it includes of course Geometry too. Yet I suspect that Euclid
>  would not have immediately agreed had he been told that no
>  coding is involved in seeing points in space as objects of the
>  form {{x},{x,{{y},{y,z}}}}, where each of x,y,z is a
>  certain infinite set of certain infinite sets of objects of
>  the form {{{{a},{a,b}}},{{{a},{a,b}},{{c},{c,d}}}}
>  where a,b,c,d are finite von Neumann ordinals.
> 
> 5) A crucial case of coding of a central mathematical concept
>  which most of core mathematicians *practically* do not accept
>  and use is the concept of a function. In set theory a function
>  is just a set of pairs Which satisfies a certain property.

The coding you are referring to is "the trivial standard coding". This is as
opposed to the coding involved in, say, systems in which all objects are
countable. In set theory, a Polish space (a complete separable metric space)
is not an hereditarily countable object, but an ordered pair (X,d), where X
is probably of power c, and d is a map from X x X into the nonnegative
reals. 

Even though this is the coding given by ones undergraduate education, and
never revisited, one can still remove this coding by many means.

One way is to expand the primitives. E.g., we can use natural numbers and
functions and sets. One writes down the obvious axioms.

Special devices are not needed because of the power of the axioms - say an
adapted form of ZC or ZFC.

Once the issue of tuples and functions is handled, one way or another, then
another very suitable device can be used - existential instantiation.

E.g., one can talk of "inductively ordered rings", and prove that they exist
and are all isomorphic, and use letters to stand for the components of an
arbitrary one, as the ordered group of integers. And talk of "complete
ordered fields", with letters to stand for the components of an arbitrary
one, as the ordered field of real numbers.

One can state and prove things like "every field has a suitably unique
algebraic closure" as mathematicians do it.

Harvey Friedman