A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus
Logic in Computer Science
2023-09-13 v1
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.
Cite
@article{arxiv.2309.06309,
title = {A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus},
author = {Philippe Balbiani and Han Gao and Çiğdem Gencer and Nicola Olivetti},
journal= {arXiv preprint arXiv:2309.06309},
year = {2023}
}