English

The proof-theoretic strength of Constructive Second-order set theories

Logic 2025-09-22 v3

Abstract

In this paper, we define constructive analogues of second-order set theories, which we will call IGB\mathsf{IGB}, CGB\mathsf{CGB}, IKM\mathsf{IKM}, and CKM\mathsf{CKM}. Each of them can be viewed as IZF\mathsf{IZF}- and CZF\mathsf{CZF}-analogues of G\"odel-Bernays set theory GB\mathsf{GB} and Kelley-Morse set theory KM\mathsf{KM}. We also provide their proof-theoretic strengths in terms of classical theories, and we especially prove that CKM\mathsf{CKM} and full Second-Order Arithmetic have the same proof-theoretic strength.

Cite

@article{arxiv.2312.12854,
  title  = {The proof-theoretic strength of Constructive Second-order set theories},
  author = {Hanul Jeon},
  journal= {arXiv preprint arXiv:2312.12854},
  year   = {2025}
}

Comments

14 pages, final version

R2 v1 2026-06-28T13:57:17.751Z