Proof systems and decision algorithms for intuitionistic K
Marianna Girlando
Chair: Paul-André Melliès
Proof systems can be used to define decision algorithms for a given logic, that is, automated procedures establishing whether a formula is valid or not within the logic.
Such algorithms implement exhaustive and terminating root-first proof search for the formula in the calculus. If a proof is found the formula is valid. Otherwise, one can usually construct a countermodel for the formula at the root from a finite branch of a failed proof search tree.
In the literature, proof-theoretic decision procedures have been defined for intuitionistic logic, using (among other) sequent calculi and labelled calculi. Similarly, decidability of modal logics has (also) been proven by implementing terminating proof search for nested calculi for the logics.
In this talk we consider intuitionistic modal logic IK. This logic is the intuitionistic variant of modal logic K proposed by Fisher Servi, Plotkin and Stirling, and studied by Simpson. Semantically, the logic is characterised by bi-relational frames, comprising a preorder relation, as in intuitionistic possible-worlds models, and a binary relation, representing the modal accessibility relation.
We shall present two proof systems for the logic: a fully labelled sequent calculus, explicitly representing the two relations of IK-models, and a bi-nested calculus, having one syntactic connective for each relation. After introducing the proof systems, we will discuss and compare the corresponding decision algorithms, defined by implementing terminating proof search in the two calculi.
This talk is based on joint work with Han Gao, Roman Kuznets, Sonia Marin, Marianela Morales, Nicola Olivetti, and Lutz Straß burger.