Sound and Complete Tree-Sequent Calculus for Inquisitive Logic

Abstract. 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 obtaining our results is as follows: In Groenendijk’s inquisitive semantics, a formula of propositional logic is evaluated by 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 equivalence enables us to connect inquisitive semantics with the tree-sequent technique for non-classical logics (Kashima 1999).

• Type: Conference
• Year: 2009
• Where: WOLLIC
• Authors: Katsuhiko Sano
• Keywords: Applied Computing, Groenendijk’s Inquisitive Semantics, Inquisitive Logic, Tree-sequent Calculus, WOLLIC 2009