Well, we could define Plus(x,y,z) by “there exists a function f : x → z with successor(max(codomain(f))) = z, which preserves successorship and sends 0 to y”. (ETA: This only works if x > 0 though.)
And then we just need to do loads of inductions, but the basic induction schema is easy:
Suppose P(0) and for all finite ordinals n, P(n) implies P(n+1). Suppose ¬P(k). Let S = {finite ordinals n : ¬P(n) and n ⇐ k}. By the axiom of foundation, S has a smallest element m. Then ¬P(m). But then either m = 0 or P(m-1), yielding a contradiction in either case.
I’m not as confident but foundations is very much not my area of expertise. I’ll try to work out the details and see if I run into any issues.
Well, we could define Plus(x,y,z) by “there exists a function f : x → z with successor(max(codomain(f))) = z, which preserves successorship and sends 0 to y”. (ETA: This only works if x > 0 though.)
And then we just need to do loads of inductions, but the basic induction schema is easy:
Suppose P(0) and for all finite ordinals n, P(n) implies P(n+1). Suppose ¬P(k). Let S = {finite ordinals n : ¬P(n) and n ⇐ k}. By the axiom of foundation, S has a smallest element m. Then ¬P(m). But then either m = 0 or P(m-1), yielding a contradiction in either case.
Yes, this seems to work.