A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

2023/09/12 by Balbiani, Philippe, Gao, Han, Gencer, Çiğdem +1 · 4 citations
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2309.06309

Abstract

We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite countermodel of it.

Cited by

• Lax Modal Lambda Calculi
• Intuitionistic modal logic LIK4 is decidable
• Paraconsistent Constructive Modal Logic
• Intuitionistic modal logics: epistemic reasoning with distributed knowledge

Related

• A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels
• Local Intuitionistic Modal Logics and Their Calculi
• Intuitionistic Non-Normal Modal Logics: A general framework
• Intuitionistic modal logics: new and simpler decidability proofs for FIK and LIK
• Collapsing Constructive and Intuitionistic Modal Logics