Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic

1 Introduction

The definition of a system of logic may be given proof-theoretically as a collection of rules of inference that, when composed, determine proofs; that is, formal constructions of arguments that establish that a conclusion is a consequence of some assumptions:

$$\dfrac{\text{Established Premiss}_1 \quad \cdots \quad \text{Established Premiss}_k}{\text{Conclusion}} \Downarrow$$

The systematic use of symbolic and mathematical techniques to determine the forms of valid deductive argument defines deductive logic: conclusions are inferred from assumptions.

This is all very well as a way of defining what proofs are, but it relatively rarely reflects either how logic is used in practical reasoning problems or the method by which proofs are found. Rather, proofs are more often constructed by starting with a desired, or putative, conclusion and applying the rules of inference 'backwards'. In this usage, the rules are sometimes called reduction operators, read from conclusion to premisses, and denoted

$$\dfrac{\text{Sufficient Premiss}_1 \quad \cdots \quad \text{Sufficient Premiss}_k}{\text{Putative Conclusion}} \Uparrow$$

Constructions in a system of reduction operators are called reductions. This paradigm is known as reductive logic. The space of reductions of a putative conclusion is larger than its space of proofs, including also failed searches—Pym and Ritter [22] have studied the reductive logic for intuitionistic and classical logic in which such objects are meaningful entities.

As one fixes more and more control structure relative to a set of reduction operators, which determining what reductions are made at what time, one increasingly delegates work to a machine. The extreme case is logic programming (LP) in which such controls are fully specified. This view is, perhaps, somewhat obscured by the usual presentation of Horn-clause LP with SLD-resolution—see, for example, Kowalski [14] and Lloyd [17]—but it is explicit in work by Miller et al. [19, 20]. What makes this work is that one restricts to the hereditary Harrop fragment of a logic in which contexts contain only definite formulae—essentially, formulae in which disjunction only appears negatively. In LP, one typically thinks of the formulae in the context of a sequent as definitional, which underpins its use in symbolic artificial intelligence.

While deductive logic is suitable for considering the validity of propositions relative to sets of axioms, reductive logic is suitable for considering the meaning of propositions relative to systems of inference. That the semantics of a statement is determined by its inferential behaviour is known as inferentialism (see Brandom [2]), which has a mathematical realization as proof-theoretic semantics (P-tS).

In P-tS, the meaning of the logical connectives is usually derived from the rules of a natural deduction system for the logic—for example, typically, one uses Gentzen's [32] NJ for intuitionistic logic. Meanwhile, the meanings of atomic propositions is supplied by an atomic system—a set of rules over atomic propositions. For example, taken from Sandqvist [26], the meaning of the proposition 'Tammy is a vixen' can be understood as arising from the following rule:

$$\dfrac{\text{Tammy is a fox} \quad \text{Tammy is female}}{\text{Tammy is a vixen}}$$

Sandqvist [29] gave a P-tS for intuitionistic propositional logic (IPL) called base-extension semantics (B-eS). It proceeds by a judgement called support, parameterized by atomic systems, that defines the logical constants whose base case, the meaning of atoms, is given by derivability in an atomic system.

There is an intuitive relationship between P-tS and LP: the way in bases are definitional in P-tS is precisely how sets of definite formulae are definitional in LP. Schroeder-Heister and Hallnäs [9, 10] have used this relationship to address questions of harmony and inversion in P-tS.

In this paper, we show that the completeness of IPL for the B-eS can be understood in terms of the operational view of definite formulae. Miller [19] gave this operational view of the hereditary Harrop fragment of IPL a proof-theoretic denotational semantics which proceeds by a least fixed point construction over the Herbrand base. A set of definite formulae parameterizes the construction. By thinking of this set as a base, we prove the completeness of IPL for the aforementioned B-eS by passing through the denotational semantics.

