Date: Aug 19, 2013 11:29 AM
Author: Alan Smaill
Subject: Re: Can addition be defined in terms of multiplication?
Alan Smaill <smaill@SPAMinf.ed.ac.uk> writes:

> Ben Bacarisse <ben.usenet@bsb.me.uk> writes:

>

>> William Elliot <marsh@panix.com> writes:

>>

>>> On Sun, 18 Aug 2013, Peter Percival wrote:

> ...

>>>> Then I think the onus is on you to produced definitions in one or both of

>>>> these forms:

>>>> x + y = ...

>>>> x + y = z <-> ...

>>>>

>>>> where the only non-logical symbols (baring punctuation) in the

>>>> ... are from this set: {*,S,0} or this set: {*,S,0,<}. I wouldn't

>>>> be surprised if + can be defined (in the way requested) from

>>>> {*,S,0} or {*,S,0,<} but I would like either to see it spelt out,

>>>> or to be given a reference.

>>>

>>> As Jim Burns said

>>> z = x + y iff 2^z = 2^x * 2^y

>>>

>>> where 2^n is defined by induction 2^0 = 1, 2^1 = 1 and 2^(n+1) = 2*2^n

>>> all of which can be done with Peano's axioms.

>>

>> Stepping out of my comfort zone here, but I think the point is that

>> allowing recursive definitions makes the theory second-order, and raises

>> the question of why one would not simply define + directly that way too.

>>

>> Broadly speaking, you can either have a second-order theory in which +

>> and * and so on are not in the signature of the language (but are

>> defined recursively) or you can have a first-order theory where + and *

>> and so on are added to the signature, with axioms used to induce the

>> usual meaning.

>>

>> I suspect Peter is talking about a first-order theory where recursive

>> definitions are not permitted.

>

> I do too; it can be done, but it is not easy.

>

> See Goedel on defining exponentiation from plus and times via the

> Chinese remainder theorem.

I should add: while this shows exponentiation is definable (by

abbreviational definitions) in Peano Arithmetic, as indeed any primitive

recursive function is, it doesn't show that exponentiation can be so

defined purely in terms of multiplication.

--

Alan Smaill