TY - JOUR
T1 - A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is $\Pi$1-equivalent to KP
JF - Annals of pure and applied logic
Y1 - 2015
A1 - Kentaro Sato
A1 - Rico Zumbrunnen
AB - We introduce a version of operational set theory, OST?, without a choice operation, which has a machinery for {$Δ$}0{$Δ$}0 separation based on truth functions and the separation operator, and a new kind of applicative set theory, so-called weak explicit set theory WEST, based on Gödel operations. We show that both the theories and Kripke?Platek set theory KPKP with infinity are pairwise {$\Pi$}1{$\Pi$}1 equivalent. We also show analogous assertions for subtheories with ?-induction restricted in various ways and for supertheories extended by powerset, beta, limit and Mahlo operations. Whereas the upper bound is given by a refinement of inductive definition in KPKP, the lower bound is by a combination, in a specific way, of realisability, (intuitionistic) forcing and negative interpretations. Thus, despite interpretability between classical theories, we make ?a detour via intuitionistic theories?. The combined interpretation, seen as a model construction in the sense of Visser's miniature model theory, is a new way of construction for classical theories and could be said the third kind of model construction ever used which is non-trivial on the logical connective level, after generic extension à la Cohen and Krivine's classical realisability model.
PB - Elsevier
VL - 166
UR - http://www.iam.unibe.ch/ltgpub/2014/sz14.pdf
ER -