There’s a definition of division, or more precisely [a/b] on page 223 of Kleene’s

“Introduction to Metamathematics”. It’s by plain old type 0 primitive recursion.

I’ll write it out, followed by the definitions it needs. (I admit it needs a bit of

staring to see it’s correct.)

[0/b] = 0

[a'/b] = [a/b] + sgbar | b – (rm(a,b))’ |

rm(0,b) = 0

rm(a’,b) = (rm(a,b))’ . sg | b – (rm(a,b))’ |

|a – b| = (a .- b) + (b -. a)

a -. 0 = a

a -. b’ = pd(a -. b)

sgbar 0 = 1

sgbar b’ = 0

sg a = sgbar(sgbar a)

I hope that’s enough!

]]>