> Transfinite induction does feel a bit icky in that finite prooflines you outline a process that has infinitely many steps. But as limits have a similar kind of thing going on I don’t know whether it is any ickier.
Well, transfinite induction / recursions is reduced to (at least in ZF set theory) the existence of an infinite set and the Replacement axioms (a class function on a set is a set). I suspect you don’t trust the latter.
The primary first need for transfinite recursion is to go from the successor construction to the natural numbers existing. Going to an approach that assumes an infinite set rather than proves it seems handy but weaker. Althought I guess in reading surreal papers I take set theory as given and while it doesn’t feel like any super advanced features are used there migth be a lot of assumption baggage.
It also feels llike a dirty trick that we don’t need to postulate the existence of zero and that we get surreals from not knowing any surreals. Surreal number definition references sets of surreal numbers? Don’t know any? Worry not there is the set that is of every type. And now that you have read the definition with that knowledge you know a new surreal number which enables you to read the definition again. So we get a lot of finite numbers without positing the existence of a single number and we don’t even need to explicitly define a successor relation.
The base number construction only uses set formation and order and doesn’t touch arithmetic operations, so on that level “the birthday” of mappings has yet to come so it is of limited use. I have seen formulations of surreal theory where it is written in a more axiomatic fashion but a “process” style gives a lto of ground to realise connections betweeen strctures.
The way it’s used in the set theory textbooks I’ve read is usually this:
define a function successor on a set S: S→S∪{S}
assume the existence of an inductive set that contains a set and all its successors. This is a weak and very limited form of infinite induction.
Use Replacement on the inductive set to define a general form of transfinite recursion.
Use transfinite recursion and the union operation to define the step “taking the limit of a sequence”.
So, there is indeed the assumption of a kind of infinite process before the assumption of the existence of an infinite set, but it’s not (necessarily) the ordinal ω. You can’t also use it to deduce anything else, you still need Replacement. The same can be said for the existence and uniqueness of the empty set, which can be deduced from the axioms of Separation.
This approach is not equivalent nor weaker to having fiat transfinite recursion , it’s the only correct way if you want to make the least amount of new assumptions.
Anyway, as far as I can tell, having a well defined theory of sets is crucial to the definitions of surreals, since they are based on set operations and ontology, and use infinite sets of every kind.
On the other hand, I don’t understand your problem with the impredicativity of the definitions of the surreals. These are often resolved into recursive definitions and since ZF-sets are well-founded, you never run into any problem.
I am pretty sure the is not obstacle for applying the successor function to the infinite set. And then there is the construction mirroring ω + ω. If you have the infinite set and it has many successors what limits one to not do the inductive set trick again to this situation?
I kinda know that if you assume a special inductive set that is only one “permitted application” of it and a “second application” would need a separate ad hoc axiom.
Then if we have “full blown” transfinite recursion we just allow that second-level application.
New assumtions assume that there are old assumptions. If we just have non-proof “I have feeling it should be that way” we have a pre-axiomatic system before hand. If we don’t aim to get the same theorems then “minimal change to keep intact” doesn’t make sense. The conneciton here is whether some numbers “fakely exist” where a fake existence could be that some axiom says the thing exist but there is no proof/construction that results in it. A similar kind of stance could be that real numbers are just a fake way to talk about natural numbers and their relations. One could for example note that reals are innumerable but proofs are discrete so almost all reals are undefineable. If most reals are undefinable then unconstructibility by itself doesn’t make transfinites any less real. But if the real field can establish some kind of properness then the same avenues of properness open up to make transfinites “legit”.
I am not that familar how limits connect to the foundamentals but if that route-map checks out then transfinites should not be any ickier than limits.
> Transfinite induction does feel a bit icky in that finite prooflines you outline a process that has infinitely many steps. But as limits have a similar kind of thing going on I don’t know whether it is any ickier.
Well, transfinite induction / recursions is reduced to (at least in ZF set theory) the existence of an infinite set and the Replacement axioms (a class function on a set is a set). I suspect you don’t trust the latter.
The primary first need for transfinite recursion is to go from the successor construction to the natural numbers existing. Going to an approach that assumes an infinite set rather than proves it seems handy but weaker. Althought I guess in reading surreal papers I take set theory as given and while it doesn’t feel like any super advanced features are used there migth be a lot of assumption baggage.
It also feels llike a dirty trick that we don’t need to postulate the existence of zero and that we get surreals from not knowing any surreals. Surreal number definition references sets of surreal numbers? Don’t know any? Worry not there is the set that is of every type. And now that you have read the definition with that knowledge you know a new surreal number which enables you to read the definition again. So we get a lot of finite numbers without positing the existence of a single number and we don’t even need to explicitly define a successor relation.
The base number construction only uses set formation and order and doesn’t touch arithmetic operations, so on that level “the birthday” of mappings has yet to come so it is of limited use. I have seen formulations of surreal theory where it is written in a more axiomatic fashion but a “process” style gives a lto of ground to realise connections betweeen strctures.
The way it’s used in the set theory textbooks I’ve read is usually this:
define a function successor on a set S: S→S∪{S}
assume the existence of an inductive set that contains a set and all its successors. This is a weak and very limited form of infinite induction.
Use Replacement on the inductive set to define a general form of transfinite recursion.
Use transfinite recursion and the union operation to define the step “taking the limit of a sequence”.
So, there is indeed the assumption of a kind of infinite process before the assumption of the existence of an infinite set, but it’s not (necessarily) the ordinal ω. You can’t also use it to deduce anything else, you still need Replacement. The same can be said for the existence and uniqueness of the empty set, which can be deduced from the axioms of Separation.
This approach is not equivalent nor weaker to having fiat transfinite recursion , it’s the only correct way if you want to make the least amount of new assumptions.
Anyway, as far as I can tell, having a well defined theory of sets is crucial to the definitions of surreals, since they are based on set operations and ontology, and use infinite sets of every kind.
On the other hand, I don’t understand your problem with the impredicativity of the definitions of the surreals. These are often resolved into recursive definitions and since ZF-sets are well-founded, you never run into any problem.
I am pretty sure the is not obstacle for applying the successor function to the infinite set. And then there is the construction mirroring ω + ω. If you have the infinite set and it has many successors what limits one to not do the inductive set trick again to this situation?
I kinda know that if you assume a special inductive set that is only one “permitted application” of it and a “second application” would need a separate ad hoc axiom.
Then if we have “full blown” transfinite recursion we just allow that second-level application.
New assumtions assume that there are old assumptions. If we just have non-proof “I have feeling it should be that way” we have a pre-axiomatic system before hand. If we don’t aim to get the same theorems then “minimal change to keep intact” doesn’t make sense. The conneciton here is whether some numbers “fakely exist” where a fake existence could be that some axiom says the thing exist but there is no proof/construction that results in it. A similar kind of stance could be that real numbers are just a fake way to talk about natural numbers and their relations. One could for example note that reals are innumerable but proofs are discrete so almost all reals are undefineable. If most reals are undefinable then unconstructibility by itself doesn’t make transfinites any less real. But if the real field can establish some kind of properness then the same avenues of properness open up to make transfinites “legit”.
I am not that familar how limits connect to the foundamentals but if that route-map checks out then transfinites should not be any ickier than limits.