William Tait williamtait at mac.com
Fri Sep 1 11:45:35 EDT 2006

```wwtx at earthlink.net  will soon no longer reach me. Please use
williamtait at mac.com

By "binary sequences of natural numbers" I of course meant binary
sequences, iu.e. of 0's and 1's.

Bill

On Aug 31, 2006, at 5:55 PM, William Tait wrote:

>
> On Aug 31, 2006, at 11:58 AM, Richard Heck wrote:
>
>> rege proposes to define addition of cardinal numbers in terms of
>> disjoint union. He proves that sums are unique but does not prove
>> that
>> they exist. It is both necessary and sufficient for this to prove
>> that
>> the domain can be partitioned, that is, that:
>>     (F)(G)(EU)(EV)[Nx:Fx = Nx:Ux & Nx:Gx = Nx:Vx & ~(Ex)(Ux & Vx)]
>> I take it that this will not be provable in Frege arithmetic:
>> second-order logic plus HP. It is clear that it would follow from
>> global
>> well-ordering, but the partition theorem seems not to imply anything
>> nearly that strong. So the question is: What can be said about what
>> partition requires? Does it entail some form of choice, for example?
>
> All that is required is a pairing function for the domain of
> individuals. Then represent the concept F by the concept F' with
> extension {(0,x} | Fx} and the concept G by G' with extension {(1, x
> | Gx}. NxF(x)+NxG(x) is then Nx{F'x or G'x), where o and 1 are two
> distinguished individuals. Cantor constructed such a pairing for the
> case that the individuals are the reals (i.e., binary sequences of
> natural numbers), for example, without assuming the reals are well-
> ordered.
>
> Regards,
>
> Bill Tait
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

```