Large cardinals without choice?

For any given extension $T$ of ZFC (or perhaps NBGC or something), we can ask whether there is an extension $T'$ of ZF which does not prove AC such that

1. $Con(T) \leftrightarrow Con(T')$

2. $Con(T) \to Con(T')$ in a "nice" way, e.g. $T' + AC = T$.

3. $Con(T') \to Con(T)$ in a "nice" way, e.g. a model of $T$ can be obtained from any model of $T'$ by forcing or passing to an inner model.

I have a meta-question related to (1,2,3), as well as a more specific question which is similar in spirit:

• For large cardinal hypotheses $T$, which of (1,2,3) can be attained? Is the answer basically the same for most large cardinal hypotheses, or is it more heterogeneous? In particular, what is the situation for, say, Mahlo, measurable, Woodin, supercompact, and rank-into-rank cardinals (just to sample the spectrum)?

EDIT I've made the following a separate question

• At the top of the large cardinal hierarchy we have extensions $T'$ of ZF without a corresponding extension $T$ of ZFC -- e.g. Reinhardt cardinals. Apparently $Con(ZF + \mathrm{Reinhardt}) \to Con(ZFC+I_0)$, but is this implication "nice"? -- does it come via forcing / passing to an inner model?
• One problem lies in the huge difference of definitions when removing the axiom of choice from the equation. Having a measure does not imply having a normal measure; having a normal measure does not imply being a limit cardinal; having a normal measure and being a limit cardinal does not imply being a critical point of an embedding. In some cases, like supercompact cardinals the definition can be so different that the consistency strength is reduced also. If my memory serves me right, having a fine and normal ultrafilter on $\mathcal P_{\omega_1}(\kappa)$ is significantly weaker than [...] Apr 21, 2016 at 16:08
• [...] supercompact in ZFC. I'm not sure about having a fine and normal ultrafilter on every $\mathcal P_\kappa(X)$, or about having embeddings with the various properties, and how those compare to actual supercompactness. But at least one "reasonable" formulation gives us a severe reduction in consistency strength. I wouldn't be surprised if this phenomenon repeats itself in other cases (e.g. superhuge cardinals, I'd expect some similar reduction when talking about characterization using ultrafilters). Apr 21, 2016 at 16:10
• (Upon a second reading, I feel that my comments sort of miss the top part of the question. But they are somewhat related to the last point: passing from Reinhardt in ZF to I0 in ZFC. So I am going to leave the comments in place.) Apr 21, 2016 at 17:08
• @AsafKaragila I was actually expecting a more "genuinely set-theoretic" answer, more along the lines you were getting at, so I appreciate it -- especially because it makes clear that this kind of systematic work hasn't been done, or at least is not well-known. And although Con(ZF + Reinhardt) => Con(ZFC + I0) seems to be implicit in a lot of things I've read, I haven't been able to find a proof anywhere -- it's starting to drive me a little nuts! Apr 21, 2016 at 17:33
• I agree that such an approach would be more satisfactory when it is possible. But it seems unlikely to me to be possible in general to translate large cardinal axioms into a ZF context as familiar combinatorial assertions. Meanwhile, method 2 in my answer somewhat approaches this: we simply assert that the axiom holds for the HOD sets. Apr 21, 2016 at 17:42

Yes, there are some general methods to attain your properties for any theory $T$.

Method 1. For any theory $T$ extending ZFC, let $T'$ be the theory consisting of the following:

• ZF
• all the arithmetic consequences of $T$
• all assertions of the form $\text{AC}\to\sigma$, where $\sigma$ is in $T$.

If $T$ is a computably enumerable theory, then so is $T'$.

Since all the axioms of $T'$ are provable in $T$, we have $T\vdash T'$ and consequently $\newcommand\Con{\text{Con}}\Con(T)\to\Con(T')$. Also, notice that $T'+\text{AC}$ is equivalent to $T$, which is another way to see that $\Con(T)\to\Con(T')$.

Conversely, if $T'$ is consistent, then $T$ is consistent, since otherwise it would prove a contradictory arithmetic assertion, and this would be amongst the axioms of $T'$. So $\Con(T')\to\Con(T)$. The point is that the consistency strength of a theory is contained already in its arithmetic consequences. This is clear enough, but perhaps you don't regard it to fulfill the "niceness" property you mentioned in statement 3, in which case I refer you to method 2. For example, I don't know in general how to build a model of $T$ from a model of $T'$ by forcing or by going to an inner model.

Meanwhile, $T'$ does not prove AC, if consistent, because if $M$ is any model of $T$, then let $W$ be a model of $\text{ZF}+\neg\text{AC}$ with the same arithmetic as $M$. For example, we could use $L(\mathbb{R})^M$, if AC failed there, or we could in any case let $W$ be a symmetric extension of $M$ by Cohen forcing. Since $W$ and $M$ have all the same arithmetic assertions, we get $T'$ in $W$ with $\neg\text{AC}$.

Method 2. For any theory $T$ extending ZFC, let $T'$ be the theory asserting:

• ZF
• all axioms of the form $\text{AC}\to\sigma$ for $\sigma$ in $T$
• plus the assertion that if AC fails, then $\sigma$ holds in $\newcommand\HOD{\text{HOD}}\HOD$, for every $\sigma$ in $T$.

Thus, the theory $T'$ basically asserts that either $T$ holds outright, or it holds in HOD. And if $T$ was a finite extension of ZFC, then $T'$ will be a finite extension of ZF.

Since $T'+AC=T$, we get $\Con(T)\to\Con(T')$ in a nice way. Conversely, we get $\Con(T')\to\Con(T)$ in a nice way, since any model of $T'$ will have a definable inner model of $T$.

Lastly, $T'$ does not prove AC, if consistent, since if $M\models T$, then we can find an extension $W$ satisfying $\neg\text{AC}$ such that $\HOD^W=M$. Thus, $W$ will satisfy $T'+\neg\text{AC}$.

• In the third bullet item of Method 2, do you allow different models $W$ for different sentences $\sigma$? If not, how do you avoid undefinability-of-truth problems there? Apr 21, 2016 at 16:57
• There is no issue if $T$ extends ZFC with a single axiom. But in the general case, I was thinking of the third bullet as a scheme. But we can assume that $W$ is definable, so they are all using the same $W$. In fact, thinking about it now, we can just take $W$ as the HOD of $V$. Perhaps that is better than talking about ground models. I'll edit to this. Apr 21, 2016 at 17:03
• I have edited to use HOD instead of ground models, which I think makes a nicer theory. Basically, T' asserts that T holds in HOD, if AC fails. Apr 21, 2016 at 17:26
• @JoelDavidHamkins Thanks, this is interesting! I noticed that in (1), the axioms $\{AC \to \sigma \mid \sigma \in T\}$ sort of "ride for free", and are only necessary to get $T' + AC = T$ -- without them everything else works and we still have $T \vdash T'$ which I think I'd still consider to be a "nice" way to get $Con(T) \to Con(T')$. Regarding the existence of $W$ in (2) -- is this something I can find in, say, Kunen's book? Lastly, I don't suppose you know anything about how $Con(ZF + Reinhardt) \implies Con(ZFC+I_0)$ is proved? If $M \vDash ZF + Reinhardt$, does $HOD^M \vDash ZFC + I_0$? Apr 21, 2016 at 17:45
• Yes, I agree with you about (1), and that is indeed the only reason I added the axioms $\text{AC}\to\sigma$. For method 2, the basic fact is that every model of ZFC is the HOD of another model---you can find this in my paper Set-theoretic geology (jdh.hamkins.org/set-theoreticgeology). So you can do that forcing, and then form a symmetric extension, which will preserve it. Lastly, I'll give some thought to your question about Reinhardt and $I_0$. Apr 21, 2016 at 17:59