IKP and friends

DOI10.2178/JSL/1190150286MaRDI QIDQ4451720zbMATH OpenOpenAlexFDO

Authors Robert S. Lubarsky

Publication date 1 March 2004

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

Full work available at URL https://arxiv.org/abs/1510.00463

zbMATH Keywords

forcingKripke modelsintuitionistic set theoryfixed points of inductive definitionsintuitionistic admissibility

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Intuitionistic mathematics (03F55)

Abstract: The basics of Intuitionistic Kripke-Platek set theory are developed, and some independence results among related classically equivalent theories are shown using Kripke models.

Recommendations

• Kripke models for subtheories of \textsf{CZF}
• Ordinal analysis of intuitionistic power and exponentiation Kripke Platek set theory
• scientific article; zbMATH DE number 5839768
• A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
• Logics of intuitionistic Kripke-Platek set theory

Cites work

• Extending Gödel's negative interpretation to ZF
• Sacks forcing sometimes needs help to produce a minimal upper bound

Cited in

(5)

• Forcing in Proof Theory
• Kripke models for subtheories of \textsf{CZF}
• Logics of intuitionistic Kripke-Platek set theory
• Realisability for infinitary intuitionistic set theory
• From the weak to the strong existence property

This page was built for publication: IKP and friends

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