Support is Search

1 Introduction

The semantics of the logical constants admits, broadly, two styles of explanation. On the first, model-theoretic semantics, meaning is given by the conditions under which a sentence is “true” in a structure. On the second, proof-theoretic semantics, meaning is given by the inferential behaviour that constitutes a demonstration of it; the tradition is that of Prawitz [32, 33], Dummett [3, 1, 2], and Schroeder-Heister [40, 41, 42]. The latter has received less attention, and its computational character in particular remains largely unexamined. This paper examines that character in a central case.

The case is the base-extension semantics for intuitionistic propositional logic due to Sandqvist [39], a particularly successful realisation of proof-theoretic semantics. A base $\base {B}$ is a collection of rules governing atomic sentences from which one defines a derivability relation on atoms $\vdash _{\base {B}}$. From this one has an inductively defined support relation $\supp _{\base {B}}$ on formulae, the clauses of which define each connective. The clause for falsum, for example, is $$\supp _{\base {B}} \bot \quad \text {iff}\quad \supp _{\base {B}} A \ \text {for every atom } A.$$

The clause is rather demanding computationally. The atoms may be infinitely many, and a verification of $\supp _{\base {B}} \bot$ accordingly comprises infinitely many verifications — and this within a programme whose founding commitment is that the meaning of a sentence is exhausted by what one can do with it. The constructivist has a standard reply: a universal claim is a claim to a method, and to say that every atom is supported is to say that one has, for any given atom, a way of showing that it is. What is that method? The clause does not say. That is the question of this paper.

The clause for disjunction is more remarkable still. It is not the expected $$\supp _{\base {B}} \varphi \lor \psi \quad \text {iff} \quad \supp _{\base {B}} \varphi \text { or } \supp _{\base {B}} \psi$$ — which would yield not intuitionistic but inquisitive logic, which is strictly stronger (see Piecha et al. [27, 26, 30]; Stafford [43]) — but rather the ‘second-order condition’ $$\begin {array}{ll} \supp _{\base {B}} \varphi \lor \psi \quad \text {iff} & \text {for every } \base {C} \baseext \base {B}\ \text {and every atom } A, \\[2pt] & \text {if } \varphi \supp _{\base {C}} A\ \text {and}\ \psi \supp _{\base {C}} A, \ \text {then } \supp _{\base {C}} A, \end {array}$$ where $\base {C} \baseext \base {B}$ means that $\base {C}$ extends $\base {B}$ by further rules, and $\varphi \supp _{\base {C}} A$ (resp. $\psi \supp _{\base {C}} A$) means that $A$ is supported in every extension of $\base {C}$ in which $\varphi$ (resp. $\psi$) is. Whether $A_1 \lor A_2$ is supported in $\base {B}$ — where $A_1$ and $A_2$ are atoms — thus depends upon every atom of the language, including those bearing no relation whatever to $A_1$ or $A_2$, and upon every extension of $\base {B}$. Whether that demand is met seems, prima facie, rather difficult to verify.

The two clauses raise a single question. Sandqvist’s theorem is that $\supp _{\base {B}} \varphi$ for every base $\base {B}$ if and only if $\varphi$ is intuitionistically provable. The result is striking, but it is also global: it characterises the formulae supported in every base. It leaves untouched what is, from a foundational point of view, the prior question — what does $\supp _{\base {B}} \varphi$ amount to in a fixed base $\base {B}$?

The naive answer has much to recommend it. At atoms, support simply is derivability: $\supp _{\base {B}} A$ holds precisely when $A$ is derivable by the rules of $\base {B}$. Support is monotone in the base, as derivability is in its hypotheses; the clause for implication, $\supp _{\base {B}} \varphi \to \psi$ iff $\varphi \supp _{\base {B}} \psi$, has the form of a deduction theorem; and a base, being a set of rules, may be read as a set of hypotheses. One expects, accordingly, that $\supp _{\base {B}} \varphi$ should coincide with derivability of $\varphi$ from some natural translation of $\base {B}$ into a set of formulae, and that the universal quantifiers of the clauses are merely a circuitous way of saying as much.

The expectation is refuted by an example that Sandqvist gives [39]. Fix atoms $A_1$ and $A_2$, and let $\base {R}$ consist of the rules one for each atom $A$: from $A$-if-$A_1$ and $A$-if-$A_2$, infer $A$. The disjunction $A_1 \lor A_2$ is supported in $\base {R}$: in any extension in which $A$ follows from $A_1$ and from $A_2$, the rule for $A$ concludes it outright. Yet neither $\supp _{\base {R}} A_1$ nor $\supp _{\base {R}} A_2$ holds: a derivation of $A_1$ in $\base {R}$ could end only with the rule for $A_1$, one of whose premisses is a derivation of $A_1$ from $A_2$, which could in turn end only with that same rule, and the same premiss remains outstanding; the case of $A_2$ is symmetric.

Derivability cannot behave in this way. The rules of $\base {R}$, read as formulae, are $\lor$-free — Harrop formulae — and from Harrop hypotheses a disjunction is derivable only if one of its disjuncts is [17]. What fails is the principle Piecha and Schroeder-Heister call export [30]: that the rules of a base may be exported into hypotheses, so that $\supp _{\base {B} \cup \Sigma } \varphi$ just in case $\Sigma ^{*} \supp _{\base {B}} \varphi$, where $\Sigma ^{*}$ is the set of rules of $\Sigma$ read as formulae, and hence, taking $\base {B}$ empty, that $\supp _{\Sigma } \varphi$ just in case $\Sigma ^{*} \vdash \varphi$. The lesson is that support in a base is not simply derivability in disguise.

We propose an alternative reading. The clause for disjunction does not say when a disjunction is supported; it says what one may do with one — namely, conclude any atom that each disjunct would yield on its own. It has, in this respect, a recognisable form in functional programming as a continuation-passing definition: the atom $A$ is the answer sought, and the hypotheses $\varphi \supp _{\base {C}} A$ and $\psi \supp _{\base {C}} A$ are the continuations — the branches of a case analysis, one of which will deliver it. A type theorist will recognise in the clause the type $$\forall \rho \,((\alpha \to \rho ) \to (\beta \to \rho ) \to \rho )$$ that a sum acquires under continuation-passing conversion. A logician will recognise it as Russell’s definition of disjunction [36, §19] and Prawitz’s second-order encoding of the connectives [34]. The recognition matters for what it suggests: that the clauses may be read computationally after all, and that the place to read them is a paradigm at once logical and computational — logic programming.

