Consider the following pair of functions:
- For α an ordinal, let $\nu(\alpha)$ be the least ordinal $\kappa$ such that $(V_{\kappa}, \in)$ is a model of ZFC in which there are $\alpha$-many inaccessibles. Note that $\kappa$ will be an inaccessible cardinal.
- For $\alpha$ an inaccessible, let $o(\alpha)$ be the set of all ordinals $\beta$ that ZFC proves "if there are $\alpha$ many inaccessible cardinals then $\beta$ is an ordinal".
(Note: as a commenter pointed out below, my original definitions weren't quite right, and my new definitions are probably still not quite right. I have an intuition that there's a thing you can do to get large ordinals which is to take an ordinal, jump to the next inaccessible (so that you have a model of ZFC), then consult ZFC to see what sort of strange sets you now should believe are ordinals, then take all those and jump to a model of a stronger theory that is like ZFC + a large cardinal you can name using all those big ordinals you just uncovered, which you can then use to uncover more ordinals, which you can use to trust a larger theory, which you can use to uncover more ordinals, and so on. That said, I suspect I'm failing to formalize this intuition correctly, and I'm not even sure it's coherent. If you know how to formalize it or show that it's incoherent, I'd appreciate some pointers.)
Question: is there a common name for the least $\alpha$ such that $o(\nu(\alpha)) = \alpha$? (I'm assuming here that ZFC can't prove it doesn't have a fixpoint, which might be wrong.)
Assuming this fixpoint exists and has a common name, what's an intuitive way to see how the definition above coincides with the common one?
I have a vague intuition that says $\mathrm{fix} (o \circ \nu)$ = Mahlo, because I suspect I could prove transfinite induction for $o(\nu(\alpha))$ for any ordinal $\alpha$ in Agda using induction-recursion, but I don't see how to prove that $(o \circ \nu)$ has a fixpoint using induction recursion, and I vaguely recall that induction recursion is equivalent in strength to the claim that a Mahlo cardinal exists. But I'm not very familiar with the mathematics of large cardinals yet, and I don't see how the definition above relates to the definition of a Mahlo cardinal (every club set contains an inaccessible). Bonus points for an answer that teaches me a bit more about good ways of thinking about the mathematics of large cardinals :-)