show/hide this revision's text 2 Added that my version of Mathias's result assumes choice.

Bounded Zermelo is Zermelo set theory with only bounded separation. It has the same strength as simple type theory or MacLane set theory or ETCS. It is a finitely axiomatized fragment of Zermelo, so Zermelo proves it is consistent. And Mathias proved a paradigmatic example of the difference: Even if we add choice, Bounded Zermelo proves $\aleph_0$ exists, and every $\aleph_{\alpha}$ has a successor cardinal $\aleph_{\alpha+1}$, while BZ does not prove the quantified statement "for every $n\in \mathbb{N}$, there exists $\aleph_n$."

But is there some more quantitative measure of its strength? For example, do Zermelo and bounded Zermelo have meaningful proof theoretic ordinals? I have heard that proof theoretic ordinals do not work well for theories strong enough to prove existence of power sets.

show/hide this revision's text 1

How to measure the strength of Zermelo over bounded Zermelo?

Bounded Zermelo is Zermelo set theory with only bounded separation. It has the same strength as simple type theory or MacLane set theory or ETCS. It is a finitely axiomatized fragment of Zermelo, so Zermelo proves it is consistent. And Mathias proved a paradigmatic example of the difference: Bounded Zermelo proves $\aleph_0$ exists, and every $\aleph_{\alpha}$ has a successor cardinal $\aleph_{\alpha+1}$, while BZ does not prove the quantified statement "for every $n\in \mathbb{N}$, there exists $\aleph_n$."

But is there some more quantitative measure of its strength? For example, do Zermelo and bounded Zermelo have meaningful proof theoretic ordinals? I have heard that proof theoretic ordinals do not work well for theories strong enough to prove existence of power sets.