> On 8/19/2013 6:23 AM, Alan Smaill wrote: >> Ben Bacarisse <firstname.lastname@example.org> writes: >> >>> William Elliot <email@example.com> writes: >>> >>>> 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 have several volumes of the complete works. > > Do you have any more specific information on > which paper?
There is a formulation in the incompleteness theorem article. he needed it to know that goedel numbers using exponentiation could be defined inside arithmetic with plus and times.