arXiv · 2312.12854
The proof-theoretic strength of Constructive Second-order set theories
Abstract
In this paper, we define constructive analogues of second-order set theories, which we will call $\mathsf{IGB}$, $\mathsf{CGB}$, $\mathsf{IKM}$, and $\mathsf{CKM}$. Each of them can be viewed as $\mathsf{IZF}$- and $\mathsf{CZF}$-analogues of G\"odel-Bernays set theory $\mathsf{GB}$ and Kelley-Morse set theory $\mathsf{KM}$. We also provide their proof-theoretic strengths in terms of classical theories, and we especially prove that $\mathsf{CKM}$ and full Second-Order Arithmetic have the same proof-theoretic strength.
Explore related subjects
Keep this discovery
Hanul Jeon. 2023-12-20. The proof-theoretic strength of Constructive Second-order set theories. https://doi.org/10.1215/00294527-2025-0008
Cite the original work for its findings. Save a collection to share your selection of sources.