A new model construction by making a detour via intuitionistic theories. IV: A closer connection between \(\mathrm{KP} \omega\) and \(\mathrm{BI}\).
type: Item
instance of: scholarly article
title: A new model construction by making a detour via intuitionistic theories. IV: A closer connection between \(\mathrm{KP} \omega\) and \(\mathrm{BI}\).
author: Kentaro Sato
published in: Annals of Pure and Applied Logic
publication date: 2024-05-14T00:00:00Z
Mathematics Subject Classification ID: 03B30
Mathematics Subject Classification ID: 03E30
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03E40
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 7848920
zbMATH Keywords: \(\Pi_{2}^ {1}\) conservation
zbMATH Keywords: interpretability
zbMATH Keywords: Kripke-style forcing
zbMATH Keywords: realizability
zbMATH Keywords: tree representation of sets
zbMATH Keywords: linearity of admissibles
MaRDI profile type: Publication
cites work: Q3992552
cites work: PROOF-THEORETIC STRENGTHS OF WEAK THEORIES FOR POSITIVE INDUCTIVE DEFINITIONS
cites work: Formalizing forcing arguments in subsystems of second-order arithmetic
cites work: On the relationship between ATR0 and
cites work: Interpreting classical theories in constructive ones
cites work: Q4075450
cites work: Q3679172
cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
cites work: Q3342568
cites work: A new method for establishing conservativity of classical systems over their intuitionistic version
cites work: From hierarchies to well-foundedness
cites work: The consistency of classical set theory relative to a set theory with intu1tionistic logic
cites work: Classes and truths in set theory
cites work: TRUTHS, INDUCTIVE DEFINITIONS, AND KRIPKE-PLATEK SYSTEMS OVER SET THEORY
cites work: A few more dissimilarities between second-order arithmetic and set theory
cites work: Open determinacy for class games
cites work: Zur Beweistheorie Der Kripke-Platek-Mengenlehre Über Den Natürlichen Zahlen
cites work: The strength of admissibility without foundation
cites work: Q3778746
cites work: Fixed points in Peano arithmetic with ordinals
cites work: Q4663832
cites work: Admissible extensions of subtheories of second order arithmetic
cites work: A survey of proof theory
cites work: A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC
cites work: The proof-theoretic analysis of transfinitely iterated quasi least fixed points
cites work: Q3138834
cites work: Proof-theoretic investigations on Kruskal's theorem
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: Forcing for hat inductive definitions in arithmetic
cites work: RELATIVE PREDICATIVITY AND DEPENDENT RECURSION IN SECOND-ORDER SET THEORY AND HIGHER-ORDER THEORIES
cites work: Full and hat inductive definitions are equivalent in NBG
cites work: A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
cites work: Elementary inductive dichotomy: separation of open and clopen determinacies with infinite alternatives
cites work: A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
cites work: A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
cites work: Q3069633
DOI: 10.1016/J.APAL.2024.103422
description: scientific article; zbMATH DE number 7848920