Justification logic is an explication of modal logic: boxes are replaced with proof terms formally through realisation theorems. This can be achieved syntactically using a cut-free proof system for a modal logic, e.g., using sequent, hypersequent, or nested sequent calculi. In constructive modal logic, boxes and diamonds are decoupled and not De Morgan dual. Previous work provides a justification counterpart to constructive modal logic  \(\textsf{CK}\) (and some extensions) by making diamonds explicit and introducing new terms called satisfiers. We continue this line of work and provide a justification counterpart to intuitionistic modal logic  \(\textsf{IK}\) and its extensions with the  \(\textsf{t}\) and  \(\textsf{4}\) axioms. We extend the syntax of proof terms to accommodate the additional axioms of intuitionistic modal logic and provide an axiomatisation of these justification logics with a syntactic realisation procedure using a cut-free nested sequent system for intuitionistic modal logic.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Justification Logic for Intuitionistic Modal Logic

  • Sonia Marin,
  • Paaras Padhiar

摘要

Justification logic is an explication of modal logic: boxes are replaced with proof terms formally through realisation theorems. This can be achieved syntactically using a cut-free proof system for a modal logic, e.g., using sequent, hypersequent, or nested sequent calculi. In constructive modal logic, boxes and diamonds are decoupled and not De Morgan dual. Previous work provides a justification counterpart to constructive modal logic  \(\textsf{CK}\) (and some extensions) by making diamonds explicit and introducing new terms called satisfiers. We continue this line of work and provide a justification counterpart to intuitionistic modal logic  \(\textsf{IK}\) and its extensions with the  \(\textsf{t}\) and  \(\textsf{4}\) axioms. We extend the syntax of proof terms to accommodate the additional axioms of intuitionistic modal logic and provide an axiomatisation of these justification logics with a syntactic realisation procedure using a cut-free nested sequent system for intuitionistic modal logic.