A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
type: Item
instance of: scholarly article
title: A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
author: Kentaro Sato
published in: Annals of Pure and Applied Logic
publication date: 2022-12-23T00:00:00Z
Mathematics Subject Classification ID: 03B30
Mathematics Subject Classification ID: 03E70
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F60
zbMATH DE Number: 7637214
zbMATH Keywords: \(\Pi_2^1\) conservation
zbMATH Keywords: interpretation
zbMATH Keywords: intuitionistic forcing
zbMATH Keywords: realizability
zbMATH Keywords: \(\Sigma_1^1\) collection
zbMATH Keywords: \(\Sigma_1^ 1\)-DC
MaRDI profile type: Publication
Wikidata QID: Q115221864
full work available at URL: j.apal.2022.103207
OpenAlex ID: W4307726500
cites work: Formalizing forcing arguments in subsystems of second-order arithmetic
cites work: Interpreting classical theories in constructive ones
cites work: Q4215634
cites work: Q3679172
cites work: On the relation between choice and comprehension principles in second order arithmetic
cites work: From hierarchies to well-foundedness
cites work: Q5619071
cites work: A well-ordering proof for Feferman's theoryT 0
cites work: TRUNCATION AND SEMI-DECIDABILITY NOTIONS IN APPLICATIVE THEORIES
cites work: A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC
cites work: Lifschitz' realizability
cites work: Forcing under Anti‐Foundation Axiom: An expression of the stalks
cites work: Double helix in large large cardinals and iteration of elementary embeddings
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: A NOTE ON PREDICATIVE ORDINAL ANALYSIS I: ITERATED COMPREHENSION AND TRANSFINITE INDUCTION
cites work: Elementary inductive dichotomy: separation of open and clopen determinacies with infinite alternatives
cites work: Bounded inductive dichotomy: separation of open and clopen determinacies with finite alternatives in constructive contexts
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
cites work: Factorization of polynomials and \(\Sigma ^ 0_ 1\) induction
DOI: 10.1016/J.APAL.2022.103207
description: scientific article; zbMATH DE number 7637214