A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is $\Pi$1-equivalent to KP

TitleA new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is $\Pi$1-equivalent to KP
Publication TypeJournal Article
Year of Publication2015
AuthorsSato, K, Zumbrunnen, R
JournalAnnals of pure and applied logic
Volume166
Pagination121-186
AbstractWe 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.
URLhttp://www.iam.unibe.ch/ltgpub/2014/sz14.pdf