An Arithmetical Interpretation of Verification and Intuitionistic Knowledge

TL;DR

This paper extends the arithmetical semantics of intuitionistic logic to include an epistemic operator based on verification, linking intuitionistic knowledge with verification through formal semantics.

Contribution

It introduces an arithmetical interpretation of verification in intuitionistic epistemic logic, expanding the semantics of the BHK interpretation to include knowledge based on verification.

Findings

Extended the arithmetical semantics to intuitionistic epistemic logic.

Provided a formal system connecting verification with intuitionistic knowledge.

Linked the BHK interpretation with verification-based epistemic operators.

Abstract

Intuitionistic epistemic logic introduces an epistemic operator, which reflects the intended BHK semantics of intuitionism, to intuitionistic logic. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the Logic of Proofs and its arithmetical semantics. We show here that this interpretation can be extended to the notion of verification upon which intuitionistic knowledge is based, thereby providing the systems of intuitionistic epistemic logic extended by an epistemic operator based on verification with an arithmetical semantics too.