Logic programming, in the tradition of Kowalski [19] and, in the form relevant here, of Miller et al. [24, 23], is the view of computation as proof-search. A program is a set of formulae of restricted form — program clauses — and a goal is a formula whose provability from the program is in question; to execute the goal is to search for a proof of it, and the search is driven by the logical structure of the goal, each connective being an instruction as to how to proceed. A conjunction instructs one to establish both conjuncts; a disjunction, to establish either; an implication $D \supset G$, to add $D$ to the program and establish $G$; an atom, to consult the program. The program is thus consulted only at atoms, and the connectives of the goal are operations of search.

The bearing on the present problem is immediate: a base is a set of rules for atoms — that is, a program — and the support clauses, read as above, are themselves goals: instructions as to how a formula is to be verified against it. The instructions are not always those of the like-named connectives. Support for a disjunction does not require support for either disjunct, and the clause for disjunction is accordingly not a disjunctive goal; it is a universally quantified implication, which instructs one to take an arbitrary atom, to assume that it follows from each disjunct, and to establish it.

In logic programming, moreover, a universal quantifier in a goal is not a claim about a totality at all but an instruction: introduce a fresh name and proceed [24]. If the quantifiers of Sandqvist’s clauses admit this reading, the infinities disappear, and each support clause says precisely what a verification consists in — which is what was asked for.

To each formula $\varphi$ we associate a goal $\enc {\varphi }$ of the propositional hereditary Harrop language of Miller et al. [24], extended by a quantifier over atoms, and we establish that, for every base $\base {B}$, $$\supp _{\base {B}} \varphi \quad \text {iff}\quad \base {B} \vdash _O \enc {\varphi },$$ where $\vdash _O$ is the operational semantics of the language — the relation that obtains when $\enc {\varphi }$, executed as a goal against the program $\base {B}$, succeeds (Theorem 4.2). The encoding is a variant of the Russell–Prawitz translation, and the proof pairs each universal quantifier of the semantic clauses with a step of proof-search: the quantifiers over base extensions become Augment, which adds a hypothesis to the program, and the quantifiers over atoms become Generic, which introduces an atom under the usual freshness condition and proceeds. The constructive reading promised a method; the theorem exhibits it. Support is search.

The correspondence is not to be had for nothing, and three points require care. The encoding of an implication, $\enc {\varphi } \supset \enc {\psi }$, must serve both as a goal and as a clause of a program, and its consequent is in general compound; the clausal language must accordingly admit program clauses with compound heads, as the hereditary Harrop formulae of Miller et al. [24] do, such clauses being resolved into clauses with atomic heads when the program is consulted (Definition 2.6).

The quantifier of the language is instantiated at atoms only. It is the quantifier of Ferreira and Ferreira’s atomic polymorphism [4], not that of second-order logic. So the substitution lemma one would naturally reach for is false: a universal goal may be derivable while a compound instance of it is not (Remark 4.5).

The proof therefore proceeds by renaming of atoms, together with identity and cut for the class of formulae that are at once program clauses and goals; it follows the method of Miller’s argument that his Kripke models of hereditary Harrop programs agree with uniform provability [21, 22]. What it adds is the treatment of Sandqvist’s clauses for $\lor$ and $\bot$, which are elimination conditions quantifying over atoms and not the satisfaction clauses of a Kripke model, and of the atomic quantifier that answers to them.

The result is a local correspondence theorem complementing Sandqvist’s global one. It has three consequences.

First, the semantic clauses need not be regarded as ranging over completed infinite collections of inferential contexts. Their content is exhausted by a finitary search procedure — a successful search being a finite derivation. Proof-theoretic semantics, anti-realist in motivation, calls for a constructive reading. That reading is supplied not by external argument but by the structure of the semantics itself.

Second, support acquires computational content of a definite kind. The relation $\supp _{\base {B}} \varphi$ is not merely constructive in some abstract sense; it is the input–output specification of an explicit procedure — execute $\enc {\varphi }$ as a goal against $\base {B}$ — whose successful runs are uniform derivations witnessing support. The semantics is, in this sense, executable; and since, by Sandqvist’s theorem, $\varphi$ is intuitionistically provable just in case $\enc {\varphi }$ succeeds against the empty program (Corollary 4.9), so too is intuitionistic provability.

Third, and most broadly, the result places proof-theoretic semantics and the proof theory of logic programming in unexpected proximity. Sandqvist’s construction was developed independently of, and later than, Mints’ resolution-based proof methods for intuitionistic logic [25]; we have shown that the two constructions coincide up to renaming [6]. The present paper extends this convergence: it is not only Sandqvist’s particular base that is computationally intelligible, but the semantic framework in which it is constructed. What was offered as a philosophical foundation turns out to be, in mathematical content, a chapter of computational logic.

Organisation. Section 2 develops the framework of atomic systems and hereditary Harrop programs with a quantifier over atoms, and recalls the correspondence between them established by Gheorghiu and Pym [11]. Section 3 recalls Sandqvist’s base-extension semantics, the relevant background results, and the local question. Section 4 introduces the encoding of intuitionistic formulae as logic programming goals and proves the main theorem. Section 5 discusses the implications of the result — in particular for the question of what the universal quantifiers in base-extension semantics mean, for the role of higher-level rules, and for the prospects of a uniformly computational reading of proof-theoretic semantics more broadly.

2 Atomic Systems and Clausal Programs

Base-extension semantics rests on a primitive notion of atomic inference: before any account is given of the logical constants, one must first say what it is for an atomic sentence to be derivable. This is the role of an atomic system, or base. The purpose of this section is to fix the framework of atomic systems we shall use, and to develop a computational presentation of it. Two moves are involved. First, following Prawitz [32, 33] and Piecha and Schroeder-Heister [28, 29], we admit atomic rules of arbitrary finite level — rules whose premisses may themselves be rules. Second, following Hallnäs and Schroeder-Heister [15, 16] and Miller et al. [20, 24], we re-present these rules as clauses of a logic programming language, with derivability in the atomic system corresponding to operational proof-search in the clausal program.

