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.
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.