A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
type: Item
instance of: scholarly article
title: A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
zbMATH Open document ID: 1371.03092
author: Sato Kentaro
author: Rico Zumbrunnen
published in: Annals of Pure and Applied Logic
publication date: 2014-11-28T00:00:00Z
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03C65
Mathematics Subject Classification ID: 03E70
Mathematics Subject Classification ID: 03F55
zbMATH DE Number: 6374922
zbMATH Keywords: applicative set theory
zbMATH Keywords: Feferman's OST
zbMATH Keywords: intuitionistic forcing
zbMATH Keywords: realisability
zbMATH Keywords: inductive definition
MaRDI profile type: Publication
full work available at URL: j.apal.2014.10.001
OpenAlex ID: W2065894311
cites work: Logic colloquium '77. Proceedings of the colloquium held in Wroclaw, August 1977
cites work: Interpreting classical theories in constructive ones
cites work: Forcing in Proof Theory
cites work: Q4075450
cites work: Principles of continuous choice and continuity of functions in formal systems for constructive mathematics
cites work: Goodman's theorem and beyond
cites work: Q3679172
cites work: Extending constructive operational set theory by impredicative principles
cites work: Q5457300
cites work: Q3081642
cites work: Q4981442
cites work: Q4128540
cites work: Q3882452
cites work: Q3671968
cites work: Operational set theory and small large cardinals
cites work: The consistency of classical set theory relative to a set theory with intu1tionistic logic
cites work: Q4179016
cites work: Q3037432
cites work: Proof-theoretical analysis: Weak systems of functions and classes
cites work: Proof-theoretic conservations of weak weak intuitionistic constructive set theories
cites work: A well-ordering proof for Feferman's theoryT 0
cites work: A VERSION OF KRIPKE‐PLATEK SET THEORY WHICH IS CONSERVATIVE OVER PEANO ARITHMETIC
cites work: Q3778746
cites work: Fixed points in Peano arithmetic with ordinals
cites work: Q5316376
cites work: On Feferman's operational set theory \textsf{OST}
cites work: Full operational set theory with unbounded existential quantification and power set
cites work: Operational closure and stability
cites work: Universes in explicit mathematics
cites work: Some theories with positive induction of ordinal strength φω0
cites work: Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
cites work: Reflections on reflections in explicit mathematics
cites work: Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
cites work: Q4981451
cites work: Explicit mathematics and operational set theory: some ontological comparisons
cites work: Q3852172
cites work: Realizability algebras: a program to well order R
cites work: Realizability algebras. II: New models of \(\mathrm{ZF} + \mathrm{DC}\)
cites work: Set theory. An introduction to independence proofs
cites work: The strength of Mac Lane set theory
cites work: Deduction-preserving "Recursive Isomorphisms" between theories
cites work: Forcing under Anti‐Foundation Axiom: An expression of the stalks
cites work: The strength of extensionality. I: Weak weak set theories with infinity
cites work: The strength of extensionality. II: Weak weak set theories without infinity
cites work: Q3395521
cites work: Theories with self-application and computational complexity.
cites work: A proof-theoretic characterization of the basic feasible functionals
cites work: Q4499084
cites work: Constructivism in mathematics. An introduction. Volume I
cites work: Realization of analysis into Explicit Mathematics
cites work: Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
cites work: Logic and structure
cites work: The predicative Frege hierarchy
DOI: 10.1016/J.APAL.2014.10.001
description: scientific article; zbMATH DE number 6374922