[Back]

R. Kuznets, S. Marin, L. Strassburger:
"Intuiting Duals of Proofs";
Talk: Milano Logic Group Logic Lunch Seminar Series, online, Italy (invited); 2021-03-11.

Justification Logic was introduced by Sergei Artemov, under the name of Logic of Proofs, in 1995 as a refinement of modal logic with explicit terms in place of the necessity/provability/knowledge modality. Over the years, multiple modal logics have received a justification treatment, which led to uncovering of the diversity of functional operators hidden within the modality []. For instance, while the K modality can be represented using only two functions on proofs/justifications (concatenation and application), the same modality of strength S5 is realized with two additional operators (positive and negative proof checker). However, the other modal operator <> has never been explored because classically it is simply a dual of []. In this joint work with Sonia Marin and Lutz Straßburger, we explore for the first time the nature of explicit terms for <> in bimodal intuitionistic-style modal logics, such as constructive modal logics, where De Morgan laws do not hold and the modality <> is uncoupled from [].