Justification logic for constructive modal logic
Roman Kuznets, Sonia Marin, Lutz Straßburger · HAL (Le Centre pour la Communication Scientifique Directe) · 2021
We provide a treatment of the intuitionistic ◊ modality in the style of justification logic. We introduce a new type of terms, called satisfiers, that justify consistency, obtain justification analogs for the constructive modal logics CK, CD, CT, and CS4, and prove the realization theorem for them.