9
$\begingroup$

I will clarify what I mean by the title in the following four ways:

For which cardinals $\kappa$ do we have that ZFC-(Powerset axiom)+$\exists\kappa$ is equiconsistent with ZFC? If that is not possible, for which cardinals $\kappa$ is the former theory stronger proof-theoretically, and what is the "weakest" cardinal axiom that can be taken so that that is the case?

Alternatively, for which cardinal axioms or axiom schema $A$ do we have that ZFC-(Powerset axiom)+$A$ is equiconsistent with ZFC+$A$? Is that even possible?

Alternatively, for which cardinals $\kappa$ do we have that CZF+$\exists\kappa$ or KP+$\exists\kappa$ is equiconsistent with ZF? If that is not possible, what is the "weakest" cardinal axiom that can be taken so that the former is stronger consistency or proof-theoretically-wise?

Are there cardinal axioms $A$ for which KP+$A$ or CZF+$A$ are as strong as ZFC-(Powerset axiom)+$A$? How about ZF+$A$?

Improve this question
$\endgroup$
3
  • 4
    $\begingroup$ I don't know about CZF, but for KP and ZFC-powerset the answer will be essentially never. This is because ZFC proves various reflection principles - for any finite collection of formulas, there is going to be some set satisfying these formulas. KP is implied by a finitely axiomatizable fragment of ZFC, so ZFC+T always implies Con(KP+T). For ZFC-powerset, in many cases we can instead pick $H_\kappa$ still satisfying T, and if $\kappa$ is regular, it will satisfy ZFC-powerset. $\endgroup$
    – Wojowu
    Commented Mar 24, 2022 at 18:22
  • 4
    $\begingroup$ For CZF this kind of question is really going to depend on how you formalize the large cardinal axiom in question. Classically equivalent formulations of axioms are frequently not intuitionistically equivalent. $\endgroup$
    – James E Hanson
    Commented Mar 24, 2022 at 18:31
  • $\begingroup$ @JamesHanson I would expect that to be the case for ZFC-powerset too. My proposed idea works for "local" definitions, in the sense of saying that if $\kappa$ has a large cardinal property, then it also does in $H_\lambda$ for some $\lambda$. But for more "global" definitions like using correctness or elementary embedding definitions the answer might be different. $\endgroup$
    – Wojowu
    Commented Mar 24, 2022 at 18:36

2 Answers 2

Reset to default
4
$\begingroup$

Are there cardinal axioms $A$ for which KP+$A$ or CZF+$A$ are as strong as ZFC-(Powerset axiom)+$A$? How about ZF+$A$?

In this answer I am going to treat this as a "know it when you see it" question, and attempt to give an answer that you may find satisfying even without a uniform treatment of what the canonical way is to formalize $A$ constructively.

In Hanul Jeon's talk slides "Very large set axioms over Constructive set theories" (2022, Cornell Logic Seminar) it is stated that the theories $\mathrm{CZF}$+"$V$ is totally Reinhardt" and $\mathrm{ZF}$+"$V$ is totally Reinhardt" are equiconsistent. The proof of one direction (constructive interpreting classical) is given in Jeon and Matthews's preprint with the same title, but there are some technicalities with formalizing "$V$ is totally Reinhardt", in which second-order versions of $\mathrm{CZF}$ and $\mathrm{ZF}$ have to be used.

Improve this answer
$\endgroup$
4
$\begingroup$

Every large cardinal property admits a formalization with the desired property. That is, every large cardinal property $\text{LC}$ admits a ZFC-provably equivalent formulation $A$ for which $\newcommand{\ZFC}{\text{ZFC}}\ZFC^-+A$ is equiconsistent with ZFC.

Let's begin with a lemma. (See my paper, Nonlinearity and illfoundedness in the large cardinal hierarchy of consistency strength for more along these lines.)

Lemma. There is an arithmetic sentence $\sigma$ such that $\ZFC^-+\sigma$ is equiconsistent with $\ZFC$.

Proof. Let $\sigma$ assert, "for any proof of a contradiction in $\ZFC$, there is a smaller proof of $\neg\sigma$ in $\ZFC^-$." Assume $\text{Con}(\ZFC)$, and hence $\text{Con}(\ZFC^-)$. If $\text{Con}(\ZFC^-+\sigma)$ fails, then there is a proof of $\neg\sigma$ from $\ZFC^-$. Since $\text{Con}(\ZFC)$ holds, there is no smaller proof of a contradiction in $\ZFC$, and so we can also easily prove $\sigma$ is true, contrary to $\text{Con}(\ZFC^-)$. So $\text{Con}(\ZFC)$ implies $\text{Con}(\ZFC^-+\sigma)$. Conversely, if $\text{Con}(\ZFC)$ fails yet $\text{Con}(\ZFC^-+\sigma)$ holds, then there is a proof of a contradiction in $\ZFC$, but no smaller proof of $\neg\sigma$ in $\ZFC^-$, and from this we can prove $\neg\sigma$, contrary to assumption. $\Box$

Theorem. For every large cardinal property $\newcommand{\LC}{\text{LC}}$, there is a $\ZFC$-provably equivalent formulation $A$ such that $\ZFC^-+\exists \kappa A(\kappa)$ is equiconsistent with $\ZFC$.

Proof. Let $A(\kappa)$ assert "if the power set axiom holds, then $\LC(\kappa)$, and if it does not, then $\sigma$." In $\ZFC$, the power set axiom holds, and so this property is equivalent to $\LC(\kappa)$ in $\ZFC$. But if it fails, we are asserting $\sigma$. If $\text{Con}(\ZFC^-+\exists\kappa A(\kappa))$, then either we get $\text{Con}(\ZFC+\exists\kappa\LC(\kappa))$ or we get $\text{Con}(\ZFC^-+\sigma)$, both of which imply $\text{Con}(\ZFC)$. Conversely, if $\text{Con}(\ZFC)$, then $\text{Con}(\ZFC^-+\sigma)$ and hence by going down to the hereditarily countable sets, we get $\text{Con}(\ZFC^-+\exists \kappa A(\kappa)$. $\Box$

I don't really work in CZF, but I expect that this kind of trick is fairly general.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .