Proof-theoretic semantics for first-order logic

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 the completeness of classical propositional logic by directly relating 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 the completeness of the P-tS of CL using the techniques used for IPL. Simultaneously, we give a proof of soundness and completeness for first-order intuitionistic logic (IL).