This work exposes an interpretation of negation in P-tS as a manifestation of the negation-as-failure (NAF) protocol. The P-tS of negation is a subtle issue—see, for example, Kürbis [16]. Meanwhile, in LP, the relationship between provability and refutation is made through NAF: a statement $\neg\phi$ is established precisely when the system fails to find a proof for $\phi$. The completeness argument for IPL in this paper shows that negation in B-eS can be understood in terms of the failure to find a proof. Hence, from the perspective of B-eS, it is not the case, as advanced by Frege [6] and endorsed by Dummett [4], that denying a statement $\phi$ is equal to asserting the negation of $\phi$. Instead, denial in P-tS is conceptually prior to negation. In this way, through the lens of reductive logic, P-tS may be regarded as practising a form of bilateralism—the philosophical practice of giving equal consideration to dual concepts such as assertion and denial, truth and falsity, and so on. Of course, bilateralism with respect to negation in logic is a subject that received serious attention in the literature—see, for example, Smiley [31], Rumfitt [25], Francez [5], Wansing [35], and Kürbis [16].

The paper brings together the following fields: proof-theoretic semantics, reductive logic, and logic programming. Some such connexions have already been witnessed in the literature—see, for example, Hallnäs and Schroeder-Heister [9, 10]. The value is that we can mutually use one to explicate phenomena in the other, such as understanding the meaning of negation in terms of NAF. That is not to argue in favour of NAF as an explanation of negation, but only that it manifests in the operational account of B-eS provided by the LP perspective.

The paper has three parts. In the first part, Section 2, we give the relevant background on IPL: Section 2.1 contains the syntax and terminology that we adopt for IPL; Section 2.2 defines the hereditary Harrop fragment (i.e., definite formulae) and gives their operational reading. In the second part, Section 3, we summarize the B-eS for IPL as given by Sandqvist [29]: in Section 3.1 we define the support relation giving the semantics, and in Section 3.2 we summarize the existing proof of completeness. In the third part, Section 4, we study B-eS from the perspective of the operational reading of definite formulae: Section 4.1 relates atomic systems and sets of definite formulae; Section 4.2 proves completeness argument for IPL for the B-eS through the operational reading of definite formulae; and, Section 4.3 discusses how this perspective manifests negation-as-failure as an explanation of the proof-theoretic meaning of negation. The paper concludes in Section 5 with a summary of our results and a discussion of future work.

2 Intuitionistic Propositional Logic

2.1 Syntax and Consequence

There are various presentations of intuitionistic propositional logic (IPL) in the literature. We begin by fixing the relevant concepts and terminology used in this paper.

2.2 The Hereditary Harrop Fragment

The hereditary Harrop fragment of IPL admits an operational reading that we use to deliver the completeness of a proof-theoretic semantics for IPL. This section closely follows work by Miller [19] (see also Harland [11]).

The propositional hereditary Harrop formulae are generated by the following grammar in which $A \in \mathcal{A}$ is an atomic proposition, $D$ is a definite formula, and $G$ is a goal formula:

$$D \;::=\; A \;\mid\; G \to A \;\mid\; D \land D$$ $$G \;::=\; A \;\mid\; D \to G \;\mid\; G \land G \;\mid\; G \lor G$$

A set of definite formulae $P$ is a program—typically, it is a finite set, but we shall have cause to consider infinite sets. The set of all programs is $\mathcal{P}$.

We call a sequent $P \,.\, G$, in which $P$ is a program and $G$ is a goal, a query. The hereditary Harrop fragment of IPL admits an operational reading which renders it a logic programming language, here called hHLP. The operational semantics of hHLP is given by uniform proof-search for $P \,.\, G$ in a sequent calculus for IPL—see Miller et al. [20].

For purely technical reasons, we require a decomposition function $\mathrm{cl}({-}) : \mathcal{P} \to \mathcal{P}$ that will unpack conjunctions. Let $\mathrm{cl}(P)$ be the least set satisfying the following:

• $P \subseteq \mathrm{cl}(P)$
• If $D_1 \land D_2 \in \mathrm{cl}(P)$, then $D_1 \in \mathrm{cl}(P)$ and $D_2 \in \mathrm{cl}(P)$.

