论文标题
建设性理论上的非常大的公理
Very large set axioms over constructive set theories
论文作者
论文摘要
我们研究了根据建设性设置理论的基本嵌入方式定义的大型公理，重点是$ \ Mathsf {ikp} $和$ \ Mathsf {czf} $。大多数先前研究的大型公理，尤其是大型红衣主教的建设性类似物低于$ 0^\ sharp $，其证明理论强度比全二阶算术弱。另一方面，对于通过基本嵌入定义的情况，情况大不相同。我们表明，通过将$ j \ colon v \ $ j \ colon v \添加到$ \ mathsf {ikp} $中，以$Δ_0$ -formulas的形式嵌入$ j \ colon v \至m $，我们将用$ \ m athsf {Δ_0\ text { - } btee} btee} btee} btee} _m $，我们获得$ $ $ $ {我们还将看到Reinhardt集的一致性强度超过$ \ Mathsf {Zf+Wa} $的一致性。此外，我们将定义Super Reinhardt集和$ \ Mathsf {tr} $，这是$ V $的建设性类似物，完全是Reinhardt，并证明其证明理论的强度超过了$ \ Mathsf {Zf {Zf} $的$ \ Mathsf {Zf} $。
We investigate large set axioms defined in terms of elementary embeddings over constructive set theories, focusing on $\mathsf{IKP}$ and $\mathsf{CZF}$. Most previously studied large set axioms, notably the constructive analogues of large cardinals below $0^\sharp$, have proof-theoretic strength weaker than full Second-order Arithmetic. On the other hand, the situation is dramatically different for those defined via elementary embeddings. We show that by adding to $\mathsf{IKP}$ the basic properties of an elementary embedding $j\colon V\to M$ for $Δ_0$-formulas, which we will denote by $\mathsf{Δ_0\text{-}BTEE}_M$, we obtain the consistency of $\mathsf{ZFC}$ and more. We will also see that the consistency strength of a Reinhardt set exceeds that of $\mathsf{ZF+WA}$. Furthermore, we will define super Reinhardt sets and $\mathsf{TR}$, which is a constructive analogue of $V$ being totally Reinhardt, and prove that their proof-theoretic strength exceeds that of $\mathsf{ZF}$ with choiceless large cardinals.