The first move lets the semantics characterise intuitionistic rather than classical logic: Sandqvist has shown that first-level rules alone yield classical logic [38], while rules of level two suffice for the intuitionistic case [39]. We admit rules of arbitrary finite level for uniformity with the clausal language. The second move makes the main theorem of the paper possible. Both are well established in the literature, but they are not customarily presented together, and the combination repays explicit treatment.

Fix an infinite set $\mathrm {At}$ of atoms, or atomic sentences, ranged over by $A, B, C, \ldots$. The infinity at issue is potential, not actual: at any stage of a derivation only finitely many atoms have been introduced, but no bound is placed on how many may be introduced later. This is the only notion of infinity admissible from an anti-realist standpoint, and the only one we shall use — it presupposes no completed totality, only the open-ended availability of fresh names as derivation proceeds.

Higher-level atomic systems. The simplest atomic systems consist of production rules: rules that license the inference of an atom from a finite collection of atoms.

This format is, however, too restrictive. Rules in natural deduction for the logical constants — implication introduction and disjunction elimination, in particular — are not of this shape: their premisses are not assertions but derivations from hypotheses. If the atomic level is to support a semantics flexible enough to deliver intuitionistic logic, it must admit rules of the same kind. The generalisation, due to Piecha and Schroeder-Heister [28, 29], allows the premisses of an atomic rule to be themselves finite sets of atomic rules; iterating yields rules of arbitrary finite level.

Rules as clauses. The presentation of atomic systems we have just given is faithful to their natural deduction origins, but for the purposes of this paper a different presentation is more convenient. We re-present atomic rules as clauses of a logic programming language, and atomic derivability as operational proof-search. The translation, which we use throughout, is due in essence to Hallnäs and Schroeder-Heister [15, 16].

The clausal language is the propositional fragment of the hereditary Harrop formulae of Miller et al. [20, 24].

The asymmetry between $D$ and $G$ is the source of the language’s good proof-theoretic behaviour: definite formulae allow conjunction but not disjunction; goal formulae allow both, but their implications are hypothetical — the antecedent is a definite formula, added to the program for the duration of the goal.

The intended reading of a query is procedural: to resolve $G$ against $P$, decompose $G$ according to its logical structure, consulting $P$ only when an atomic goal is reached. This is captured by the following operational semantics.

Fact	$P \vdash _O A$	if $A \in [P]$
Backchain	$P \vdash _O A$	if $G \supset A \in [P]$ and $P \vdash _O G$, for some $G$
And	$P \vdash _O G_1 \cap G_2$	if $P \vdash _O G_1$ and $P \vdash _O G_2$
Or	$P \vdash _O G_1 \cup G_2$	if $P \vdash _O G_1$ or $P \vdash _O G_2$
Augment	$P \vdash _O D \supset G$	if $P \cup \{D\} \vdash _O G$
Generic	$P \vdash _O \forall X\, G$	if $P \vdash _O G[A/X]$, for some $A$ fresh for $P$ and $G$

The connection between atomic systems and clausal programs is now direct: each atomic rule translates to a program clause, and the level of the rule corresponds to the nesting depth of implications in that clause.

Gheorghiu and Pym [11] have shown that the hierarchy of higher-level atomic systems corresponds exactly to the implication-nesting depth of definite formulae: an atomic rule of level $n$ becomes a definite formula of nesting depth $n$, and conversely. For any atomic system $\base {S}$ with clausal representation $P$, and any atom $A$, $$P \vdash _O A \qquad \text {iff} \qquad \vdash _{\base {S}} A.$$ Clauses with compound heads add convenience, not strength: the clausal representation of an atomic rule has an atomic head, and a clause with a compound head is, by the elaboration, a notation for clauses with atomic heads. Compound heads are admitted because Section 4 requires implications to be at once program clauses and goals whatever their consequents. We shall henceforth identify an atomic system with its clausal representation, writing $\base {S} \vdash _O A$ in place of $\vdash _{\base {S}} A$.

Schematic infinity and the atomic quantifier. One complication remains. The atomic systems used in base-extension semantics are routinely infinite; indeed, the completeness of intuitionistic propositional logic with respect to support requires this. But not every infinite system is to be admitted. This is not a technical convenience but a substantive constraint: the anti-realist foundations of the semantics forbid appeal to arbitrary completed infinities. The infinities of base-extension semantics must be schematic: each instance of a rule must be specifiable by a finite description.

A representative case illustrates the point. Sandqvist’s completeness proof [39] uses an atomic system containing every instance of the schema $$(A \supset X) \cap (B \supset X) \supset X$$ for some fixed atoms $A$ and $B$ as $X$ ranges over atoms. The system is infinite, but its content is exhausted by a finite specification. We need only formalise that finite specification. To this end, we extend the logic programming language with a quantifier ranging over atoms. Propositional variables, ranged over by $X$, are drawn from a set $\mathrm {Var}$ disjoint from the atoms.

The schema above becomes the single program clause $$\forall X\bigl ((A \supset X) \cap (B \supset X) \supset X\bigr ),$$ and the move from infinite to finite specification is complete.

The atomic formulae of the extended language are the atoms together with the variables. We write $G[A/X]$ for the result of replacing the free occurrences of $X$ in $G$ by the atom $A$, and we say that an atom is fresh for a formula or program if it does not occur in it. Programs, and the goals queried against them, are closed: every variable occurring in them is bound. In a closed formula, therefore, an atomic subformula standing alone as a goal or as a program clause is an atom.

The quantifier is not the quantifier of second-order propositional logic, nor the higher-order quantifier of Miller et al. [24], either of which may be instantiated at compound formulae of the appropriate type. It is instantiated at atoms only, and is in this respect the quantifier of the system $\mathbf {F}_{\mathrm {at}}$ of atomic polymorphism studied by Ferreira and Ferreira [4, 5]; the point is taken up in Remark 4.5. Its operational behaviour is governed by the eigenvariable discipline.

