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

摘要

We introduce a version of operational set theory, OST-, without a choice operation, which has a machinery for Delta(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 Godel operations. We show that both the theories and Kripke-Platek set theory KP with infinity are pairwise Pi(1) equivalent. We also show analogous assertions for subtheories with is an element of-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 KP, 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 a la Cohen and Krivine's classical realisability model. (C) 2014 Published by Elsevier B.V.