  A folk theorem says higher order arithmetic has the proof theoretic strength
of set theory with limited power set. This paper makes the theorem precise in
terms of several axiom system based on ZF.
