An Arithmetical Interpretation of Verification and Intuitionistic Knowledge
Tudor Protopopescu

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
