Hybrids of the ^ -translation for CZF^

DOI10.1016/J.JAL.2005.09.001MaRDI QIDQ946579zbMATH OpenOpenAlexFDO

Authors Dominic Schulte

Publication date 23 September 2008

Published in Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jal.2005.09.001

zbMATH Keywords

functional interpretationadmissibility of rules in \(\text{CZF}^\omega\)constructive set theory in all finite typesmodified realisationq-hybrids of translations

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50) Functionals in proof theory (03F10)

Recommendations

• Logically enforced subprinciples of ZFC
• scientific article; zbMATH DE number 6307929
• Realizability for constructive Zermelo-Fraenkel set theory
• Functional interpretation of Aczel's constructive set theory
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Constructive sets in computable sets
• The disjunction and related properties for constructive Zermelo-Fraenkel set theory
• Choice and independence of premise rules in intuitionistic set theory
• Metamathematical properties of intuitionistic set theories with choice principles
• A new use of Friedman's translation: interactive realizability

Cites work

• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Functional interpretation of Aczel's constructive set theory
• Handbook of proof theory
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard

Cited in

(1)

• From the weak to the strong existence property

This page was built for publication: Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\)

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