Relational dual tableau decision procedures and their applications to modal and intuitionistic logics

Annals of Pure and Applied Logic 165 (2):409-427 (2014)
  Copy   BIBTEX


This paper introduces Basic Intuitionistic Set Theory BIST, and investigates it as a first-order set theory extending the internal logic of elementary toposes. Given an elementary topos, together with the extra structure of a directed structural system of inclusions on the topos, a forcing-style interpretation of the language of first-order set theory in the topos is given, which conservatively extends the internal logic of the topos. This forcing interpretation applies to an arbitrary elementary topos, since any such is equivalent to one carrying a dssi. We prove that the set theory BIST+Coll is sound and complete relative to forcing interpretations in toposes with natural numbers object . Furthermore, in the case that the structural system of inclusions is superdirected, the full Separation schema is modelled. We show that all cocomplete and realizability toposes can be endowed with such superdirected systems of inclusions.A large part of the paper is devoted to an alternative notion of category-theoretic model for BIST, which, following the general approach of Joyal and Moerdijkʼs Algebraic Set Theory, axiomatizes the structure possessed by categories of classes compatible with BIST. We prove soundness and completeness results for BIST relative to the class-category semantics. Furthermore, BIST+Coll is complete relative to the restricted collection of categories of classes given by categories of ideals over elementary toposes with nno and dssi. It is via this result that the completeness of the original forcing interpretation is obtained, since the internal logic of categories of ideals coincides with the forcing interpretation



    Upload a copy of this work     Papers currently archived: 93,069

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

33 (#500,331)

6 months
12 (#242,953)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Joanna Golinska-Pilarek
University of Warsaw
Emilio Muñoz-Velasco
Universidad de Málaga