We close the section by recording three properties of $\vdash _O$ which will be used freely in what follows. Each is proved by induction on the derivation, and each preserves the height of the derivation, a fact on which the inductions of Section 4 depend. A function $\sigma$ from atoms to atoms is extended to formulae homomorphically, leaving variables unchanged, and to programs pointwise; we write $F\sigma$ and $P\sigma$ for the results. Observe that $[P]\sigma \subseteq [P\sigma ]$: the map $\sigma$ commutes with the conditions that define the elaboration, and in particular it carries the instance $D[A/X]$ of $\forall X\, D$ to the instance $(D\sigma )[A\sigma /X]$ of $\forall X\, (D\sigma )$.

The case of interest is that in which $\sigma$ moves a single atom. If $P \vdash _O G$ and the atom $A$ does not occur in $P$, then $P \vdash _O G[B/A]$ for every atom $B$, where $G[B/A]$ denotes the result of replacing $A$ by $B$ throughout $G$. An eigenvariable introduced by Generic may thus be moved to any atom whatever, provided the program does not mention it. This is the only form of substitution the paper requires; see Remark 4.5.

We write $Q \baseext P$ to mean that $Q \supseteq P$, that is, that $Q$ extends $P$ as a program.

A conjunction $D_1 \cap D_2$ is not itself a resolved clause, and $[D_1 \cap D_2] = \{D_1 \cap D_2\} \cup [D_1] \cup [D_2]$. The programs $P \cup \{D_1 \cap D_2\}$ and $P \cup \{D_1, D_2\}$ therefore have the same resolved clauses, and the lemma gives $$P, D_1 \cap D_2 \vdash _O G \qquad \text {iff} \qquad P, D_1, D_2 \vdash _O G.$$

Finally, $\vdash _O$ is closed under cut on atoms: if $P \vdash _O A$ and $P, A \vdash _O G$, then $P \vdash _O G$. The proof is by induction on the height of the derivation of $P, A \vdash _O G$. The atom $A$ contributes only itself to $[P, A]$, so it can be used only by Fact, to conclude $A$, and there the derivation of $P \vdash _O A$ serves instead; at Augment, that derivation is first weakened by Lemma 2.13. Lemma 4.8 extends the property to a wider class of formulae.

3 Base-extension Semantics

We turn now to the semantics itself. The atomic systems of Section 2 are the ground on which the logical constants are given meaning. The semantics is due, in the form we present, to Sandqvist [39], and we record his global completeness theorem before stating the local question that motivates the present paper.

The language of intuitionistic propositional logic is given by $$\varphi , \psi , \chi \;::=\; A \in \mathrm {At}\;\mid \; \bot \;\mid \; \varphi \land \psi \;\mid \; \varphi \lor \psi \;\mid \; \varphi \to \psi ,$$ with $\lnot \varphi \coloneqq \varphi \to \bot$. We write $\Gamma \vdash \varphi$ for intuitionistic derivability of $\varphi$ from $\Gamma$.

The semantics is parametrised by atomic systems. In view of the clausal presentation of Section 2, we identify atomic systems with logic programs throughout.

This is not quite Sandqvist’s class of bases. His are arbitrary sets of atomic rules of level at most two [39]; ours are finite programs, whose rules may be of any finite level and which admit infinite families of rules only through the quantifier. The results quoted from [39] below — Propositions 3.4 and 3.5 and Theorem 3.8 — are stated there for his class. Their proofs transfer unchanged, because they use only two facts about the class of bases: that a base extended by atoms or rules is again a base, and, for completeness, that the flattening base $\base {N}$ constructed below belongs to the class. The base $\base {N}$, in particular, consists of finitely many rule schemas, a few for each subformula of the given formula, and each schema is a single clause of that language; Gheorghiu and Pym [11] carry out the construction for clausal programs.

The meaning of the logical constants is given by an inductively defined relation between bases and formulae — the support relation — whose clauses we now state.

$$\begin{align*} & \supp _{\base {B}} A && \text {iff} \quad \base {B} \vdash _O A \tag {At} \\[1mm] & \supp _{\base {B}} \varphi \to \psi && \text {iff} \quad \varphi \supp _{\base {B}} \psi \tag {$\to $} \\[1mm] & \supp _{\base {B}} \varphi \land \psi && \text {iff} \quad \supp _{\base {B}} \varphi \text { and } \supp _{\base {B}} \psi \tag {$\land $} \\[1mm] & \supp _{\base {B}} \varphi \lor \psi && \text {iff} \quad \text {for every $\base {C} \baseext \base {B}$ and every $A \in \mathrm {At}$,} \notag \\ & && \quad \quad \text {if } \varphi \supp _{\base {C}} A \text { and } \psi \supp _{\base {C}} A \text {, then } \supp _{\base {C}} A \tag {$\lor $} \\[1mm] & \supp _{\base {B}} \bot && \text {iff} \quad \supp _{\base {B}} A \text { for every } A \in \mathrm {At} \tag {$\bot $} \\[1mm] & \Gamma \supp _{\base {B}} \varphi && \text {iff} \quad \text {for every $\base {C} \baseext \base {B}$, if } \supp _{\base {C}} \psi \text { for every } \psi \in \Gamma \text {, then } \supp _{\base {C}} \varphi \tag {Inf} \end{align*}$$

Two structural properties of support are used throughout. The first is immediate from the definition. The second is nearly so. From left to right, it is clause (Inf) at the base $\Bas \cup S$, together with clause (At). From right to left, it requires in addition that $\vdash _O$ be closed under cut on atoms, as recorded at the end of Section 2: if $P \vdash _O B$ for every $B \in S$ and $P, S \vdash _O A$, then $P \vdash _O A$.

A third property is not needed for the proof of the main theorem, but bears on its interpretation in Section 4. It says that every formula is characterised by what it licenses one to conclude, and it generalises a reformulation of the clause for conjunction observed by Gheorghiu et al. [9]. Two consequences of clause (Inf) are used in its proof and thereafter without comment: if $\Gamma \supp _{\BasC } \varphi$ and $\base {D} \baseext \BasC$, then $\Gamma \supp _{\base {D}} \varphi$; and if $\Gamma \supp _{\BasC } \varphi$ and $\supp _{\BasC } \psi$ for every $\psi \in \Gamma$, then $\supp _{\BasC } \varphi$, by taking the extension in (Inf) to be $\BasC$ itself.

