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

Text
sz142.pdf  Submitted Version Available under License Publisher holds Copyright. Download (629kB)  Preview 

Text
1s2.0S0168007214000980main.pdf  Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (1MB)  Request a copy 
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, socalled 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 nontrivial on the logical connective level, after generic extension à la Cohen and Krivine's classical realisability model.
Item Type:  Journal Article (Original Article) 

Division/Institute:  08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG) 08 Faculty of Science > Institute of Computer Science (INF) 
UniBE Contributor:  Sato, Kentaro and Zumbrunnen, Rico 
Subjects:  000 Computer science, knowledge & systems 500 Science > 510 Mathematics 
ISSN:  01680072 
Publisher:  Elsevier 
Language:  English 
Submitter:  Florian Ranzi 
Date Deposited:  21 May 2015 13:13 
Last Modified:  25 May 2015 04:21 
Publisher DOI:  10.1016/j.apal.2014.10.001 
BORIS DOI:  10.7892/boris.63965 
URI:  http://boris.unibe.ch/id/eprint/63965 