# Can second order arithmetic make $\aleph_1^L$ countable?

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.

-
Can't the independence results, as purely formal statements of arithemtic $\text{Con}(ZF)\to\text{Con}(ZFC+\psi)$, be formalized in PA or much weaker systems? We don't need ZF to prove that ZF can formalize forcing. – Joel David Hamkins Nov 3 '12 at 12:03
Yes. Something weaker than PA (like EFA) suffices to show $\text{Con}(ZF)\rightarrow \text{Con}(Z_2+\psi)$ where $\psi$ is existence of a countable but not constructibly countable ordinal. I am asking whether $\text{Con}(Z_2)\rightarrow \text{Con}(Z_2+\psi)$. I would also be curious to know how far the forcing argument used in ZF can be interpreted in $Z_2$. – Colin McLarty Nov 3 '12 at 19:18
I'm still thinking about this (in the little spare time that I have these days) so I don't have an answer. Nevertheless, the proof of CH mod $V = L$ is very robust so I don't see how to get past that obstruction right now. Could you say more why you "expect it can" be done? – François G. Dorais Nov 5 '12 at 2:47
I'd expect that $Z_2$ plus "there is a countable ordinal that is $\aleph_1^L$" would prove the consistency of $Z_2$, by means of the countable model consisting of the constructible sets of natural numbers. If that's right, then of course, by the second incompleteness theorem, that theory could not be proved (in $Z_2$) to be consistent relative to $Z_2$. This might be sensitive to exactly how you formalize constructibility. My expectation might have a better chance if you use Gödel operations rather than definability. – Andreas Blass Nov 5 '12 at 6:04
Thanks to all. Very helpful comments giving me clearer expectations. In terms of my current project (proof theory of ZF with restricted power set) this has warned me away from a false route, and anyway I've found a simpler path that avoids this issue. So I could accept something like these comments as a sufficient answer. – Colin McLarty Nov 7 '12 at 15:23