Sure, in the sense that it’s not a set. But instead we can make do with a (possibly proper) “class”. We define a formula Plus(x,y,z) in the language of set theory (i.e. using nothing other than set equality and membership + logical operations), then we prove that for all finite ordinals x and y there exists a unique finite ordinal z such that Plus(x,y,z), and then we agree to use the notation x + y = z instead of Plus(x,y,z).
This is not an unusual situation in set theory. For instance, cardinal exponentiation and ‘functions’ like Aleph are really classes (i.e. formulas) rather than sets.
Yes. But in ZFC we can’t talk about classes. We can construct predicates that describe classes, but one needs to prove that those predicates make sense. Can we in this context we can show that Plus(x,y,z) is a well-defined predicate that acts like we expect addition to act (i.e. associative, commutative and has 0 as an identity)?
In practice we tend to throw them around even when working in ZFC, on the understanding that they’re just “syntactic sugar”. For instance, if f(x,y) is a formula such that for all x there exists unique y such that f(x,y), and phi is some formula then rather than write “there exists y such that f(x,y) and phi(y)” it’s much nicer to just write “phi(F(x))” even though strictly speaking there’s no such object as F.
Can we in this context we can show that Plus(x,y,z) is a well-defined predicate that acts like we expect addition to act (i.e. associative, commutative and has 0 as an identity)?
I think the proofs go through almost unchanged (once we prove ‘finite replacement’).
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.
Sure, in the sense that it’s not a set. But instead we can make do with a (possibly proper) “class”. We define a formula Plus(x,y,z) in the language of set theory (i.e. using nothing other than set equality and membership + logical operations), then we prove that for all finite ordinals x and y there exists a unique finite ordinal z such that Plus(x,y,z), and then we agree to use the notation x + y = z instead of Plus(x,y,z).
This is not an unusual situation in set theory. For instance, cardinal exponentiation and ‘functions’ like Aleph are really classes (i.e. formulas) rather than sets.
Yes. But in ZFC we can’t talk about classes. We can construct predicates that describe classes, but one needs to prove that those predicates make sense. Can we in this context we can show that Plus(x,y,z) is a well-defined predicate that acts like we expect addition to act (i.e. associative, commutative and has 0 as an identity)?
In practice we tend to throw them around even when working in ZFC, on the understanding that they’re just “syntactic sugar”. For instance, if f(x,y) is a formula such that for all x there exists unique y such that f(x,y), and phi is some formula then rather than write “there exists y such that f(x,y) and phi(y)” it’s much nicer to just write “phi(F(x))” even though strictly speaking there’s no such object as F.
I think the proofs go through almost unchanged (once we prove ‘finite replacement’).
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.