The proof-theoretic strength of constructive second-order set theories

DOI10.1215/00294527-2025-0008MaRDI QIDQ6930120zbMATH OpenFDO

Authors Hanul Jeon

Publication date 16 September 2025

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-66/issue-3/The-Proof-Theoretic-Strength-of-Constructive-Second-Order-Set-Theories/10.1215/00294527-2025-0008.full

zbMATH Keywords

constructive set theoryGödel-Bernays set theoryKelley-Morse set theoryproof-theoretic strengthsecond-order set theorytype-theoretic interpretation

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Relative consistency and interpretations (03F25) Metamathematics of constructive systems (03F50) Other constructive mathematics (03F65)

Cites work

• A model of second-order arithmetic satisfying AC but not DC
• Constructive set theory
• Constructive set theory and Brouwerian principles
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• Constructivism in mathematics. An introduction. Volume II
• CZF and second order arithmetic
• scientific article; zbMATH DE number 3427308 (Why is no real title available?)
• scientific article; zbMATH DE number 3427309 (Why is no real title available?)
• scientific article; zbMATH DE number 3839951 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 4012604 (Why is no real title available?)
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 194101 (Why is no real title available?)
• Proof theory. 2nd ed
• Subsystems of second order arithmetic
• THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS)
• The consistency of classical set theory relative to a set theory with intu1tionistic logic
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• The strength of some Martin-Löf type theories
• Very large set axioms over constructive set theories

This page was built for publication: The proof-theoretic strength of constructive second-order set theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6930120)