Intuitionistic Modal Logic made Explicit.

The logic of proofs of Heyting arithmetic includes explicit justifications for all admissible rules of intuitionistic logic in order to satisfy completeness with respect to provability semantics. We study the justification logic iJT4, which does not have these additional justification terms. We establish that iJT4 is complete with respect to modular models, which provide a Kripke-style seman- tics, and that there is a realization of intuitionistic S4 into iJT4. Hence iJT4 can be seen as an explicit version of intuitionistic S4.

Authors

• Michel Marti
• Thomas Studer

Keywords

No keywords are indexed for this paper.