Part (i) is the reformulation of Gheorghiu et al. [9]; part (ii) is the corresponding fact for implication. Together they show that every connective, and not only $\bot$ and $\lor$, admits a clause in elimination form.

The principal result of the framework is Sandqvist’s theorem.

Soundness — the direction from right to left — is routine: each rule of natural deduction is shown to be respected by support, and the result follows by induction on derivations. Completeness — from left to right — is the substantive direction, and its proof is illuminating for what follows.

Sandqvist’s argument proceeds by flattening. Fix a formula $\varphi$ and let $\Xi$ be its set of subformulae. Construct an injection $(-)^\flat \colon \Xi \to \mathrm {At}$ that is the identity on atoms ($A^\flat = A$ for $A \in \Xi \cap \mathrm {At}$) and that associates a fresh atom to each complex subformula. From this, one constructs a base $\base {N}$ with two key properties:

• $\chi ^\flat$ and $\chi$ are semantically interchangeable in any extension $\base {N}' \baseext \base {N}$: $$\supp _{\base {N}'} \chi \qquad \text {iff} \qquad \base {N}' \vdash _{O} \chi ^\flat ;$$
• derivability in $\base {N}$ simulates provability in intuitionistic propositional logic, written $\vdash$: $$\base {N} \vdash _O \varphi ^\flat \qquad \text {iff} \qquad \vdash \varphi .$$

Global completeness follows immediately: $$\begin{align*} \supp _{\base {B}} \varphi \text { for all $\base {B}$} \quad &\Longrightarrow \quad \supp _{\base {N}} \varphi \\ &\Longrightarrow \quad \base {N} \vdash _O \varphi ^\flat \tag {$\dagger $} \\ &\Longrightarrow \quad \vdash \varphi . \tag {$\dagger \dagger $} \end{align*}$$

The argument is elementary, constructive, and versatile, having since been deployed to establish completeness for a range of logics [7, 12, 9, 10].

Sandqvist’s theorem is global. It leaves untouched the local question of the introduction: what $\supp _{\base {B}} \varphi$ amounts to in a fixed base.

The question has been partly addressed. Gheorghiu and Pym [11] have generalised the flattening construction by relativising the operator $(-)^\flat$ to a given base $\base {B}$: the fresh atom $\chi ^\flat$ assigned to each complex subformula $\chi$ of $\varphi$ is required not to occur in $\base {B}$. The resulting simulation lemma is exactly local: $$\supp _{\base {B}} \varphi \qquad \text {iff} \qquad \base {N} \cup \base {B} \vdash _O \varphi ^\flat .$$ The equivalence is a genuine local correspondence theorem, but it is purchased at a cost. The flattening operator absorbs the entire logical structure of $\varphi$ into the base $\base {N}$, replacing the formula with a single fresh atom $\varphi ^\flat$. Whatever relation the connectives of $\varphi$ bear to the proof-search procedure is invisible in the theorem itself: the procedure sees only an atom, and the structure of $\varphi$ has been compiled away.

What is wanted, instead, is a correspondence in which the connectives of $\varphi$ remain visible — in which the universal quantifiers of the support clauses correspond to identifiable steps of proof-search, and the procedure is driven by the logical structure of the formula rather than by a precomputed translation of it. The next section supplies it. The encoding is direct: each connective of $\varphi$ is matched with a fixed pattern of the clausal language, and the universal quantifiers in the support clauses turn out to be the eigenvariables of proof-search in disguise.

4 The Encoding and the Main Theorem

The clauses of the support relation, read as they stand, define a procedure: given a formula and a base, decompose the formula according to its outermost connective, generate the clauses for each connective, and consult the base when an atomic case is reached. The procedure is, in everything but name, the operational semantics of a logic programming language. This section makes the identification exact. It begins with the shape of the support clauses.

The clause for disjunction is the following: $$\begin {array}{ll} \supp _{\base {B}} \varphi \lor \psi \quad \text {iff} & \text {for every } \base {C} \baseext \base {B}\ \text {and every atom } A, \\[2pt] & \text {if } \varphi \supp _{\base {C}} A\ \text {and}\ \psi \supp _{\base {C}} A,\ \text {then } \supp _{\base {C}} A. \end {array}$$ The clause says what one may do with a disjunction: conclude any atom $A$ that can be concluded from each disjunct separately. The atom $A$ is an arbitrary conclusion which the disjunction is to deliver, and the disjuncts function as continuations — branches of a case analysis to which control is passed when $A$ is sought. In this sense the clause is a continuation-passing definition. The reading has independent support: Gu et al. [14] interpret the minor premisses of disjunction elimination as continuations, the conclusion being the result of the computation, and analyse Sandqvist’s completeness proof as an implicit CPS transformation.

The description calls for a word of justification, since continuation-passing style (CPS) is in the first instance a transformation on programs [31], and the semantics transforms nothing. What is intended is the type discipline that the transformation induces. Under CPS conversion a value of type $\alpha$ becomes a function that accepts a continuation of type $\alpha \to \rho$ and returns an answer of type $\rho$, so that the type $\alpha$ itself becomes $(\alpha \to \rho ) \to \rho$; abstracting the answer type gives $\forall \rho \,((\alpha \to \rho ) \to \rho )$, and the image of a sum type $\alpha + \beta$ is $\forall \rho \,((\alpha \to \rho ) \to (\beta \to \rho ) \to \rho )$. Griffin [13] observed that, read at the level of types, the conversion is the double-negation translation.

The clause ($\lor$) is this type with the answer type restricted to atoms and the arrows read as consequence in a base. It is in this sense, and not in the sense of a transformation applied to source programs, that we call the clauses continuation-passing. The resulting encoding of the connectives by implication and a propositional quantifier is older than either reading: it is the Russell–Prawitz translation [36, §19], [34], and we use that name when the encoding is in question as a syntactic object rather than as a reading of the semantics.