Importantly, hHLP is complete for the hereditary Harrop fragment of IPL; that is, $P \,.\, G$ has a successful execution iff it is a consequence of IPL—see Miller [20].

The standard frame semantics for IPL by Kripke [15] forms a model-theoretic semantics for hHLP. However, the hereditary Harrop fragment is sufficiently restrictive that we may simplify the semantics in a useful way.

We desire a particular interpretation $J$ such that the following holds:

$$J, P \models G \quad \text{iff} \quad P \vdash G$$

To this end, we consider a function $T$ from interpretations to interpretations that corresponds to unfolding derivability in a base:

$$T(I)(P) \;:=\; \{A \mid A \in \mathrm{cl}(P)\} \;\cup\; \{A \mid (G \to A) \in \mathrm{cl}(P) \text{ and } I, P \models G\}$$

Interpretations form a lattice under point-wise union, point-wise intersection, and point-wise subset; the bottom of the lattice is given by $I_\bot : P \mapsto \emptyset$. It is easy to see that $T$ is monotonic and continuous on this lattice, and, by the Knaster–Tarski Theorem [1], its least fixed-point is given as follows:

$$T^\omega I_\bot \;:=\; I_\bot \sqcup T(I_\bot) \sqcup T^2(I_\bot) \sqcup \cdots$$

Intuitively, each application of $T$ concerns the application of a clause so that $T^\omega I_\bot$ corresponds to arbitrarily many applications.

3 Base-extension Semantics

In this section, we give a brief, but complete, synopsis of the base-extension semantics (B-eS) for IPL as introduced by Sandqvist [29]. The semantics proceeds through a support relation parametrized by certain atomic systems, called bases. There are related base-extension semantics for classical logic—see Sandqvist [27, 28] and Makinson [18].

We differ slightly in presentation from Sandqvist [29]. First, we refer to more the possibility of more general definitions (e.g., considering $n$th level atomic systems for $n > 2$). Second, we make use of derivations as mathematical objects. Third, we parameterize support over a notion of base called a basis, a class of atomic systems. These differences help bridge the gap between the earlier work and the connexions to logic programming in this paper. It also sets the B-eS for IPL within the wider literature of P-tS from which we draw the generalizations.

3.1 Support in a Base

A common idea in proof-theoretic semantics—the paradigm of meaning in which B-eS operates—is that the meaning of atomic propositions is given by sets of atomic rules governing their inferential behaviour. Piecha and Schroeder-Heister [30, 21] have given a useful inductive hierarchy of them.

The support relation satisfies some important expected properties, such as the following:

This summarizes the B-eS for IPL. Sandqvist [29] proved the soundness of IPL for the B-eS by showing that validity admits all the rules of NJ. His proof of completeness is more complex. In essence, Sandqvist [29] proved completeness of IPL for the B-eS by constructing a bespoke atomic system $N$ to a given validity judgement that allows us to simulate an NJ-derivation for the sequent in question. We present the main ideas here as we refer to them in Section 4.2.

3.2 Completeness of IPL via a Natural Base

We want to show that $\Gamma \Vdash \gamma$ implies $\Gamma \vdash \gamma$. We understand the latter in terms of provability in NJ. Therefore, we associate to each formula $\rho$ in the sequent $\Gamma \,.\, \gamma$ a unique atom $r$ and construct a base $N$ emulating NJ such that $r$ behaves in $N$ as $\rho$ behaves in NJ.

For example, let $\Gamma \,.\, \gamma$ contain $\rho := p \land q$. The rules governing $\rho$ are the conjunction introduction and elimination rules of NJ, so we require $N$ to contain the following rules in which $r$ is alien to $\Gamma \,.\, \gamma$:

$$\dfrac{p \quad q}{r} \qquad \dfrac{r}{p} \qquad \dfrac{r}{q}$$

These rules are designed such that $r$ behaves in $N$ precisely as $\rho$ does in NJ. That is, they emulate the conjunction rules. The shorthand for $r$ is $(p \land q)^\flat$—that is, $r = \rho^\flat$—so that the above rules may be expressed more clearly as follows:

