Can we define root extraction using Peano Arithmetic?

211 Views Asked by At

I've been playing with Peano Arithmetic and I've got multiplication, division, exponentiation, and logarithms. I can't figure out root extraction but I have a stab at it.

Exponentiation: $a^0 = 1, a^{S(b)} = a\cdot a^b$ Logarithm: $\log_a(1) = 0, \log_a(b) = 1 + \log_a(b/a)$

I'm finding root extraction much more complicated to work out a clean recursive definition for.

This is what I have so far, and I know it's wrong:

$\sqrt[b]{a} = f(1)$, $f(n) = n$ if $n^b = a$, otherwise $f(n+1)$