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

[img]
Preview
Text
sz14-2.pdf - Submitted Version
Available under License Publisher holds Copyright.

Download (629kB) | Preview
[img] Text
1-s2.0-S0168007214000980-main.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, 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.

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: 0168-0072
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

Actions (login required)

Edit item Edit item
Provide Feedback