Proof-theoretic Semantics for First-order Logic

TL;DR

This paper develops a straightforward, constructive proof of completeness for proof-theoretic semantics in classical and first-order intuitionistic logic, avoiding complex model-theoretic assumptions.

Contribution

It introduces an elementary, native proof of completeness for classical logic's proof-theoretic semantics, extending techniques to first-order intuitionistic logic.

Findings

Elementary proof of completeness for classical logic P-tS

Soundness and completeness for first-order intuitionistic logic

Simplified approach applicable to propositional and first-order logics

Abstract

Sandqvist gave a proof-theoretic semantics (P-tS) for classical logic (CL) that explicates the meaning of the connectives without assuming bivalance. Later, he gave a semantics for intuitionistic propositional logic (IPL). While soundness in both cases is proved through standard techniques, the proof completeness for CL is complex and somewhat obscure, but clear and simple for IPL. Makinson gave a simplified proof of completeness for classical propositional logic (CPL) by directly relating the the P-tS to the logic's extant truth-functional semantics. In this paper, we give an elementary, constructive, and native -- in the sense that it does not presuppose the model-theoretic interpretation of classical logic -- proof of completeness the P-tS of CL using the techniques applies for IPL. Simultaneously, we give a proof of soundness and completeness for first-order intuitionistic logic (IL).