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

-
There is something confusing in the statement about cardinals. Is BZ the same as Bounded Zermelo? If so, is this just a failure of induction? Also, when you write $\aleph_\alpha$ do you mean a wellordered cardinal or the actual initial ordinal? –  François G. Dorais Dec 28 '12 at 1:25
Ah, in the absence of choice I should not use $\aleph$s so freely. Mathias shows: Bounded Zermelo proves there are transfinite sets, and any finite list of them can be lengthened, but does not prove the quantified statement "for every $n$ there is a set of $n$ transfinite sets each larger than the last." I would not call it a failure of induction. It is just that induction is stated for subsets of $\mathbb{N}$, and the above statement is not bounded and does not define a subset of $\mathbb{N}$. –  Colin McLarty Dec 28 '12 at 2:33
Toshiyasu Arai has been working on getting proof theoretic analysis higher up toward ZF. I'm not familiar enough with it to say anything. Arai has a lot of relevant papers on the arxiv - arxiv.org/find/math/1/au:+Arai_T/0/1/0/all/0/1 - and some surveys on his home page - kurt.scitec.kobe-u.ac.jp/~arai –  François G. Dorais Dec 28 '12 at 2:45