A completeness theorem in proof-theoretic semantics via set-theoretic semantics
Ryo Takemura
TL;DR
The paper tackles the problem of completeness of intuitionistic logic with respect to proof-theoretic semantics by focusing on $\mathsf{IL^2 at}$, an atomic second-order intuitionistic propositional logic. It develops phase semantics built from closed $\lambda$-terms and constructs an $E$-phase model that captures proof-theoretic validity ($qE$-validity) and proves completeness, then extends the framework with $\eta$-expansion to an $I$-phase model to secure completeness for $I$-validity. The main contributions include a concrete phase-model construction, a precise link between E-phase validity and proof-theoretic validity, and a separate introduction-based model for $I$-validity, thereby connecting derivations to proof-terms under the Curry-Howard correspondence. This work clarifies how a set-theoretic phase interpretation can reflect proof-theoretic semantics and lays groundwork for extending the approach to additional connectives and argumentative reasoning.
Abstract
We investigate the completeness of intuitionistic logic with respect to Prawitz's proof-theoretic validity. As an intuitionistic natural deduction system, we apply atomic second-order intuitionistic propositional logic. By developing phase semantics with proof-terms introduced by Okada & Takemura (2007), we construct a special phase model whose domain consists of closed terms. We then discuss how our phase semantics can be regarded as proof-theoretic semantics, and we prove completeness with respect to proof-theoretic semantics via our phase semantics.