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

Sato, Kentaro; Zumbrunnen, Rico (2015). A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is Π1-equivalent to KP. Annals of pure and applied logic, 166(2), pp. 121-186. Elsevier 10.1016/j.apal.2014.10.001

Preview	Text sz14-2.pdf - Submitted Version Available under License Publisher holds Copyright. Download (629kB) | Preview
	Text 1-s2.0-S0168007214000980-main.pdf - Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (1MB)

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 Π1Π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.

Interest & Impact

Downloads

341 since deposited on 21 May 2015
22 in the past 12 months

Citations

5 Citations in Web of Science ®
6 Citations in Scopus

Search

in Google Scholar™

Services

Actions (login required)

Edit item

Actions (login required)

Edit item