A programme in the philosophy of language developed by Dag Prawitz (1936– ) and Michael Dummett (1925–2011). These diverge from model-theoretic semantics by fleshing out logician Gerhard Gentzen’s (1909–1945) remark that the meanings of logical connectives are constituted or given by their introduction and elimination rules. Proof-theoretic semantics, like model-theoretic semantics, provide an account of the meaning of formulae, but parts ways with respect to what is needed in order to provide that meaning. Model theory explicates the meaning of formulae in terms of the models or circumstances in which they are true; proof-theoretic semantics is concerned with the meaning of a formula in terms of the circumstances in which it may be asserted, i.e., its assertability conditions.

The introduction rules for a connective $\circ$, for example, are taken to constitute the conditions under which formulae with $\circ$ as their primary connective may be asserted. For example, one may arguably come to understand the meaning of disjunctions by considering its introduction rule:

From the perspective of proof-theoretic semantics, this rule is meaning-constituting in the sense that one may infer that ${\phi }_0\vee {\phi }_1$ is assertable just in case ${\phi }_0$ or ${\phi }_1$ is assertable.