Sciweavers

Share
WOLLIC
2009
Springer

Sound and Complete Tree-Sequent Calculus for Inquisitive Logic

9 years 4 months ago
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).
Katsuhiko Sano
Added 25 May 2010
Updated 25 May 2010
Type Conference
Year 2009
Where WOLLIC
Authors Katsuhiko Sano
Comments (0)
books