$$\dfrac{p \quad q}{(p \land q)^\flat} \qquad \dfrac{(p \land q)^\flat}{p} \qquad \dfrac{(p \land q)^\flat}{q}$$

For clarity, we give another example. Suppose $\Gamma \,.\, \gamma$ also contains $\sigma := p \to q$, then $N$ contains rules that emulate the implication introduction and elimination rules of NJ for $\sigma$ using an atom $s := \sigma^\flat := (p \to q)^\flat$ alien to $\Gamma$ and $\gamma$. That is, $N$ contains the following rules:

$$\dfrac{[p]}{q \atop (p \to q)^\flat} \qquad \dfrac{p \quad (p \to q)^\flat}{q}$$

The details of how $N$ is constructed and how it delivers completeness are below.

Fix a sequent $\Gamma \,.\, \gamma$. To every sub-formula $\phi$ of $\Gamma \,.\, \gamma$ associate a unique atomic proposition $\phi^\flat$ as follows:

• if $\phi \notin \mathcal{A}$, then $\phi^\flat$ is an atom that does not occur in $\Gamma \,.\, \gamma$;
• if $\phi \in \mathcal{A}$, then $\phi^\flat = \phi$.

The right-inverse of $-^\flat$ is $-^\sharp$ and both functions act on sets point-wise:

$$\Sigma^\flat := \{\phi^\flat \mid \phi \in \Sigma\} \qquad P^\sharp := \{p^\sharp \mid p \in P\}$$

Let $N$ be the atomic system containing precisely the rules of Figure 5 for any $\phi, \psi$ occurring in $\Gamma \,.\, \gamma$ and any $p \in \mathcal{A}$. These rules are precisely such that $\phi^\flat$ behaves in $N$ as $\phi$ does in NJ. Note that, for any validity judgement, the atomic system $N$ thus generated is indeed a Sandqvist base.

In this set-up, Sandqvist [29] establishes three properties that collectively deliver completeness.

These lemmas collectively suffice for completeness:

4 Definite Formulae, Proof-search, and Completeness

There is an intuitive encoding of atomic rules as formulae. More precisely, as definite formulae. Under this encoding, the bases which deliver B-eS live within the hereditary Harrop fragment of IPL. The latter has a simple operational reading via proof-search for uniform proofs (see Section 2.2) that enables a proof-theoretic denotational semantics—the least fixed point construction. We use this well-understood phenomenon to deliver the completeness of IPL with respect to Sandqvist's B-eS [29]—see Section 3.

Doing this reveals a subtle interpretation of the meaning of negation in terms of the negation-as-failure protocol. A reductive logic view of the denial of a formula is the failure to find a proof of it. Thus, according to the view of B-eS arising from the account passing through the operational reading of definite formulae, in B-eS denial is conceptionally prior to negation and both require equal consideration.

4.1 Atomic Systems vs. Programs

Intuitively, atomic systems in B-eS are definitional in precisely the same way as programs in hHLP are definitional. To illustrate this, we must systematically move between them, which we do by encoding atomic systems as programs.

Let $\lfloor - \rfloor$ be as follows:

• The encoding of a zeroth-level rule is: $$\left\lfloor \dfrac{}{c} \right\rfloor := c$$
• The encoding of a first-level rule is: $$\left\lfloor \dfrac{p_1 \quad \cdots \quad p_n}{c} \right\rfloor := (p_1 \land \cdots \land p_n) \to c$$
• The encoding of an $n$th-level rule is: $$\left\lfloor \dfrac{[\Sigma_1]\; p_1 \quad \cdots \quad [\Sigma_n]\; p_n}{c} \right\rfloor := \bigl((\lfloor\Sigma_1\rfloor \to p_1) \land \cdots \land (\lfloor\Sigma_n\rfloor \to p_n)\bigr) \to c$$

For example, $\to\mathrm{I}^\flat$ in Figure 5 yields the following schematically:

$$(\phi^\flat \to \psi^\flat) \to (\phi \to \psi)^\flat$$

The hierarchy of atomic systems provided by Piecha and Schroeder-Heister [30, 21] (Definition 3.1) precisely corresponds to the inductive depth of the grammar for hereditary Harrop formulae—that is, if $\mathcal{A}$ is an $n$th-level atomic system, then

$$\vdash_{\mathcal{A}} p \quad \text{iff} \quad \lfloor\mathcal{A}\rfloor \vdash p$$

Therefore, we may suppress the encoding function, and henceforth use atomic systems and programs interchangeably—that is, we may write $\mathcal{A} \vdash p$ to denote $\lfloor\mathcal{A}\rfloor \vdash p$.

Of course, in the Sandqvist basis, we are limited to properly second-level atomic systems, but the grammar of definite clauses can handle considerably more. Indeed, the work below suggests that completeness holds for $n$th-level atomic systems for $n \geq 2$.

Formally, to say that bases are definitional in the sense of programs, we mean the following:

$$\Vdash_B \phi \quad \text{iff} \quad N \cup B \vdash \phi^\flat \tag{$*$}$$

Here $N$ contains rules governing $\phi$ when the formula is complex—that is, $\phi$ is a sub-formula of a sequent $\Gamma \,.\, \psi$ which generates $N$—and arbitrary otherwise.

It is important that we use $\phi^\flat$ rather than $\phi$ in $(*)$. It is certainly not the case that bases behave exactly as contexts; that is, we do not have the following equivalence:

$$\Vdash_B \phi \quad \text{iff} \quad B \vdash \phi \tag{$**$}$$

That this generalization fails is shown by the following counter-example:

4.2 Completeness of IPL via Logic Programming

We may prove completeness of IPL with respect to the B-eS by passing through hHLP as follows:

$$T^\omega I_\bot,\, N \models \phi^\flat \;\xleftarrow{\text{Lem. 4.3}}\; \Vdash_N \phi \;\xrightarrow{\text{Lem. 4.4}}\; \vdash \phi$$

(The middle step uses Lemma 2.9 to pass between $T^\omega I_\bot, N \models \phi^\flat$ and $N \vdash \phi^\flat$.)

The intuition of the completeness argument is three-fold: firstly, that $N$ is to $\phi^\flat$ as NJ is to $\phi$; secondly, the use of a rule in a base corresponds to the use of a clause in the corresponding program; thirdly, execution in $N$ corresponds to proof(-search) in NJ. In this set-up, the $T^\omega$ construction captures the construction of a proof: the application of a rule corresponds to a use of $T$, the iterative application of rules corresponds to the iterative application of $T$—that is, to $T^\omega$.

It remains to prove the claims and completeness. Fix a sequent $\Gamma \,.\, \phi$ and let $-^\flat$ and $N$ be constructed as in Section 3.2 for this sequent. Let $\Delta$ be an arbitrary set of sub-formulae of the sequent and $\psi$ an arbitrary subformula of the sequent.

4.3 Negation-as-Failure

A reduction in a proof system is constructed co-recursively by applying the rules of inference backwards. Even though each step corresponds to the application of a rule, the reduction can fail to be a proof as the computation arrives at an irreducible sequent that is not an instance of an axiom in the logic. For example, in hHLP, one may compute the following:

$p \,.\, q$
$p \,.\, p \lor q$   $\Uparrow$ OR
$\emptyset \,.\, p \to (p \lor q)$   $\Uparrow$ LOAD

This reduction fails to be a proof, despite every step being a valid inference, since the initial sequent $p \,.\, q$ is not an instance of IN (there is no rule for $q$ in the empty program). In reductive logic, such failed attempts at constructing proofs are not meaningless: Pym and Ritter [22] have provided a semantics of the reductive logic of IPL in which such reductions are given meaning by using hypothetical rules—that is, the construction would succeed in the presence of the following rule:

$$\dfrac{p}{q}$$

