We introduce a tree-sequent calculus for inquisitive logic (Groenendijk 2008) as a special form of labelled deductive system (Gabbay 1996). In particular, we establish that (i) our tree-sequent calculus is sound and complete with respect to Groenendijk’s inquisitive semantics and that (ii) our tree-sequent calculus is decidable and enjoys cut-elimination theorem. (ii) is semantically revealed by our argument for (i). The key idea which allows us to obtain these results is as follows: In Groenendijk’s inquisitive semantics, a formula of propositional logic is evaluated against a pair of worlds on a model. Given the appropriate pre-order on the set of such pairs, any inquisitive model can be regarded as a Kripke model for intuitionistic logic. This representation enables us to connect inquisitive semantics with the tree-sequent technique for non-classical logics (Kashima 1999).
Swipe to navigate through the chapters of this book
Please log in to get access to this content
To get access to this content you need the following product:
- Sound and Complete Tree-Sequent Calculus for Inquisitive Logic
- Springer Berlin Heidelberg
- Sequence number
Neuer Inhalt/© ITandMEDIA