A completeness theorem in proof-theoretic semantics via set-theoretic semantics

TL;DR

This paper establishes a completeness theorem linking proof-theoretic semantics and set-theoretic semantics for intuitionistic logic using phase models with proof-terms.

Contribution

It introduces a novel phase semantics framework that demonstrates completeness of intuitionistic logic in proof-theoretic semantics via set-theoretic models.

Findings

Constructed a phase model with closed terms as domain

Proved completeness of intuitionistic logic w.r.t. proof-theoretic semantics

Bridged proof-theoretic and set-theoretic semantics for intuitionistic logic

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.