A Survey of Proof-theoretic Semantics

Two branches of proof theory

Prawitz observed that proof theory has two branches. On the one hand, there is the Hilbert-style 'reductive' proof theory that seeks to represent mathematical reasoning using syntactic structures. On the other, there is 'general' proof theory that studies proofs as mathematical objects in their own right. The term 'proof' here need not mean a formal derivation: for example, the BHK interpretation of intuitionism studies proofs without a derivation system.

Proof-theoretic semantics (P-tS) is the area of general proof theory concerned with semantics. It has two projects. First, to provide a semantics of proofs—explaining what makes arguments valid. Second, to give semantics in terms of proofs—defining the logical constants via their inferential roles. The term 'proof-theoretic semantics' was popularized by Schroeder-Heister in the early 1990s.

The semantics of proofs

In his foundational Investigations into Logical Deduction, Gentzen remarked that the introduction rules of his natural deduction systems define the meaning of the logical constants. This remark is as intuitive as it is enigmatic, and much of P-tS has concerned delivering on it. Prawitz, following an idea of Lorenzen, developed his normalization theory and used it to give a semantics of proofs. Let $\mathsf{L}$ be a system of proof rules and let $\mathbf{J}$ be a procedure on proof-structures that yields proof-structures (e.g. Prawitz's reductions for normalizing proofs). Validity relative to a 'base' $\mathcal{B}$ and the procedures $\mathbf{J}$ is then governed by the following principles:

There are several ways of instantiating these ideas. Prawitz conjectured that when $\mathbf{C}(\mathsf{L})$ is the set of $\mathcal{B}$-derivations together with canonical $\mathsf{NJ}$-derivations and $\mathbf{J}$ is taken to be the reduction operations of his normalization theorem, this would yield a semantics for intuitionistic proof. This turned out to be false.

From proofs to the logical constants

One can give a semantics of the logical constants based on Prawitz's semantics of proofs. A formula $\phi$ is 'supported' by $\mathcal{B}$ iff there is a $\langle \mathcal{B}, \mathbf{J} \rangle$-valid proof $\Phi$ concluding $\phi$. Piecha et al. studied Prawitz's semantics in this way. For example, disjunction may be expressed as follows:

$$\Vdash_{\mathcal{B}} \phi \lor \psi \qquad \text{iff} \qquad \Vdash_{\mathcal{B}} \phi \text{ or } \Vdash_{\mathcal{B}} \psi.$$

It turns out that intuitionistic logic is incomplete for this semantics—that is, Prawitz's conjecture was false. Stafford showed that the result is a semantics for an intermediate logic.

In parallel, Sandqvist developed a similar support relation and called it base-extension semantics (B-eS). The biggest difference is the treatment of disjunction, for which he uses the following clause:

$$\Vdash_{\mathcal{B}} \phi \lor \psi \qquad \text{iff} \qquad \forall \mathcal{C} \supseteq \mathcal{B}\ \forall P,\ \text{if } \phi \Vdash_{\mathcal{C}} P \text{ and } \psi \Vdash_{\mathcal{C}} P, \text{ then } \Vdash_{\mathcal{C}} P.$$

He showed that, depending on the choice of bases $\mathcal{B}$, this is a semantics for intuitionistic logic. Sandqvist has also given analogous semantics for classical logic. The motivation was to give an anti-realist foundation to logic, and so in both cases soundness and completeness are constructively valid.

Recent developments

This work has been developed tremendously in the recent period. Makinson revisited the B-eS for classical logic and explained its connection to the truth-functional account. Eckhardt and Pym used this to develop the B-eS for the standard modal logics. Gheorghiu et al. used the B-eS of intuitionistic logic to give B-eS for substructural logics—first IMLL and then BI—and Gheorghiu has studied the first-order case, following Sandqvist. There are many other results indicating the significance of B-eS for computational logic. These developments suggest that P-tS may offer a robust alternative to model-theoretic accounts, particularly in constructive and computational settings.

References