The categorical treatment of this semantics has them as indeterminates in a polynomial category—this adumbrates current work by Pym et al. [23], who have shown that the B-eS is entirely natural from the perspective of categorical logic. The use of such additional rules to give semantics to constructions that are not proofs directly corresponds to the use of atomic systems in the B-eS for IPL; for example, let $\mathcal{A}$ be the atomic system containing the rule above, then the judgement $p \Vdash_{\mathcal{A}} q$ obtains. Altogether, this suggests a close relationship between B-eS and reductive logic, which manifests with the operational reading of definite clauses and their relationship to atomic rules in Section 4.

Within P-tS, negation is a subtle issue—see Kürbis [16]. We may use the perspective of LP developed herein to review the meaning of absurdity ($\bot$). There is no introduction rule for $\bot$ in NJ. One may not construct a proof of absurdity without it already being, in some sense, assumed; for example, $\phi,\, \phi \to \bot \vdash \bot$ obtains because the context $\{\phi,\, \phi \to \bot\}$ is already, in some sense, absurd. We may use LP to understand what that sense is. To simplify matters, observe that the judgement $\Gamma \vdash \bot$ is equivalent to $\vdash \phi \to \bot$ for some formula $\phi$. Therefore, we may restrict attention to negations of this kind to understand the meaning of absurdity.

By Theorem 3.6 (Soundness) and Lemma 4.4 (Simulation), we see that the converse of Lemma 4.3 holds. Therefore,

$$\Vdash \neg\phi \quad \text{iff} \quad T^\omega I_\bot,\, N \models (\neg\phi)^\flat$$

Unfolding the semantics, this is equivalent to $T^\omega I_\bot,\, N \cup \{\phi^\flat\} \models \bot^\flat$. Thus, the sense in which $\phi$ is absurd is that its interpretation under $T^\omega I_\bot$ contains absurdity; that is, $\phi$ is absurd iff $\bot^\flat \in T^\omega I_\bot(\phi)$. What does this tell us about the meaning of $\neg\phi$? Since there is no proof of $\bot^\flat$, we have that the meaning of $\neg\phi$ is that there is no proof of $\phi^\flat$ in $N$. This is the negation-as-failure principle. How does it yield the clause for $\bot$ in Figure 4?

Passing through $(*)$ in Section 4.1,

$$\Vdash_B \bot \quad \text{iff} \quad N \cup B \vdash \bot^\flat$$

Since there is no introduction rule for $\bot^\flat$ in $N$, it must be that $B$ derives it. Thus, there is a rule in $B$ of the following form:

$$\dfrac{[\Sigma_1]\; p_1 \quad \cdots \quad [\Sigma_n]\; p_n}{\bot^\flat}$$

To simplify matters, we introduce alien $q$ and $\bar{q}$ as 'conjunctions' of some subset $q_1, \ldots, q_k$ and $q_{k+1}, \ldots, q_n$ of $p_1, \ldots, p_n$ in the inferentialist sense. That is, we introduce the following, where $\Pi_i = \Sigma_j$ iff $q_i = p_i$ for $i, j \in \{1, \ldots, n\}$:

$$\dfrac{[\Pi_1]\; q_1 \quad \cdots \quad [\Pi_k]\; q_k}{q} \qquad \dfrac{[\Pi_{k+1}]\; q_{k+1} \quad \cdots \quad [\Pi_n]\; q_n}{\bar{q}}$$

Doing this allows us to replace the above rule with the following:

$$\dfrac{q \quad \bar{q}}{\bot^\flat}$$

In this case, the inferential behaviour of $q$ and $\bar{q}$ is that they are contradictory propositions: together, they infer absurdity.

In this way, negation is implicit in atoms. What is significant from this analysis is that the semantics of $\bot$ requires us to observe that there is no proof of it and thus extend the space with proofs of contradictory $q$ and $\bar{q}$. If they are proved in $B$, then one has proved absurdity; if $B$ has proved absurdity, then one has proofs for each of these. The subtlety is that since we do not have negation explicit in our atoms, we only admit the principle that some atoms are contradictory. If we prove all atoms, then we prove these contradictory atoms; and, if we prove these contradictory atoms, then we have proved absurdity. This justifies the clause for $\bot$:

