Advertisement
Published in:
2009 | OriginalPaper | Chapter
Sound and Complete Tree-Sequent Calculus for Inquisitive Logic
Author : Katsuhiko Sano
Published in: Logic, Language, Information and Computation
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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).