Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic (Long Version)

TL;DR

This paper introduces epistemic realizability semantics for various forms of intuitionistic logic, defining verifier and generator programs that establish soundness and completeness of these logical systems.

Contribution

It proposes a novel epistemic semantics framework with verifier and generator programs, extending to minimal, second-order, and higher-order intuitionistic logic.

Findings

Proves soundness and completeness of the semantics for minimal logic.

Extends the semantics to second-order and higher-order intuitionistic logic.

Defines verifier and generator programs as evidence and generic realizers.

Abstract

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.