$$\Vdash_B \bot \quad \text{iff} \quad \Vdash_B p \text{ for any } p \in \mathcal{A}$$

Piecha and Schroeder-Heister [30, 21] have argued that there are two perspectives on atomic systems: the knowledge view and the definitional view. This becomes clear according to various ways in which a program may be regarded in LP. The negation-as-failure protocol makes use of the definitional perspective; its analogue in terms of knowledge is the closed-world assumption. In this case, a knowledge base treats everything that is not known to be valid as invalid. There is significant literature about the closed-world assumption that may be useful for understanding P-tS and what it tells us about reasoning—see, for example, Clark [3], Reiter [24], and Kowalski [14, 13], and Harland [11, 12].

5 Conclusion

Proof-theoretic semantics is the paradigm of meaning based on proof (as opposed to truth). Essential to this approach is the use of atomic systems, which give meaning to atomic propositions. Base-extension semantics is a particular instance of proof-theoretic semantics that proceeds by an inductively defined judgement whose base case is given by provability in an atomic system. It may be regarded as capturing the declarative content of proof-theoretic semantics in the Dummett–Prawitz tradition—see Gheorghiu and Pym [8]. Sandqvist [27] has given a base-extension semantics for intuitionistic propositional logic. Completeness follows by constructing a special bespoke base in which the validity of a complex proposition simulates a natural deduction proof of that formula.

In the base-extension semantics, the meaning of the logical constants is derived from the rules of NJ, while the atomic systems give the meaning of atomic propositions. These atomic systems, which include Sandqvist's special bases that delivers completeness, all sit within the hereditary Harrop fragment of IPL. The significance of this is that an effective operational reading of definite formulae renders them meaning-conferring in a sense analogous to the use of atomic systems. Moreover, this operational account coheres with the independently conceived notion of derivability in an atomic system. Of course, that atomic systems and programs are intimately related has been studied before—see Schroeder-Heister and Hallnäs [9, 10].

Significantly, the operational reading of the definite formulae allows from a simple proof-theoretic model-theoretic semantics that captures the idea of unfolding the inferential content of a set of definite clauses or an atomic system. In this paper, we have used the operational account of definite formulae to prove the completeness of intuitionistic propositional logic with respect to its base-extension semantics. The aforementioned special base is interpreted as a program so that completeness follows immediately from the existing completeness result of the model-theoretic semantics of the logic programming language. Doing this reveals the subtle meaning of negation in proof-theoretic semantics.

Historically, the negation of a formula is understood as the denial of the formula itself. This is indeed the case in the model-theoretic semantics of IPL—see Kripke [15]. Using the connection to logic programming in this paper, we see that in base-extension semantics, negation is defined by the failure for there to be a proof. Thus, denial is conceptionally prior to negation. In short, base-extension semantics considers the space of reductions, which is larger than the space of proofs, including failed searches. As illustrated above, the connection between logic programming and base-extension semantics is quite intuitive and useful. More specifically, the $T$ operator delivering the semantics of logic programming corresponds to the application of a rule in a proof system; hence, the $T^\omega$ construction is fundamental to proof-theoretic semantics. Since logic programming has been studied for various logics (see, for example, the treatment of BI in Gheorghiu et al. [7]), this suggests the possibility for uniform approaches to setting up base-extension semantics for logics by studying their proof-search behaviours. In particular, work by Harland [11, 12] on handling negation in logic programming may be used to address the difficulties posed by the connective—see Kürbis [16].

It remains to investigate further the connection between proof-theoretic semantics and reductive logic, in general, and base-extension semantics and logic programming, in particular.

Acknowledgements. We are grateful to Edmund Robinson, for suggesting the formula in Example 4.1, and to Elaine Pimentel, Yll Buzoku, and the reviewers of an earlier version of the paper for their helpful comments and feedback.