Reasoning about proof and knowledge
arXiv:1709.06672 · doi:10.1016/j.apal.2018.10.001
Abstract
In previous work [Lewitzka, Log. J. IGPL 2017], we presented a hierarchy of classical modal systems, along with algebraic semantics, for the reasoning about intuitionistic truth, belief and knowledge. Deviating from Gödel's interpretation of IPC in S4, our modal systems contain IPC in the way established in [Lewitzka, J. Log. Comp. 2015]. The modal operator can be viewed as a predicate for intuitionistic truth, i.e. proof. Epistemic principles are partially adopted from Intuitionistic Epistemic Logic IEL [Artemov and Protopopescu, Rev. Symb. Log. 2016]. In the present paper, we show that the S5-style systems of our hierarchy correspond to an extended Brouwer-Heyting-Kolmogorov interpretation and are complete w.r.t. a relational semantics based on intuitionistic general frames. In this sense, our S5-style logics are adequate and complete systems for the reasoning about proof combined with belief or knowledge. The proposed relational semantics is a uniform framework in which also IEL can be modeled. Verification-based intuitionistic knowledge formalized in IEL turns out to be a special case of the kind of knowledge described by our S5-style systems.
51 pages. The final corrected version is published in Annals of Pure and Applied Logic (2018), https://doi.org/10.1016/j.apal.2018.10.001
References in corpus (5)
- Intuitionistic Epistemic Logic
- Denotational semantics for modal systems S3--S5 extended by axioms for propositional quantifiers and identity
- A modal logic amalgam of classical and intuitionistic propositional logic
- Algebraic semantics for a modal logic close to S1
- Epistemic extensions of combined classical and intuitionistic propositional logic