Reasoning about proof and knowledge

TL;DR

This paper develops a hierarchy of modal logics for reasoning about intuitionistic truth, proof, belief, and knowledge, providing algebraic and relational semantics, and establishing completeness and adequacy of the systems.

Contribution

It introduces S5-style modal systems that extend previous hierarchies, linking them to an extended BHK interpretation and providing a unified semantics framework.

Findings

S5-style systems correspond to an extended BHK interpretation.

The systems are complete with respect to intuitionistic general frames.

Verification-based intuitionistic knowledge is a special case within these systems.

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\"odel'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.