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

2023/12/20 by Jeon, Hanul
#03E70 #03F25 #03F50 #03F65 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.2312.12854

Abstract

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

Related

• Comparison of constructive multi-typed theory with subsystems of second order arithmetic
• The Structure of Models of Second-order Set Theories
• A simple computational interpretation of set theory
• Logics and Admissible Rules of Constructive Set Theories
• Proof Theory of Constructive Systems: Inductive Types and Univalence