Choice and independence of premise rules in intuitionistic set theory

DOI10.1016/J.APAL.2023.103314MaRDI QIDQ6109095zbMATH OpenOpenAlexFDO

Authors Emanuele Frittaion, Takako Nemoto, Michael Rathjen

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 choicefinite typesindependence of premiseintuitionistic set theorypartial combinatory algebrasrealizability interpretation

Mathematics Subject Classification ID

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

Cites work

• An approach to general proof theory and a conjecture of a kind of completeness of intuitionistic logic revisited
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Constructive set theory
• Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions
• Constructivism in mathematics. An introduction. Volume II
• CZF and second order arithmetic
• CZF does not have the existence property
• Derived rules related to a constructive theory of metric spaces in intuitionistic higher order arithmetic without countable choice
• Disjunction and existence under implication in elementary intuitionistic formalisms
• Formal systems for some branches of intuitionistic analysis
• Formalized recursive functionals and formalized realizability
• 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 3839955 (Why is no real title available?)
• scientific article; zbMATH DE number 3811564 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3652333 (Why is no real title available?)
• scientific article; zbMATH DE number 3687373 (Why is no real title available?)
• scientific article; zbMATH DE number 3732046 (Why is no real title available?)
• scientific article; zbMATH DE number 3556031 (Why is no real title available?)
• scientific article; zbMATH DE number 1215498 (Why is no real title available?)
• scientific article; zbMATH DE number 3450172 (Why is no real title available?)
• scientific article; zbMATH DE number 3432235 (Why is no real title available?)
• scientific article; zbMATH DE number 3328132 (Why is no real title available?)
• scientific article; zbMATH DE number 3329865 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• Intuitionist type theory and the free topos
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Metamathematical properties of intuitionistic set theories with choice principles
• NEW PROOFS OF SOME INTUITIONISTIC PRINCIPLES
• On the interpretation of intuitionistic number theory
• Proof theory and intuitionistic systems
• Realizability and recursive set theory
• Realizability for constructive Zermelo-Fraenkel set theory
• Realizability. An introduction to its categorical side
• Relativized ordinal analysis: the case of power Kripke-Platek set theory
• Some derived rules of intuitionistic second order arithmetic
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories

Cited in

(4)

• scientific article; zbMATH DE number 749939 (Why is no real title available?)
• scientific article; zbMATH DE number 5064954 (Why is no real title available?)
• scientific article; zbMATH DE number 3296225 (Why is no real title available?)
• Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\)

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

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