Reference request: proof-theoretic strength of $\mathsf{KP}$ with recursively large ordinals and $\mathsf{CZF}$ with large set axioms

Large set axioms are notions corresponding to large cardinals on constructive set theories like $$\mathsf{IZF}$$ or $$\mathsf{CZF}$$. The notion of inaccessible sets, Mahlo sets, and 2-strong sets correspond to inaccessible, Mahlo, and weakly compact cardinals on $$\mathsf{ZFC}$$. (See Rathjen's The Higher Infinite in Proof Theory and Ziegler's thesis for the definition of notions I mentioned, and check the description added in the )

It is known that the proof-theoretic strength (or consistency strength if you are not familiar with the proof-theoretic one) of $$\mathsf{CZF}$$ is the same as that of $$\mathsf{KP}$$, so we may expect the strength of $$\mathsf{CZF}$$ with large sets are quite weaker than that of $$\mathsf{ZF}$$. In fact, Rathjen described the proof-theoretic strength of large sets over $$\mathsf{CZF}$$ in his paper The Higher Infinite in Proof Theory. Here is the result he stated:

Theorem 6.9. $$\mathsf{CZF}+\forall x\exists I (x\in I \land \text{I is inaccessible})$$ can be interpretable in $$\mathsf{KP}+\forall \alpha\exists \kappa>\alpha(\text{\kappa is recursively inaccessible})$$. Moreover, the interpretation preserves the validity of $$\Pi^0_2$$-sentences.

Theorem 6.14. $$\mathsf{CZF}+\forall x\exists M (x\in M \land \text{M is Mahlo})$$ can be interpretable in $$\mathsf{KP}+\forall \alpha\exists \kappa>\alpha(\text{\kappa is recursively Mahlo})$$. Moreover, the interpretation preserves the validity of $$\Pi^0_2$$-sentences.

Theorem 6.20. $$\mathsf{CZF}+\forall x\exists K (x\in M \land \text{K is 2-strong})$$ can be interpretable in $$\mathsf{KP}+\forall \alpha\exists \kappa>\alpha(\text{\kappa is \Pi_3-reflecting})$$. Moreover, the interpretation preserves the validity of $$\Pi^0_2$$-sentences.

However, Rathjen does not state the proof of his results in this paper. Combining some known results may result in a proof of the statement given above, but I have no clear idea which one would be relevant.

Question. Where can I find a proof (or a rough sketch of a proof) of the statements described above?

Added on 1 April 2021: I realized that just referring to Ziegler's thesis for the definition of large set axioms is not correct, since the different definitions result in different proof-theoretic strength.

Ziegler defined inaccessible sets as transitive sets which satisfy the second-order Strong Collection and $$\mathsf{CZF}$$. Some other references (e.g., Rathjen's paper I cited) add an additional requirement that an inaccessible set must satisfy the regular extension axiom $$\mathsf{REA}$$, which claims that every set is contained in a regular set. Let me call the former weakly inaccessible sets, and the latter strongly inaccessible sets.

It turns out that the existence of weakly inaccessible sets does not strictly increase the proof-theoretic strength:

Theorem. The theory $$\mathsf{CZF}$$ + "every set is contained in a weakly inaccessible set" has the same proof-theoretic strength with $$\mathsf{CZF+REA}$$.

(See Theorem 4.7 of Rathjen's The Anti-Foundation Axiom in Constructive Set Theories for its proof.)

However, the proof-theoretic strength of $$\mathsf{CZF}$$ with a strongly inaccessible set exceeds that of $$\mathsf{CZF+REA}$$. In fact, it has the same proof-theoretic strength with $$\mathsf{KP}$$ with a recursively inaccessible ordinal. (Theorem 6.5 of Rathjen's Proof Theory of Constructive Systems: Inductive Types and Univalence.)

Note that both weakly and strongly inaccessible sets are just $$V_\kappa$$ for an inaccessible cardinal $$\kappa$$ over $$\mathsf{ZFC}$$. There may be a difference between them over $$\mathsf{ZF}$$ since strongly inaccessible sets would think there is a proper class of regular cardinals. I do not think there is any direct relation between these two kinds of sets and weakly inaccessible cardinals.

Rathjen defined his inaccessible sets as strongly inaccessible sets in his papers, so we have to understand inaccessible sets in that sense.

• If we drop the higher infinites and just demand interpretation of $\mathsf{CZF}$ in $\mathsf{KP}$, do you know where a proof of this can be found, or is this also part of your question? Dec 27, 2020 at 17:25
• @Gro-Tsen I think this proof is relatively well-known. I cannot suggest the exact proof, but interpreting $\mathsf{CZF}$ to Martin-Löf type theory via Aczel's interpretation, and interpreting the type theory to $\mathsf{KP}$ would suffice. Dec 27, 2020 at 17:27
• @Gro-Tsen I also get a report from relevant sources from Twitter. (Unfortunately, the reporter mentions it via a protected account, so I cannot share.) Rathjen's The Realm of Ordinal Analysis briefly mentions how to prove it, and (unfortunately, at least for me that is not familiar with ordinal analysis) the proof uses ordinal analysis. (Add: the reporter said he will post an answer tomorrow (according to GMT+9), so I am waiting for it.*) Dec 27, 2020 at 17:29

Rathjen stated rough sketch of proof that intuitionistic theory (e.g. $$\mathsf{CZF}+(\forall x)(\exists I)[x\in I\land I \text{ is inaccessible}]$$) has at least the strength of the classical one (e.g. $$\mathsf{KP}\omega+(\forall\alpha)(\exists\kappa)[\alpha<\kappa\land\kappa\text{ is recursively inaccessible}]$$) in The Realm of Ordinal Analysis.
Let $$T_i$$ be intuitionistic theory, $$T$$ be classical theory corresponding to intuitionistic one, and $$\langle A,\prec\rangle$$ be primitive recursive well-ordering which has proof-theoretic ordinal of $$T$$.
1. Prove well-foundedness of $$\prec\restriction$$ in $$T_i$$ by using higher infinites where $$\prec\restriction$$ is proper initial seqment of $$\prec$$.
2. Embed $$T$$ into infinitary derivation $$\mathrm{RS}$$ and prove "$$T\vdash\varphi$$ implies there exists $$\alpha\in A$$ such that $$\mathrm{RS}$$-cutfree proof of $$\varphi$$ whose height bounded by $$\alpha$$ for all $$\Sigma_1^{L_{\omega_1^\mathrm{CK}}}$$-sentence $$\varphi$$" by using cut elimination and collapsings in $$T_i$$.
3. Prove "If there is $$\mathrm{RS}$$-cutfree proof of $$\varphi$$ whose height bounded by $$\alpha\in A$$, then $$\varphi$$ is true for all $$\Pi^0_2$$-sentence" by using transfinite induction up to $$\alpha$$ and $$\Pi^0_2$$-partial truth definition in $$T_i$$.