The other connectives admit the same reading. Falsum is the trivial case: it passes any continuation, since $\supp _{\base {B}} \bot$ licenses the conclusion of every atom. Sandqvist’s clause for conjunction is direct, but Corollary 3.7(i) shows it to be equivalent to an elimination form of the same shape as ($\lor$), an observation first made by Gheorghiu et al. [9]; and Corollary 3.7(ii) shows that implication, too, is characterised by what it licenses one to conclude: from $\varphi \to \psi$ together with $\varphi$, whatever follows from $\psi$. Every connective is thus given by its elimination behaviour. The encoding transcribes that behaviour where Sandqvist’s clauses state it, for $\bot$ and $\lor$; for $\land$ and $\to$, whose clauses are direct, the encoding is direct also.

CPS-shaped definitions translate directly into clauses of a hereditary Harrop language. The case analysis on continuations becomes a conjunction of implications; the universal quantification over atoms becomes the quantifier over atoms; the procedure of trying the continuation against each disjunct becomes backchaining through the implications. We make this translation explicit.

The encoding follows Sandqvist’s clauses one by one. Conjunction and implication, whose clauses are direct, are encoded by the corresponding connectives of the clausal language; falsum and disjunction, whose clauses are elimination conditions quantifying over atoms, are encoded by quantified formulae of the same shape. For $\bot$, $\to$, and $\lor$ the result is the Russell–Prawitz translation. Conjunction, which that translation encodes in elimination form, is here taken directly, the clausal language having it as a primitive; for this reason we speak of a variant of that translation.

Nothing turns on the choice of the direct forms. Corollary 3.7 shows that Sandqvist’s clauses for conjunction and implication are equivalent to their elimination forms, and the theorem holds equally for the corresponding encodings, $\forall X\,((\enc {\varphi } \cap \enc {\psi } \supset X) \supset X)$ and $\forall X\,(\enc {\varphi } \cap (\enc {\psi } \supset X) \supset X)$, by arguments modelled on the case of disjunction below. We do not need these alternatives, and omit the verification. The direct forms are chosen because they are the natural ones, and because they make the corresponding cases of the proof short.

The direct encoding of implication is the reason for which the clausal language admits compound clause heads. Whenever an implication occurs to the left of another, its encoding $\enc {\varphi } \supset \enc {\psi }$ must be installed in a base by Augment, and its head $\enc {\psi }$ is in general compound. It is the encoding adopted in the short version of this paper [8]. No substitution of compound formulae for atoms is involved in its treatment — a substitution which, as Remark 4.5 shows, is in any case unavailable.

The universal quantifier $\forall X$ in the clauses for $\bot$ and $\lor$ reflects, at the syntactic level, the universal quantification over atoms in the corresponding semantic clauses. Under the operational semantics of Section 2, $X$ is instantiated only with atoms, and the instantiation is governed by the eigenvariable discipline of Generic: a single fresh witness suffices. The infinity that the set-theoretic reading of the support clauses appeared to require has become a single name-introduction step, standard in the proof theory of quantification.

The main theorem of the paper is that the encoding is faithful: to be supported in a base is for the encoded goal to succeed against that base as a program.

The left-hand side is defined by quantification over every extension of the base and every atom; the right-hand side, by six rules of search. The theorem says that they are one relation.

Sandqvist’s example from the introduction shows the theorem at work. As a program, the base $\base {R}$ is the single program clause $$\forall X\,((A_1 \supset X) \cap (A_2 \supset X) \supset X),$$ and this is the goal $\enc {A_1 \lor A_2}$ itself. The search for it succeeds at once: Generic introduces a fresh atom $A$, Augment adds $(A_1 \supset A) \cap (A_2 \supset A)$ to the program, and Backchain on the instance of the clause at $A$ leaves, by And, the goals $A_1 \supset A$ and $A_2 \supset A$, each of which is closed by Augment, Backchain, and Fact.

The search for $\enc {A_1} = A_1$ does not succeed. The only resolved clause with head $A_1$ is the instance of the clause at $A_1$, and backchaining on it leaves, among others, the goal $A_2 \supset A_1$: that is, $A_1$ again, from a program in which that instance is still the only clause with head $A_1$. Every attempt regenerates its own goal, and there is no derivation. The disjunction is supported and neither disjunct is, and the search shows why.

The proof of the theorem requires four lemmas, to which we now turn.

Neutral formulae. The encodings produced by Definition 4.1 have a distinctive syntactic feature: the goal-only connective $\cup$ does not occur in them. They are therefore simultaneously definite formulae and goal formulae — a property we name and exploit.

In particular, a base extended by the encoding of a formula is again a base, a fact used repeatedly below. The neutral formulae are exactly the formulae of the clausal language in which $\cup$ does not occur. The elaboration of a neutral formula consists of neutral formulae, each condition on $[P]$ preserving neutrality.

Before proving the encoding faithful, we ask how neutral formulae sit within the language. Atoms are the paradigm of formulae that are at once goals and program clauses, and neutral formulae extend that class; one might expect them to behave like atoms in every respect, and in particular to be substitutable for them. They are not, and the reason is instructive.

Some of the behaviour of atoms does survive, and it is exactly the behaviour that proof-search relies on. The rule Fact, which closes an atomic goal found in the elaborated program, generalises to neutral formulae; so does the admissibility of cut. Throughout, the size of a formula is the number of occurrences of atomic formulae, connectives, and quantifiers in it; note that $F[A/X]$ has the same size as $F$, and that $G \cap G' \supset D$ has the same size as $G \supset (G' \supset D)$.

Neither Lemma 4.6 nor Lemma 4.8 would be well formed without Lemma 4.4(i): in each, $F$ occurs once as a goal and once as a clause of a program. This is where membership in both syntactic classes earns its keep. The arguments are those of the admissibility of cut for uniform proofs [24], adapted to the atomic quantifier.

Proof of the main theorem. We are now in a position to prove Theorem 4.2.

Observe that no compound instantiation of a quantifier occurs anywhere in the proof, in keeping with Remark 4.5: the fresh atom introduced by Generic is moved to the atom supplied by the semantic clause by Lemma 2.14(iii), which is to say by renaming, and the compound formulae required as hypotheses are supplied by identity and discharged by cut.

