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