Contributions to intuitionistic epistemic logic
Michel Marti · BORIS Theses (Bern Open Research Information System) (Bern University Library, Hochschulstrasse 6, 3012 Bern, Switzerland) · 2017
This thesis is about two kinds of (closely related) logics: Modal logics and justification logics, both based on intuitionistic propositional logic. Epistemology is the theory of knowledge, and epistemic logics are logics dealing with knowledge. A classical way to formally treat knowledge goes back to Hintikka [Hin62]. In this approach, modal logic is used as an epistemic logic, with “the agent i knows that” as the modality ⃣ i and a possible worlds semantics. Justification logics are a more recent addition to the logical landscape. In these logics, we can explicitly reason about an agents’ evidence/justifications. Justification is a central epistemic concept as well, and justification logics are closely related to modal logics. Accordingly, this thesis has two parts. The first part is about intuitionistic modal logics, the second about intuitionistic justification logics. In the first chapter, we recall some soundness and completeness results about intuitionistic modal logic and fix notation and terminology. The logics IK and IT introduced here will serve as base logics that will later be extended by additional machinery, and the logic IS4 will show up again in the justification logic part. The next two chapters are about extending these base logics with distributed knowledge D and common knowledge C, respectively. For both these extensions, completeness will be shown using some canonical model constructions. In the case of distributed knowledge, we need to make a detour via so-called pseudo-models and strict pseudo- models. For common knowledge, we will have to work in a finite fragment and construct canonical models tailored to specific formulas. Finally, we turn to intuitionistic justification logic. Using similar tech- niques as in the previous chapters, we show soundness and completeness for so-called basic modular models and modular models.