Simpson's book Subsystems of Second Order Arithmetic shows $Z_2$ can interpret some fragments of ZF strong enough to give good theories of constructible sets and formalize statements like "there is a countable ordinal $\gamma$ such that $\gamma=\aleph_1^L$", Forcing in ZF shows this is independent of ZF and so certainly independent of $Z_2$. But can the independence be proved in some set theory interpretable in $Z_2$?

I ask because I expect it can.

But a positive answer would mean $Z_2$ implies consistency of a fragment of ZF with global well-ordering and existence of $\aleph_1$, obviously without power set. I don't know if that is possible.