After a successful first talk given by Fabrizio Riguzzi, our Logic Lunch Seminar Series continues! The second talk will be delivered by Roman Kuznets (TU Wien) next Thursday (March 11th) starting at 12:30. Save the date and join us on Zoom at this link!
Title: Intuiting Duals of Proofs
Abstract: 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 .