--- In dcproof@yahoogroups.com, Thomas Heye <1910-131@...> wrote:
>
> Hi Dan,
> On Wed, 11 Oct 2006 04:51:32 -0000, you wrote:
>
> >Thomas,
> >
> >I like your straightforward construction of the add function
(lines
> >18 - 27). It is much superior to the one I posted here recently.
> >Good work!
>
> Thanks for the flowers ;-). But in fact it's your construction of
Sep.
> 13. The main reason for removing the condition "(a,b,c) e n3" was
to
> ease handling the indirect proofs-- and maybe to save some lines of
> proof :-).

[snip]

My proof of Sep 13 was based on a construction of the set of
functions of two variables mapping NxN -> N, and then taking a
subset of that to get the set of what might be called additive
functions -- ones that satisfy the requirements for an add function.
Finally, I showed that all such functions are equivalent. With a bit
of "hand waving," this can be used to justify the definition of the
+ operator on the Numbers menu.

I was unable, however, to formally prove the existence of an add
function, i.e. there exists a function f mapping NxN -> N such that
(1) for all natural numbers x, f(x,1)=next(x), and (2) for all
natural numbers x and y, f(x,next(y))=next(f(x,y)). Your proof comes
closer to that ideal. I am working on a revised proof using your
construction that I hope will achievement this ideal.

Regards,
Dan