Choice and independence of premise rules in intuitionistic set theory

DOI10.1016/j.apal.2023.103314OpenAlexW4383215718MaRDI QIDQ6109095

Michael Rathjen, Takako Nemoto, Emanuele Frittaion

Publication date: 26 July 2023

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2023.103314

zbMATH Keywords

axiom of choiceintuitionistic set theoryrealizability interpretationpartial combinatory algebrasfinite typesindependence of premise

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Proof theory in general (including proof-theoretic semantics) (03F03) Intuitionistic mathematics (03F55) Relative consistency and interpretations (03F25)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Relativized ordinal analysis: the case of power Kripke-Platek set theory
• Realizability. An introduction to its categorical side
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• Realizability and recursive set theory
• Intuitionist type theory and the free topos
• Constructivism in mathematics. An introduction. Volume II
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• CZF and second order arithmetic
• Proof theory and intuitionistic systems
• CZF does not have the existence property
• NEW PROOFS OF SOME INTUITIONISTIC PRINCIPLES
• Disjunction and existence under implication in elementary intuitionistic formalisms
• Derived rules related to a constructive theory of metric spaces in intuitionistic higher order arithmetic without countable choice
• Constructive set theory
• Some derived rules of intuitionistic second order arithmetic
• An Approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• Formalized recursive functionals and formalized realizability
• Formal systems for some branches of intuitionistic analysis
• On the interpretation of intuitionistic number theory

This page was built for publication: Choice and independence of premise rules in intuitionistic set theory