Since every base extends the empty base, Proposition 3.4 shows that $\varphi$ is supported in every base iff it is supported in the empty base. Theorem 3.8 therefore yields the following.

The theorem identifies support in a fixed base with proof-search in a fixed program. The universal quantifiers in the support clauses — the universal over base extensions in ($\to$) and (Inf), the universals over extensions and atoms in ($\lor$), and the universal over atoms in ($\bot$) — have all become steps of search: Augment adds to the program, and Generic takes a fresh atom. None of them ranges over a completed totality. On this reading the semantics is finitary, mechanical, and exact.

5 Discussion

The result of Section 4 admits a one-line statement: support in a fixed base is proof-search in a fixed program. The remainder of this paper makes three observations about what this statement means and what it makes possible.

The first concerns the meta-theory of base-extension semantics itself. The clauses defining support quantify universally over base extensions and atoms; read set-theoretically, they range over a completed totality of inferential contexts, populated in advance and quantified over from without. That reading is not forced. A constructivist asserts universal claims freely, understanding them as claims to a method, and we do not claim that Sandqvist’s meta-theory anywhere makes a constructively invalid inference. But a reading merely available is one thing and a method exhibited another. A semantics with anti-realist ambitions ought to supply the second.

Theorem 4.2 supplies it. Each universal quantifier in the support clauses is identified with a specific operational mechanism: the universal over base extensions in clauses ($\to$) and (Inf) becomes the augmentation of the program in Augment; the universals over atoms in ($\lor$) and ($\bot$) become the freshness condition in Generic. None of these mechanisms ranges over a completed totality. Each is a single step, standard in the proof theory of quantification. The semantics is constructive not merely in aspiration but in execution.

The set-theoretic and the constructive readings of the quantifiers agree on which formulae are supported in which bases (Remark 3.3); the theorem does not separate them extensionally. What it fixes is the intensional content of support: what it is to verify $\supp _{\base {B}} \varphi$. On the first reading, it is the truth of a universal claim about a class of inferential contexts; on the second, it is the existence of a successful run of a finite search. The theorem shows that base-extension semantics, read through its own clauses, defines the second.

The second observation concerns the limits of the result, and is perhaps more interesting than the result itself. Theorem 4.2 depends essentially on the higher-level structure of atomic systems — that is, on the availability of hypothetical premisses in atomic rules. Without higher-level rules, the encoding of Section 4 cannot be carried out: hereditary Harrop formulae collapse to Horn clauses, and the elimination-driven clauses of the support relation lose their natural translation. The correspondence between support and proof-search dissolves with them.

This dependence is not a technical artefact; it tracks a genuine logical fact. Sandqvist [38] has shown that restricting base-extension semantics to first-level atomic systems yields a characterisation not of intuitionistic but of classical propositional logic. The same restriction that destroys our encoding also destroys the intuitionistic character of the semantics. The two phenomena are aspects of a single fact: higher-level rules are to atomic systems what hypothetical goals are to logic programming; and the difference between having them and lacking them is the difference between intuitionistic and classical logic. The present paper establishes the intuitionistic half of this correspondence.

The classical side remains open, and the gap is significant. Dummett’s programme leaves room, in principle, for a vindication of classical logic on anti-realist grounds, without prior commitment to bivalence, though Dummett himself doubted that one was to be had and concluded that classical logic should be given up. Sandqvist [37, 38] offers his classical semantics as just such a vindication.

If support in the classical setting is genuinely a coherent anti-realist notion, then it should admit a constructive, search-based reading analogous to the one we have given for the intuitionistic case. If it does not — if the classical correspondence cannot be made computational without falling back on Horn clauses and a model-theoretic reading of the universal quantifiers — then the anti-realist credentials of classical base-extension semantics are not what they have been advertised to be. We leave this question open, but flag it as the natural sequel to the present work, and as a test case for the foundational claims of the broader programme.

The third observation looks outward. Base-extension semantics has been developed for a range of logics beyond intuitionistic propositional logic — first- and higher-order intuitionistic logic [7, 12], intuitionistic multiplicative linear logic [9], the logic of bunched implications [10], and others — and the pattern of the semantic clauses is the same in every case. The meaning of each connective is given by its elimination behaviour, expressed as a universal quantification over base extensions. The shape that drives our encoding is not peculiar to intuitionistic propositional logic: it is constitutive of the framework.

This suggests a research programme. Wherever the elimination-driven shape holds, and wherever a suitable analogue of higher-level atomic systems is available, the present result indicates that support should reduce to proof-search in a corresponding logic programming language. Carrying this out systematically would require, for each logic, identifying the right class of program clauses, the right encoding of formulae as goals, and the right notion of uniform proof. In some cases the candidate is already to hand: for first-order logic, the first-order hereditary Harrop programs of Miller et al. [24]; for intuitionistic multiplicative linear logic, the linear hereditary Harrop programs of Hodas and Miller [18]. The payoff would be substantial: a uniform computational foundation for proof-theoretic semantics, in which the philosophical content of the framework is at every point underwritten by a transparent mathematical object.

Proof-theoretic semantics has long been received — with some justice, given its expository register — as a primarily philosophical undertaking, of interest chiefly to those already persuaded of its anti-realist motivations. The present result, and the programme it sketches, suggests a different reading. Under the surface, and largely without remarking on it, proof-theoretic semantics has been writing computational specifications for the logical constants. On the reading we have given, Sandqvist’s clauses for intuitionistic logic are a logic program; the theorem does not impose that structure but finds it there. Whether the same is true of the framework as a whole is a question we leave open, but one we now have the means to ask precisely.

References

References

[1]

M. Dummett, The Justification of Deduction, in Truth and other Enigmas, Duckworth & Co, 1978, p. 318.

[2]

———, The Logical Basis of Metaphysics, Harvard University Press, 1991.

[3]

———, What Is a Theory of Meaning?, in The Seas of Language, Oxford University Press, 1996.

[4]

F. Ferreira and G. Ferreira, Atomic Polymorphism, The Journal of Symbolic Logic, 78 (2013), pp. 260–274.

[5]

F. Ferreira and G. Ferreira, The faithfulness of atomic polymorphism, Trends in Logic XIII, (2014).

