How strong is a Reinhardt set over extensions of CZF?

TL;DR

This paper explores the consistency strength of Constructive ZF with Full Separation and Reinhardt sets, showing it can interpret certain strong classical set theories with elementary embeddings.

Contribution

It establishes that CZF with Full Separation and a Reinhardt set can interpret ZF^- with elementary embeddings and models of the Wholeness axiom, indicating high consistency strength.

Findings

CZF+Sep with a Reinhardt set interprets ZF^- with an elementary embedding.

CZF+Sep with a Reinhardt set interprets ZF+WA_0.

Reinhardt sets over CZF have significant interpretative power.

Abstract

We investigate the lower bound of the consistency strength of $\mathsf{CZF}$ with Full Separation $\mathsf{Sep}$ and a Reinhardt set, a constructive analogue of Reinhardt cardinals. We show that $\mathsf{CZF+Sep}$ with a Reinhardt set interprets $\mathsf{ZF^-}$ with a cofinal elementary embedding $j\colon V\prec V$. We also see that $\mathsf{CZF+Sep}$ with a Reinhardt set interprets $\mathsf{ZF^-}$ with a model of $\mathsf{ZF+WA_0}$, the Wholeness axiom for bounded formulas.