For example, if I used as an axiomatic system all the axioms of ZFC but left out the axiom of infinity and the axiom of replacement, I cannot then show that + is a well-defined operation.
I know this is a sidetrack, but I don’t think that’s right, unless we’re omitting the axiom of pairing as well. Can’t we use pairing to prove the finite version of replacement? (This needs an induction, but that doesn’t require the axioms of replacement or infinity.) Hence, can’t we show that addition of finite ordinals is well-defined, at least in the sense that we have a class Plus(x,y,z) satisfying the necessary properties?
(Actually, I think it ought to be possible to show that addition is well-defined even without pairing, because power set and separation alone (i.e. together with empty set and union) give us all hereditarily finite sets. Perhaps we can use them to prove that {x,y} exists when x and y are hereditarily finite.)
I know this is a sidetrack, but I don’t think that’s right, unless we’re omitting the axiom of pairing as well. Can’t we use pairing to prove the finite version of replacement? (This needs an induction, but that doesn’t require the axioms of replacement or infinity.)
If we don’t have the axiom of infinity then addition isn’t a function (since its domain and range aren’t necessarily sets).
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, but we still have a “class”. “Classes” are either crude syntactic sugar for “formulae” (as in ZFC) or they’re a slightly more refined syntactic sugar for “formulae” (as in BGC). In either case, classes are ubiquitous—for instance, ordinal addition isn’t a function either, but we prove things about it just as if it was.
I know this is a sidetrack, but I don’t think that’s right, unless we’re omitting the axiom of pairing as well. Can’t we use pairing to prove the finite version of replacement? (This needs an induction, but that doesn’t require the axioms of replacement or infinity.) Hence, can’t we show that addition of finite ordinals is well-defined, at least in the sense that we have a class Plus(x,y,z) satisfying the necessary properties?
(Actually, I think it ought to be possible to show that addition is well-defined even without pairing, because power set and separation alone (i.e. together with empty set and union) give us all hereditarily finite sets. Perhaps we can use them to prove that {x,y} exists when x and y are hereditarily finite.)
If we don’t have the axiom of infinity then addition isn’t a function (since its domain and range aren’t necessarily sets).
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.
Sure, but we still have a “class”. “Classes” are either crude syntactic sugar for “formulae” (as in ZFC) or they’re a slightly more refined syntactic sugar for “formulae” (as in BGC). In either case, classes are ubiquitous—for instance, ordinal addition isn’t a function either, but we prove things about it just as if it was.