# Largest provably existing ordinal in ZF without power set

If I remove the power set axiom from ZF, but retain the axiom of infinity, what will be the largest ordinal that can still be proven to exist. Or, if no largest such ordinal exist, what is the limit ordinal of all ordinals that can still be proven to exist. Of course, it is possible that even in this extended sense no such largest ordinal exists.

As Asaf convinced me, there is no need to modify the axiom of replacement or the axiom of foundation for the question to make sense in this context. However, the question as initially intended was about a useful set theory without the power set axiom (i.e. a theory one would use occasionally). As I gather from Miha Habič's comment, this would have been Kripke-Platek set theory (plus the axiom of infinity), and the largest provably existing ordinal would be $\omega_1^{CK}$ in that case.

• Why do you need to remove or adjust other axioms? The language does not have a symbol for the power set anyway. – Asaf Karagila Jun 1 '13 at 10:39
• My gut intuition is $\omega_1$ is the sup of ordinals constructible without power set, but don't hold me on this. – Kris Jun 1 '13 at 10:40
• This is an excellent question! – Rudy the Reindeer Jun 1 '13 at 10:46
• IIUC, strictly speaking, the answer to your question as written is "there is none": If there was a largest provably existing ordinal $o_{\text{max}}$, then you could prove the existence of $o_{\text{max}}+1>o_{\text{max}}$, in contradiction to the assumption that $o_{\text{max}}$ is the largest provably existing ordinal. – celtschk Jun 1 '13 at 12:49
• The question asks about ordinals that "can be proven to exist in every model of the axioms". That presupposes that one can compare ordinals from different models. That seems fine if we're talking about well-founded models, but if we take the phrase "every model of the axioms" literally, then some clarification is needed. Such models will, for example, have elements that are $\omega$ in the sense of the model but have predecessors beyond the usual natural numbers. – Andreas Blass Jun 1 '13 at 13:03