# Proof-theoretic Semantics for First-order Logic

arXiv: https://arxiv.org/abs/2410.11751 · HTML: https://mlsanity.com/paper/2410.11751/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Oct 2024.

## Built on by (most cited first, 1 of 1)

- [Towards an Inferentialist Account of Information Through Proof-theoretic Semantics](https://mlsanity.com/paper/2605.05368/) (2026)

## Abstract (arXiv)

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).