[6]

A. V. Gheorghiu, On an Inferential Semantics for Intuitionistic Sentential Logic, Journal of Logic and Computation, 35 (2025).

[7]

———, Proof-theoretic Semantics for First-order Logic, Logic Journal of the IGPL, 33 (2025).

[8]

———, Support is search. arXiv:2603.13018, 2026. Accessed August 2026.

[9]

A. V. Gheorghiu, T. Gu, and D. J. Pym, Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic, in Automated Reasoning with Analytic Tableaux and Related Methods — TABLEAUX, R. Ramanayake and J. Urban, eds., Springer, 2023, pp. 367–385.

[10]

———, Proof-theoretic Semantics for the Logic of Bunched Implications, Studia Logica, (2025).

[11]

A. V. Gheorghiu and D. J. Pym, Definite Formulae, Negation-as-Failure, and the Base-extension Semantics for Intuitionistic Propositional Logic, Bulletin of the Section of Logic, (2023).

[12]

———, Proof-theoretic Semantics for Second-order Logic. arXiv preprint, August 2025.

[13]

T. G. Griffin, A formulae-as-types notion of control, in Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’90), ACM, 1990, pp. 47–58.

[14]

T. Gu, D. J. Pym, E. Ritter, and E. Robinson, Continuations and Completeness in Proof-theoretic Semantics, 2026. arXiv:2605.04689.

[15]

L. Hallnäs and P. Schroeder-Heister, A Proof-theoretic Approach to Logic Programming: I. Clauses as Rules, Journal of Logic and Computation, 1 (1990), pp. 261–283.

[16]

———, A Proof-theoretic Approach to Logic Programming: II. Programs as Definitions, Journal of Logic and Computation, 1 (1991), pp. 635–660.

[17]

R. Harrop, Concerning formulas of the types $A \to B \lor C$, $A\to (Ex) B (x)$ in intuitionistic formal systems , The Journal of Symbolic Logic, 25 (1960), pp. 27–32.

[18]

J. S. Hodas and D. Miller, Logic programming in a fragment of intuitionistic linear logic, Information and Computation, 110 (1994), pp. 327–365.

[19]

R. Kowalski, Logic for Problem Solving, no. 7 in Artificial Intelligence Series, North-Holland, New York, 1979.

[20]

D. Miller, A Logical Analysis of Modules in Logic Programming, The Journal of Logic Programming, 6 (1989), pp. 79–108.

[21]

———, Abstract syntax and logic programming, in Logic Programming: Proceedings of the First and Second Russian Conferences on Logic Programming, vol. 592 of Lecture Notes in Artificial Intelligence, Springer, 1992, pp. 322–337.

[22]

———, Proof Theory and Logic Programming: Computation as Proof Search, Cambridge University Press, Cambridge, 2025.

[23]

D. Miller and G. Nadathur, Programming with Higher-Order Logic, Cambridge University Press, Cambridge, 2012.

[24]

D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, 51 (1991), pp. 125–157.

[25]

G. Mints, Gentzen-type systems and resolution rules Part I: Propositional logic, in Computer Logic—COLOG-88, P. Martin-Löf and G. Mints, eds., Lecture Notes in Computer Science, Springer, 1988, pp. 198–231.

[26]

T. Piecha, Completeness in Proof-theoretic Semantics, in Advances in Proof-theoretic Semantics, Springer, 2016, pp. 231–251.

[27]

T. Piecha, W. de Campos Sanz, and P. Schroeder-Heister, Failure of Completeness in Proof-theoretic Semantics, Journal of Philosophical Logic, 44 (2015), pp. 321–335.

[28]

T. Piecha and P. Schroeder-Heister, Atomic Systems in Proof-Theoretic Semantics: Two Approaches, in Epistemology, Knowledge and the Impact of Interaction, Ángel Nepomuceno Fernández, O. P. Martins, and J. Redmond, eds., Springer Verlag, 2016.

[29]

———, The Definitional View of Atomic Systems in Proof-theoretic Semantics, in The Logica Yearbook 2016, College Publications London, 2017, pp. 185–200.

[30]

———, Incompleteness of Intuitionistic Propositional Logic with Respect to Proof-theoretic Semantics , Studia Logica, 107 (2019), pp. 233–246.

[31]

G. D. Plotkin, Call-by-name, call-by-value and the $\lambda$-calculus, Theoretical Computer Science, 1 (1975), pp. 125–159.

[32]

D. Prawitz, Ideas and Results in Proof Theory, in Studies in Logic and the Foundations of Mathematics, vol. 63, Elsevier, 1971, pp. 235–307.

[33]

———, Towards a Foundation of a General Proof Theory, in Studies in Logic and the Foundations of Mathematics, vol. 74, Elsevier, 1973, pp. 225–250.

[34]

———, Natural Deduction: A Proof-theoretical Study, Dover Publications, 2006 [1965].

[35]

D. J. Pym and E. Ritter, Reductive Logic and Proof-search: Proof Theory, Semantics, and Control, Oxford University Press, 2004.

[36]

B. Russell, The Principles of Mathematics, Cambridge University Press, Cambridge, 1903.

[37]

T. Sandqvist, An Inferentialist Interpretation of Classical Logic, PhD thesis, Uppsala University, 2005.

[38]

———, Classical Logic without Bivalence, Analysis, 69 (2009), pp. 211–218.

[39]

———, Base-extension Semantics for Intuitionistic Sentential Logic, Logic Journal of the IGPL, 23 (2015), pp. 719–731.

[40]

P. Schroeder-Heister, Validity Concepts in Proof-theoretic Semantics, Synthese, 148 (2006), pp. 525–571.

[41]

———, Proof-Theoretic versus Model-Theoretic Consequence, in The Logica Yearbook 2007, M. Pelis, ed., Filosofia, 2008.

[42]

———, Proof-Theoretic Semantics, in The Stanford Encyclopedia of Philosophy, E. N. Zalta, ed., Metaphysics Research Lab, Stanford University, Spring 2018 ed., 2018.

[43]

W. Stafford, Proof-Theoretic Semantics and Inquisitive Logic, Journal of Philosophical Logic, (2021).