Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic (Long Version)
For logicians and computer scientists, this provides a new semantic framework that bridges realizability and epistemic notions, though the results are foundational and incremental in nature.
The paper introduces epistemic realizability, a semantics for intuitionistic logic where evidence-checking is semi-decidable, and proves soundness and completeness for minimal, second-order, and higher-order intuitionistic logic.
This paper explores epistemic realizability, a form of realizability in which the property that a piece of data constitutes evidence for a logical proposition is semi-decidable. In this framework, each proposition A is assigned a verifier} program that checks whether a datum X is a realizer for A, and a dual generator program that behaves as a generic realizer for X. We propose epistemic realizability interpretations for minimal logic, second-order intuitionistic logic, and higher-order intuitionistic logic, proving that each system is sound and complete under the proposed semantics.