A Constructive Semantics for Classical Logic

Background

Constructivism in logic and mathematics holds that the meaning of a proposition is given by what counts as a proof or verification of it, rather than by potentially verification-transcendent truth conditions. The Brouwer–Heyting–Kolmogorov interpretation is the canonical expression of this position, explaining each logical constant in terms of what constitutes a proof of a compound proposition. As Schroeder-Heister argues, one of the ways of reifying this interpretation is proof-theoretic semantics (P-tS): it systematises the constructive programme by giving a precise, rule-based account of meaning in terms of inference.

The philosophical underpinning of P-tS is the Dummettian thesis that meaning is justification-practices. On this view, to grasp the meaning of a proposition is to know the conditions under which it is verified—what Dummett calls its assertion conditions—rather than the conditions under which it would be true independently of our capacity to recognise this. The logical constants receive their meaning from the rules governing their correct use in inference, not from their interpretation in a model. It is within this paradigm that the present work gives a constructive account of full classical propositional logic.

The specific framework employed is base-extension semantics (B-eS), in the tradition of Sandqvist and of Piecha et al. A base $\mathfrak{B}$ is a set of atomic inference rules encoding pre-logical inferential knowledge; the meaning of the logical constants is given by a support relation $\Gamma \Vdash_{\mathfrak{B}} \phi$ defined inductively on formulae, with the base case tied to derivability in $\mathfrak{B}$. Sandqvist gave a B-eS for classical logic, but his completeness proof relies on bar induction; while it has been refined to be elementary, the technique does not extend to the full standard language. By contrast, Sandqvist's B-eS for intuitionistic logic admits an elementary completeness proof, one that transfers to other logics with suitable natural deduction symmetry. Extending this constructive approach to classical logic with the full language—including $\vee$ as primitive—has remained an open problem.

Main contribution

This work presents a B-eS for classical propositional logic that resolves the above difficulties, built around the slogan:

Classical Logic = Intuitionistic Logic + Duality

The key innovation is to operate over literals rather than atoms. Following speech-act theory, but crucially restricting bilateralism to the atomic level, one distinguishes a set $\mathcal{C}$ of contents from the propositions built from them. A literal is either a positive proposition $c^{+}$ (assertion of $c$) or its primitive dual $c^{-}$ (denial of $c$); complex formulae built from literals by $\wedge, \vee, \to, \bot, \top$ are logico-grammatical structures, not themselves objects of illocutionary force. This restriction avoids the complications of uniform bilateralism while enabling the elementary completeness argument.

The system NK^±

The natural deduction system $\mathrm{NK}^{\pm}$ consists of the standard rules of intuitionistic propositional logic $\mathrm{NJ}$—operating over literals as atoms—augmented by two rules governing literal duality:

Here $l \in \mathcal{L}$ and $\varphi$ is any formula, and $l^{\bot}$ denotes the dual of the literal $l$ (so $(c^{+})^{\bot} = c^{-}$ and $(c^{-})^{\bot} = c^{+}$). The rule $\mathsf{Exc}_1$ (exclusion) ensures that $l^{\bot} \leftrightarrow \neg l$ is derivable; $\mathsf{Exc}_2$ (case analysis on literals) is the decidability schema for atoms. By a result of Negri and von Plato, these two rules together recover full classical logic from the intuitionistic base. The rules are harmonious: $\mathsf{Exc}_1$ is an introduction rule for $\bot$ and $\mathsf{Exc}_2$ functions as a case-elimination rule, and neither extends the expressible consequence relation beyond what the other warrants.

Base-extension semantics

Bases consist of atomic rules over literals; that is, with $l_i, l \in \mathcal{L}$ and $L_i \subseteq \mathcal{L}$ finite, they have the form

$$\dfrac{L, L_1 \Rightarrow l_1 \quad \cdots \quad L, L_n \Rightarrow l_n}{L \Rightarrow l}$$

Derivability in a base, $L \vdash_{\mathfrak{B}} l$, is defined inductively over such rules, for any $L \subseteq \mathcal{L}$, together with the two duality clauses:

• $\mathsf{Exc}_1$: if $L \vdash_{\mathfrak{B}} l$ and $L \vdash_{\mathfrak{B}} l^{\bot}$, then $L \vdash_{\mathfrak{B}} m$ for every $m \in \mathcal{L}$;
• $\mathsf{Exc}_2$: if $l, L \vdash_{\mathfrak{B}} m$ and $l^{\bot}, L \vdash_{\mathfrak{B}} m$, then $L \vdash_{\mathfrak{B}} m$.

Support is then defined by the clauses of Sandqvist's intuitionistic B-eS verbatim, as in Figure 2. Atomic support reduces to base derivability, conjunction and implication receive their standard proof-theoretic clauses, and disjunction is interpreted by quantification over base extensions and literals. The support clauses are identical to those for intuitionistic logic; the classical character is carried entirely by the base-level duality clauses above.

Soundness and completeness

The main result is the following:

$$\textbf{Theorem.}\quad \Gamma \Vdash \varphi \quad \text{if and only if} \quad \Gamma \vdash_{\mathrm{NK}^{\pm}} \varphi.$$

Soundness is proved by induction on $\mathrm{NK}^{\pm}$-derivations; the intuitionistic cases follow directly from Sandqvist, and the two classical cases use the duality clauses of base derivability. Completeness adapts Sandqvist's elementary simulation method: a simulation base $\mathcal{N}$ is constructed that encodes the rules of $\mathrm{NK}^{\pm}$ as atomic rules over literals, via a flattening of subformulae to fresh literals. Crucially, since $\mathsf{Exc}_1$ and $\mathsf{Exc}_2$ are built directly into base derivability, they require no separate simulation in $\mathcal{N}$, and the argument goes through for the full propositional language including $\vee$.

The proof is entirely constructive, requiring no bar induction, no excluded middle, and no detour through classical model theory; the reasoning appears formalisable in an intuitionistic metatheory, though a precise identification is left to future work. This meta-level constructivity is independent of the object-level sense in which the semantics is constructive—namely that support is defined without assuming bivalence.

Significance

Several aspects of this work are of direct interest to the proof-theoretic community. First, the bilateral restriction to atoms—rather than uniform bilateralism as in Rumfitt or Restall—is the precise condition that allows Sandqvist's elementary completeness strategy to transfer to classical logic with the full propositional language including $\vee$. Prior work either handled only implication and $\bot$, or required technically involved non-constructive proofs.

Second, since the support clauses above the atomic level are exactly those of intuitionistic logic, the semantics makes mathematically precise the philosophical thesis that classical logic is intuitionistic logic supplemented by atomic duality. This opens a direct path to the systematic study of classical extensions—including classical modal logics—along the lines of the intuitionistic programme developed by Sandqvist, by Gheorghiu, Gu, and Pym, and by Eckhardt and Pym.

Third, the result addresses Dummett's challenge on entirely anti-realist grounds: the metalogic is constructive, bivalence is not assumed, and the completeness proof witnesses that every classically valid inference is proof-theoretically supported. This semantic approach is complementary to the proof-term and polarity-based traditions for classical logic—the Curry–Howard line of Griffin, Parigot, and Girard, and the polarised calculi developed after them—which pursue constructivity through computation and focusing rather than base-extension meaning.

References