Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4661738 | Annals of Pure and Applied Logic | 2015 | 66 Pages |
Abstract
We introduce a version of operational set theory, OSTâ, without a choice operation, which has a machinery for Î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 KP with infinity are pairwise Î 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 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 à la Cohen and Krivine's classical realisability model.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
SATO Kentaro, Rico Zumbrunnen,