[FOM] Frege on Addition

[William Tait]

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