--- In dcproof@yahoogroups.com, "Dan Christensen" <dchris@...> wrote:
>
> Hi Dan,
> here's what I proved so far in constructing the add function.
>
> By the way, I think it's remarkable that the function used in the
> construction is "commutative" in its arguments, i.e. g(a,b)=g(b,a)
for
> all natural numbers a,b. (I proved this using the function
definition
> only!)
>
> Regards,
>
> Thomas
>
> [Download proof at www.dcproof.com/AddFunction_new_TH.proof ]
>


Thomas,

I like your straightfoward construction of the add function(lines
18 - 27). It is much superior to the one I posted here recently.
Good work!

Just a suggestion to tie things together. It would be nice to see
something like: Peano's Axioms implies there exists function f such
that f(x,1)=next(x) and f(x,next(y))=next(f(x,y)), f being the add
function.

Dan