[FOM] Frege on Addition

[Neil Tennant]

On Thu, 31 Aug 2006, Richard Heck wrote:

> Frege 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?

Richard,

I don't have any URLs for the earlier discussion of these matters on fom,
but you raise an interesting question, which is to some extent
investigated in a paper of mine that you can download from my publications
web-page (http://people.cohums.ohio-state.edu/tennant9/ ; click on
"Articles" in the sidebar) with the title `Natural Logicism via the Logic
of Orderly Pairing'. The main idea in defining addition in that paper is
to say that t=u+v if u=#xFx, v=#xGx, and t is the number of things (that
is, ordered pairs) whose left projections are 0 and whose
right-projections are Fs, or whose left-projections are 1 and whose
right-projections are Gs. This invokes a prior theory, "sui generis", of
ordered pairs and of left- and right-projections of ordered pairs. (Frege,
of course, would have been able to provide a reconstructive version of
such a theory if, but only if, his class theory had been consistent.)

Your method, it seems to me, ought to work if you used your *finite*
Frege arithmetic, limiting your attention to such F and G as have finite
extensions. For then you could take for U(y) the predicate "y is a natural
number less than #xFx" and for V(y) the predicate "y is among the first
#xGx natural numbers greater than or equal to #xFx". There would surely be
some way of regimenting these glosses so that you could prove, in
second-order logic plus HP, that

(F)(G)(EU)(EV)[Nx:Fx = Nx:Ux & Nx:Gx = Nx:Vx & ~(Ex)(Ux & Vx)] ?

Best,
Neil Tennant