2025/07/12 by Sonia Marin, Marin, Sonia, Paaras Padhiar +1
Computer Science · #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge
paper · pdf · doi:10.48550/arxiv.2507.09427
openalex publication_date 2025/07/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Justification logics are 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 e.g. using sequent, hypersequent or nested sequent calculi. In constructive modal logic, boxes and diamonds are decoupled and not De Morgan dual. Kuznets, Marin and Straßburger provide a justification counterpart to constructive modal logic CK and some extensions by making diamonds explicit by introducing new terms called satisfiers. We continue the line of work to provide a justification counterpart to Fischer Servi's intuitionistic modal logic IK and its extensions with the t and 4 axioms. We: extend the syntax of proof terms to accommodate the additional axioms of intuitionistic modal logic; provide an axiomatisation of these justification logics; provide a syntactic realisation procedure using a cut-free nested sequent system for intuitionistic modal logic introduced by Straßburger.