Proof-theoretic Semantics for First-order Logic

1 Introduction

Traditionally, logic has been developed around the idea that the meaning of linguistic terms in logic (e.g. predication, the logical signs, and so on) is determined by reference to external entities. We call this view denotationalism. A standard account within symbolic logic is model-theoretic semantics (M-tS) in which a logical language is interpreted within abstract algebraic structures $\mathfrak{M}$ called "models". Tarski formalized logical consequence within this framework: a proposition $\phi$ follows from a context $\Gamma$ iff every model of $\Gamma$ is also a model of $\phi$:

$$\Gamma \models \phi \quad \text{iff} \quad \text{for all models } \mathfrak{M},\ \text{if } \mathfrak{M} \models \psi \text{ for all } \psi \in \Gamma \text{, then } \mathfrak{M} \models \phi.$$

Observe that within this conception of logic, truth is conceptually prior to inference.

Arguably, this approach to semantics leaves something to be desired. Prawitz says that explaining the meaning of sentences purely in terms of the conditions under which they are "true" does little to clarify how speakers actually understand them. This is a problem as it seems a reasonable requirement of the semantics of a sentence to do so. Building on this, Dummett says succinctly, "A theory of meaning must explain what it is to understand an expression; and to understand an expression is to be capable of using it correctly." He argues that if meaning were merely a matter of reference, we would have no way to explain how speakers learn the meanings of expressions without already possessing a grasp of the entities to which they refer.

What alternative is there to the denotational or model-theoretic approach? To begin, Prawitz has argued that inference ought be conceptually prior to truth. This sets up the idea that one can ground meaning in terms of inference rather than truth. An idea again succinctly summarized by Dummett: "A grasp of the meaning of a logical constant is manifested in a mastery of the inference rules governing it." The broader philosophical view that meaning is based on inferential roles has been dubbed inferentialism by Brandom. This may be viewed as a particular instantiation of the meaning-as-use paradigm of Wittgenstein, in which "use" is given by inferential role.

This inferential conception of meaning is actually quite standard in how we think about it outside textbooks on symbolic logic. Suppose someone were to ask you for the meaning of the proposition, "Tammy is a vixen." Stating that it means that the object denoted by "Tammy" belongs to the category of objects denoted by "vixen" would be unhelpful. Rather, we may explain that it means "Tammy is female" and "Tammy is a fox". Pushed for clarification, we might explain that the statements stand in the following inferential relationships:

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

In so doing, we have given the meaning of the expression "Tammy is a vixen."

This approach to meaning may be used within a logical language too. Rather than M-tS, we have what Schroeder-Heister has called proof-theoretic semantics (P-tS). It is the approach to meaning based on "proof" rather than "truth". Of course, "proof" here does not merely denote constructions within formal systems, but is understood generally as an object denoting collections of inferences. This shift and its technical details has substantial and subtle mathematical and conceptual consequences.

There is a rich literature on P-tS. We defer to Schroeder-Heister for its broad history. An important point is the following striking, albeit somewhat enigmatic, remarks by Gentzen:

"The introductions represent, as it were, the 'definitions' of the symbols concerned, and the eliminations are no more, in the final analysis, than the consequences of these definitions. This fact may be expressed as follows: In eliminating a symbol, we may use the formula with whose terminal symbol we are dealing only 'in the sense afforded it by the introduction of that symbol.'"

While he does not explicitly state how introduction rules provide meaning to logical connectives, the foundational intuition for logical inferentialism are unmistakably present. They also suggest where to begin in developing such a semantic theory. Consider the inference rules governing conjunction ($\land$):

$$\dfrac{\phi \quad \psi}{\phi \land \psi} \qquad \dfrac{\phi \land \psi}{\phi} \qquad \dfrac{\phi \land \psi}{\psi}$$

They are analogous to the propositions concerning Tammy above, justifying the "and" used there. These rules provide meaning of "$\phi \land \psi$" the same way as the rules above provided the meaning of "Tammy is a vixen". Of course, this does not yet explain the origin of the elimination rules.

There are several branches of research within P-tS. Much of it has followed an account given by Prawitz based on his normalization results for natural deduction. We elide the details as they are not directly relevant to the work in this paper. Here we are concerned with a related formalism called base-extension semantics (B-eS).

In B-eS, one seeks to give the semantics of logical connectives by defining a support relation $\Vdash$ representing a semantic judgment (analogous to the role of satisfaction in M-tS). It differs from M-tS in that one does not evaluate validity relative to models but rather relative to collections of inference rules over atoms known as bases. These rules may include e.g. the following kinds of figures:

$$\dfrac{}{C} \qquad \dfrac{P_1 \quad \cdots \quad P_n}{C} \qquad \dfrac{[\mathbb{P}_1] \quad \cdots \quad [\mathbb{P}_n] \quad P_1 \quad \cdots \quad P_n}{C}$$

where $C, P_1, \ldots, P_n$ are atoms and $\mathbb{P}_1, \ldots, \mathbb{P}_n$ are finite sets of atoms.

A formula $\phi$ follows from a context $\Gamma$ if and only if every $\mathcal{B}$ supporting $\Gamma$ also supports $\phi$; that is,

$$\Gamma \Vdash \phi \quad \text{iff} \quad \text{for all bases } \mathcal{B},\ \text{if } {\Vdash}_{\!\mathcal{B}}\, \psi \text{ for all } \psi \in \Gamma \text{, then } {\Vdash}_{\!\mathcal{B}}\, \phi.$$

Schroeder-Heister has observed that both M-tS and B-eS adhere to the standard dogma of semantics, in which consequence is understood as the transmission of some categorical notion, and he has been a critic of this view. Though B-eS is closely related to M-tS, especially possible world semantics in the sense of Beth and Kripke, it remains subtle.

Sandqvist studied B-eS as a way to present classical logic (CL) without prior commitment to bivalence. By "bivalence" we mean that there are exactly two truth values, True and False. The critique of the denotationalist conception of meaning above renders such a commitment dubious. Nonetheless, classical logic has merit in that, if nothing else, it appears to capture the logical foundations of mathematics rather well. Therefore, Dummett writes:

"In the resolution of the conflict between [the view that generally accepted classical modes of inference ought to be theoretically accommodated, and the demand that any such accommodation be achieved without recourse to bivalence] lies, as I see it, one of the most fundamental and intractable problems in the theory of meaning; indeed, in all philosophy."

This puts Sandqvist's result in perspective: it is a major achievement in both philosophy and mathematical logic. One technical requirement for soundness and completeness is that bases contain rules of the form

$$\dfrac{}{C} \qquad \text{and} \qquad \dfrac{P_1 \quad \cdots \quad P_n}{C}$$

Including rules with discharge results in incompleteness.

Makinson remarks that Sandqvist's proof of completeness is "not very helpful" for understanding the system. Accordingly, he has provided an alternative proof of completeness for classical propositional logic (CPL) by directly relating the proposed B-eS to the logic's existing truth-functional semantics—note that he reverses the terms "soundness" and "completeness" for reasons he discusses. Eckhardt and Pym have used this approach to systematically develop the B-eS for normal modal logic. While Makinson's proof clarifies the classicality of the B-eS for CL, it does so by committing to the model-theoretic interpretation of the logic. In so doing, it forfeits genuinely exposing the inferential nature of the semantics. Rather than demonstrating how inferential reasoning alone recovers classical logic, it sidesteps the issue. Therefore, we seek a completeness proof that also illustrates inferential foundations of the framework.

Sandqvist has also provided a B-eS for intuitionistic propositional logic (IPL). It follows the semantics for CL for the connectives $\land, \to, \bot$ but takes the following clause for disjunction:

${\Vdash}_{\!\mathcal{B}}\, \phi \lor \psi$  iff  for any base $\mathcal{C} \supseteq \mathcal{B}$ and any atom $p$, if $\phi \;{\Vdash}_{\!\mathcal{C}}\, p$ and $\psi \;{\Vdash}_{\!\mathcal{C}}\, p$, then ${\Vdash}_{\!\mathcal{C}}\, p$.

For completeness, the bases must range over sets that include rules with discharge,

$$\dfrac{[\mathbb{P}_1] \quad \cdots \quad [\mathbb{P}_n] \quad P_1 \quad \cdots \quad P_n}{C}$$

The results by Piecha et al. show that intuitionistic logic is incomplete for the same semantics but with a more typical clause for disjunction—viz. ${\Vdash}_{\!\mathcal{B}}\, \phi \lor \psi$ iff ${\Vdash}_{\!\mathcal{B}}\, \phi$ or ${\Vdash}_{\!\mathcal{B}}\, \psi$. Stafford later showed that this is a semantics for variants of Kriesel–Putnam logic.

The clause for disjunction can be justified in several ways. Dummett appears to have been the principal inspiration. The clause also recalls Prawitz's second-order definition of logical signs. A third perspective, followed by Gheorghiu et al., suggests that it arises from treating definitional reflection—in the sense of Hallnäs and Schroeder-Heister—as a closure condition on introduction rules that determines meaning. Of course, definitional reflection can be used either with introduction or with eliminations in the role of definiens—see de Campos Sanz and Piecha. Whatever the case, we note the restriction to quantification over atomic propositions. This remains to be justified philosophically, though the clause does extend to full formulae as expected:

${\Vdash}_{\!\mathcal{B}}\, \phi \lor \psi$  iff  for any base $\mathcal{C} \supseteq \mathcal{B}$ and any formula $\chi$, if $\phi \;{\Vdash}_{\!\mathcal{C}}\, \chi$ and $\psi \;{\Vdash}_{\!\mathcal{C}}\, \chi$, then ${\Vdash}_{\!\mathcal{C}}\, \chi$.

However, starting with this formulation would not yield an inductive definition of support.

What is most notable about the B-eS of intuitionistic logic is the proof of completeness. Sandqvist remarks:

"The mathematical resources required for the purpose are quite elementary; there will be no need to invoke canonical models, König's lemma, or even bar induction. The proof proceeds, instead, by simulating an intuitionistic deduction using basic sentences within a base specifically tailored to the inference at hand."

Specifically, it proceeds by simulating a NJ-derivation, where NJ is the natural deduction system for intuitionistic logic given by Gentzen. Gheorghiu et al. have shown that this approach is quite versatile in the context of constructive logics. Importantly, this approach to completeness clearly reveals how the inferential content of the semantics relates to proof-theoretic expression.

In this paper, we present a modular such completeness proof for both classical and intuitionistic first-order logic. In the first case, such a proof is lacking in the literature, so our work fills a gap. In the second case, we extend existing work to the first-order setting that demands simulating variables inside bases. The actual semantic clauses are the same for both logics; the only difference lies in the notion of base. The modularity of this approach suggests that much greater emphasis should be placed on how the notion of base, which is assumed prior to the definition of logical signs, influences their meaning. We regard this as a crucial and unresolved problem within P-tS.

To deliver this work requires overcoming a couple of challenges. Firstly, to "simulate" NJ-derivations, Sandqvist makes essential use of rules with discharge. Since such rules are not permitted in the B-eS for classical logic, we require some way of simulating classical deductions, including those with implications, without using discharge. To do this, rather than simulate derivations in the sense of Gentzen, we simulate derivations in the sense of Hilbert (see Kleene). This broadens the scope of what can be achieved with a simulation-style proof of completeness. Secondly, the move to first-order logic requires careful treatment of quantified variables in the simulation. We solve this problem by introducing eigenvariables in the simulation and carefully tracking their behaviour.

Roadmap. In Section 2 we give a terse proof-theoretic background to first-order classical and intuitionistic logic to fix some notations. We proceed in Section 3 to give the formal definition of their B-eS. In Section 4 and Section 5 we prove soundness and completeness, respectively. The paper ends in Section 6 with some discussion about the results presented.

Notations. We briefly outline some of the notations used throughout the paper for quick reference; the details are given below. Conventions:

• $x, y, z, \ldots$ denote variables,
• $t, s, r, \ldots$ denote terms,
• $P, Q, \ldots$ denote either predicates or atomic formulas,
• $\phi, \psi, \chi$ denote formulas,
• $\mathbb{P}, \mathbb{Q}, \mathbb{R}, \ldots$ denote (possibly empty, possibly infinite) sets of atoms,
• $\Gamma, \Delta, \Xi, \ldots$ denote (possibly empty, possibly infinite) sets of formulas, and
• $\mathcal{A}, \mathcal{B}, \mathcal{C}, \ldots$ denote atomic systems.

The sets of all variables, terms, atoms, and formulas are $\mathcal{V}, \mathcal{T}, \mathcal{A}$, and $\mathcal{F}$, respectively; the subsets containing only closed elements (where appropriate) are denoted $\mathrm{CL}(\mathcal{T})$, $\mathrm{CL}(\mathcal{A})$, and $\mathrm{CL}(\mathcal{F})$, respectively.

We write $\mathrm{FV}$ to denote the function that takes a term, atom, or formula and returns the set of its free variables. We write $[x \mapsto t]$ to denote a substitution function that replaces all free occurrences of $x$ by $t$.

We use $\bot, \land, \lor, \to, \forall, \exists$ as the logical signs. While $\bot$ is sometimes taken as an atomic formula, especially in the first-order setting, we reserve that terminology for formulas of the form $P(t_1, \ldots, t_n)$, where $P$ is a predicate symbol and $t_1, \ldots, t_n$ are terms. Intuitively, $\bot$ has some meaning that is expressed in terms of such atomic formulas, rendering it semantically complex.

2 Background: First-order Classical and Intuitionistic Logic

We fix denumerable sets of symbols: variables $\mathcal{V}$ ($x,y,z,\ldots$), constants $\mathcal{K}$ ($a,b,c,\ldots$), function symbols $\mathcal{F}_n$ of arity $n$, and predicate symbols $\mathcal{P}_n$ of arity $n$. We use $\bot, \land, \lor, \to, \forall, \exists$ as logical signs and write $\neg\phi$ for $\phi \to \bot$. We treat $\bot$ as semantically complex (not an atom) since it has logical content.

Subformulas of $\phi$ are defined inductively: (i) $\phi$ is a subformula of $\phi$; (ii) if $\phi = \phi_1 \circ \phi_2$ for $\circ \in \{\land, \lor, \to\}$, the subformulas of $\phi_1$ and $\phi_2$ are subformulas of $\phi$; (iii) if $\phi = \forall x\psi$ or $\phi = \exists x\psi$, then $\psi[x \mapsto t]$ for every $t \in \mathrm{CL}(\mathcal{T})$ are subformulas of $\phi$. Only closed formulas are subformulas.

We define classical and intuitionistic consequence via a Frege–Hilbert axiomatization—see Troelstra and Schwichtenberg, Kleene, and Church for extensive historical notes. To this end, we require substitutions. We write $[x \mapsto t]$ to denote a term substitution; i.e. $t'[x \mapsto t]$ denotes the result of uniformly replacing every occurrence of $x$ in $t'$ with $t$. It is clear that the result remains a term. This extends to formulas as expected, where bound variables are not substituted. Carefully distinguishing free and bound variables is essential for a precise formulation of first-order logic. Therefore, let $\mathrm{FV} : \mathcal{F} \to \mathcal{P}(\mathcal{V})$ map a formula $\phi$ to the set of its free variables $\mathrm{FV}(\phi)$. A term, atom, or formula is closed if it has no free variables.

To define classical and intuitionistic consequence we introduce the concept of an axiomatization. Fix a set $\mathbb{X}$ of formula-variables. From formula-variables, one constructs formula-schemes according to the grammar

$$\mathfrak{s}, \mathfrak{t} \;::=\; X \in \mathbb{X} \;\mid\; \bot \;\mid\; \mathfrak{s} \land \mathfrak{t} \;\mid\; \mathfrak{s} \lor \mathfrak{t} \;\mid\; \mathfrak{s} \to \mathfrak{t} \;\mid\; \forall x\mathfrak{s} \;\mid\; \exists x\mathfrak{s} \;\mid\; \mathfrak{s}^t_x$$

where here $x$ ranges over variables ($\mathcal{V}$) and $t$ over terms ($\mathcal{T}$).

As the name suggests, a formula scheme describes the structure of formulas. However, to use it, we require instantiation, whereby the formula-variables are systematically and completely replaced with formulas. An instantiation is a function $\iota : \mathbb{X} \to \mathcal{F}$. It extends to formula-schemes as follows:

$$\iota(\mathfrak{s}) := \begin{cases} \iota(\mathfrak{s}) & \text{if } \mathfrak{s} \in \mathbb{X} \\ \bot & \text{if } \mathfrak{s} = \bot \\ \iota(\mathfrak{s}_1) \circ \iota(\mathfrak{s}_2) & \text{if } \mathfrak{s} = \mathfrak{s}_1 \circ \mathfrak{s}_2,\; \circ \in \{\land, \lor, \to\} \\ Qx\iota(\mathfrak{s}) & \text{if } \mathfrak{s} = Qx\mathfrak{s},\; Q \in \{\forall, \exists\} \\ \iota(\mathfrak{s})[x \mapsto t] & \text{if } \mathfrak{s} = \mathfrak{s}^t_x \end{cases}$$

Given a set of formula-schemes $\mathsf{A}$, we define consequence $\Gamma \vdash_\mathsf{A} \phi$ to mean that there is a valid argument from the axioms $\mathsf{A}$ and assumptions $\Gamma$ that ends with $\phi$.

There are many axiomatizations of classical and intuitionistic logic in the literature. The following appears in Kleene:

We do not require much meta-theory about provability in first-order classical and intuitionistic logic. However, the following results will simplify later proofs:

We use the following results without proof (standard):

3 Base-extension Semantics

3.1 Atomic Systems

We begin with the notion of an atomic system. It may be thought of as an agent's commitments regarding the inferential connexions between some atomic sentences. These are pre-logical in the sense that they do not contain any logical signs. This is why $\bot$ is not "atomic" in this paper. For example, Aristotle may believe the fact

$$\dfrac{}{\text{Socrates is human}}$$

and the inference

$$\dfrac{\text{Socrates is human}}{\text{Socrates is mortal}}$$

What we mean by inference here is that support of the assertion of the premisses gives support for the assertion of the conclusion. For example, Aristotle believes that the assertion "Socrates is mortal" is supported, even though it does not appear explicitly in the position, for it is deduced from his inferential commitments.

A position in this sense is expressed mathematically as an atomic system, defined as a collection of atomic rules that represent facts and inferential relationships. The commitments relative to an atomic system are captured through a derivability judgment.

Thus, Aristotle's position above may be represented symbolically by an atomic system $\mathcal{A}$ containing the rules $\Rightarrow H(s)$ and $H(s) \Rightarrow M(s)$. Moreover, based on this belief set, Aristotle is committed to believing $M(s)$, since we can see that $\vdash_\mathcal{A} M(s)$.

This notation suggests a relationship to natural deduction in the sense of Gentzen: $\{\mathbb{P}_1 \Rightarrow P_1, \ldots \mathbb{P}_n \Rightarrow P_n\} \Rightarrow P$ may be expressed as

$$\dfrac{[\mathbb{P}_1] \quad \cdots \quad [\mathbb{P}_n]}{P_1 \quad \cdots \quad P_n \quad P}$$

That this reading is correct follows from Definition 11. However, since there is no substitution in the application of these rules, they are perhaps more closely related to hereditary Harrop formulae than natural deduction rule figures.

Working in FOL means that we have a choice about whether to include variables in the notion of an atomic system. This would allow us to naturally encode a position such as whoever is human is also mortal,

$$\dfrac{x \text{ is human}}{x \text{ is mortal}}$$

However, we intend for positions to capture the inferential relationships between complete thoughts, so we restrict ourselves to atomic sentences—i.e. closed atoms. Thus, we prefer to represent the above position by including every instance of

$$\dfrac{t \text{ is human}}{t \text{ is mortal}}$$

as $t$ ranges over all names. Mathematically, either approach is possible, but we believe this choice better aligns with our intended interpretation. It is easy to see that the two formalisms have the same expressive power.

Given an open atomic system $\mathcal{A}$, its closure $\bar{\mathcal{A}}$ is defined by applying all total unifiers $\theta : \mathcal{V} \to \mathrm{CL}(\mathcal{T})$ to each rule: $$\bar{r} := \{\{\mathbb{P}_1\theta \Rightarrow P_1\theta, \ldots, \mathbb{P}_n\theta \Rightarrow P_n\theta\} \Rightarrow P\theta \mid \text{total unifiers } \theta\}$$ and $\bar{\mathcal{A}} := \bigcup_{r \in \mathcal{A}} \bar{r}$. Open atomic systems add no expressive power:

3.2 Support

We use atomic systems to ground the semantic judgment of support ($\Vdash$). We may not necessarily accept all forms of atomic systems; different conceptions correspond to different logics. We introduce the idea of a basis, which specifies the kinds of atomic systems we work with.

Our semantics for the logical constants will be parameterised by the notion of basis. The two key bases, where $\mathcal{A}$ ranges over arbitrary atomic systems, are:

• $\mathfrak{C} := \{\mathcal{A} \mid \mathcal{A} \text{ is zero- or first-level}\}$  (for classical logic)
• $\mathfrak{I} := \{\mathcal{A} \mid \mathcal{A} \text{ is zero-, first-, or second-level}\}$  (for intuitionistic logic)

This definition merits some remarks. Firstly, it is an inductive definition, but the induction measure is not the size of the formula $\phi$. Instead, it is a measure of the "logical weight" $w$ of $\phi$. Extending Sandqvist,

$$w(\phi) \;:=\; \begin{cases} 0 & \text{if } \phi \in \mathcal{A} \\ 1 & \text{if } \phi = \bot \\ w(\phi_1) + w(\phi_2) + 1 & \text{if } \phi = \phi_1 \circ \phi_2,\ \circ \in \{\to, \land, \lor\} \\ w(\psi) + 1 & \text{if } \phi = Qx\psi,\ Q \in \{\forall, \exists\} \end{cases}$$

In each clause of Figure 2, the sum of the weights of the complex formulas flanking the support judgment in the definiendum exceeds the corresponding number for any occurrence of the judgment in the definiens. We refer to induction relative to this measure as semantic induction to distinguish it from structural induction.

Secondly, the base-extension $\mathcal{C} \supseteq \mathcal{B}$ appears to recall the change of world condition familiar from Kripke's semantics for intuitionistic logic. Its origins here come from an intuitive reading of implication that does have an intuitionistic quality to it. Intuitively, we expect a $\mathcal{B}$ to support an implication $\phi \to \psi$ if whenever it supports $\phi$ then it also supports $\psi$. However, such a condition would be satisfied vacuously if $\mathcal{B}$ did not support $\phi$. Therefore, we consider arbitrary extension $\mathcal{C} \supseteq \mathcal{B}$ in which $\phi$ is supported and check that under such commitments $\psi$ is also supported.

Thirdly, this semantics assumes a static ontology. The M-tS for intuitionistic logic introduced by Kripke is based on a quasi-ordered set of models whose domains may expand along the ordering. That is, it has an ontology that grows as knowledge increases. Grzegorczyk proposed an alternative with a constant domain, where the ontology remains fixed across all stages. But Görnemann (see also Klemke and Gabbay) demonstrated that this yields an intermediate logic extending intuitionistic logic $\mathsf{I}$ with the additional axiom:

$$\forall x(\mathfrak{s} \lor \mathfrak{t}) \to (\mathfrak{s} \lor \forall x\mathfrak{t}),$$

where $x$ is not free in $\mathfrak{s}$. By contrast, in B-eS there is no need for the domain to change with the base. This makes things comparatively simple.

We assign semantics to sentences—i.e. closed formulas—based on the view that meaning is a property of complete assertions. Nonetheless, we may extend support to all well-formed formulas (wffs) by considering the universal closure of formulas with free variables. That is, let $\phi$ and let $\mathrm{FV}(\phi) = \{x_1, \ldots, x_n\}$:

$$\forall\bar{x}\phi \;:=\; \forall x_1, \ldots, x_n\phi$$

To make this deterministic, we may choose that $x_1, \ldots, x_n$ are the free variables in $\phi$ as it is read right to left. Having established such a closure, we define the support of open formulas as follows:

${\Vdash}_{\!\mathcal{B}}\; \phi$  iff  ${\Vdash}_{\!\mathcal{B}}\; \forall\bar{x}\phi$  (WFF)

To conclude this section, we observe some important results about semantics. They are proved by Sandqvist. The following hold with respect to either $\mathfrak{C}$ or $\mathfrak{I}$—we write $\mathfrak{B}$ as a parameter.

4 Soundness

Soundness asserts that only valid consequences are derivable: if $\Gamma \vdash_\mathsf{A} \phi$, then $\Gamma \Vdash \phi$. We verify that $\Vdash$ satisfies every axiom scheme and every rule of the consequence relation (Definition 3).

5 Completeness

Completeness asserts that all valid consequences are derivable: if $\Gamma \Vdash \phi$, then $\Gamma \vdash_\mathsf{A} \phi$. We employ the simulation strategy of Sandqvist for intuitionistic propositional logic, extended to the first-order setting.

Idea. Each subformula $\chi$ of $\phi$ is assigned a fresh atomic counterpart $\chi^\flat$—e.g. $r = (a \land b)^\flat$. A specially constructed "simulation" base $\mathcal{N}$ encodes the logical behaviour of each connective atomically, ensuring:

$$\chi \;{\Vdash}_{\!\mathcal{N}}\; \chi^\flat \qquad \text{and} \qquad \chi^\flat \;{\Vdash}_{\!\mathcal{N}}\; \chi.$$

Since we assume $\Vdash \phi$, it follows that $\Vdash \phi^\flat$, and given that every rule in $\mathcal{N}$ corresponds to an intuitionistic natural deduction rule, we conclude $\vdash \phi$, as required.

Applying this technique to classical logic and the present setup requires some work. There are two principal challenges. Firstly, simulating Gentzen's NK, the classical analogue of NJ, demands second-level rules of implication introduction,

$$\dfrac{[\phi] \quad \psi}{\phi \to \psi}$$

However, rules with discharge are not permitted in $\mathfrak{C}$ as admitting them comes at the cost of soundness—e.g. DNE would no longer be valid. Secondly, in this paper we are working in the first-order setting that means the simulations require accounting for quantification and open formulas, while atomic rules only contain closed atoms. It no longer suffices to consider only sub-formulas of the given valid sequent $\Gamma \triangleright \phi$, nor can we associate to each such sub-formula $\rho$ a unique atom $r$. These challenges notwithstanding, the strategy goes through as before. By being careful about the setup, we can overcome both of these challenges. We now proceed with the technical details.

Given a set of formulas $\Gamma$ and a formula $\gamma$, let $\Xi$ be the set of sub-formulas. Recall that if $\phi$ contains $x$ as a free variable, the subformulas of $\forall x\phi$ and $\exists x\phi$ are the sentences $\phi[x \mapsto t]$ for $t \in \mathrm{CL}(\mathcal{T})$. Fix an injection $(-)^\flat : \Xi \to \mathrm{CL}(\mathcal{A})$.

Eigenvariables. To handle the quantifiers and free variables, we introduce eigenvariables. They are a set of constants that we use as variables during the simulation:

• Let $\mathcal{E} \subseteq \mathcal{K}$ be the set of constants that do not appear in $\Gamma$ or $\phi$.
• Let $\alpha : \mathcal{V} \to \mathcal{E}$ be a bijection.
• Extend $(-)^\flat$ to open formulas using $\alpha$ such that an open formula is simulated by the atom that simulates its universal closure. That is, if $\{x_1, \ldots, x_m\} = \mathrm{FV}(\phi)$, then define $\bar\phi := \phi[x_1 \mapsto \alpha(x_1)], \ldots, [x_m \mapsto \alpha(x_m)]$ and assign $\phi^\flat := (\bar\phi)^\flat$  (EIGEN).

This defines the encoding of formulas as atoms required for the simulation.

To recover formulas from the "flattening" operation, we require functions $(-)^{\xi_1} : \mathrm{CL}(\mathcal{A}) \to \mathcal{F}$ and $(-)^{\xi_2} : \mathrm{CL}(\mathcal{A}) \to \mathcal{F}$ satisfying some conditions. They both decode by reversing $(-)^\flat$ but they behave differently with respect to encodings of open formulas. This is important for relating constructions in the simulation bases $\mathcal{K}$ and $\mathcal{J}$ to constructions in $\mathsf{C}$ and $\mathsf{I}$, respectively. The conditions are as follows:

• If $P = \phi^\flat$ such that $\phi$ is closed and does not contain any eigenvariables, then $P^{\xi_1} = P^{\xi_2} = \phi$.
• If $P = \phi^\flat$ where $\phi$ is closed but contains eigenvariables, then $P^{\xi_1}$ and $P^{\xi_2}$ distinguish whether or not we want the closed or open version of the formula: $$P^{\xi_1} := \forall\bar{x}\bigl(\phi[a_1 \mapsto \alpha^{-1}(a_1)], \ldots, [a_n \mapsto \alpha^{-1}(a_n)]\bigr) \quad (\mathrm{VAR}_1)$$ $$P^{\xi_2} := \phi[a_1 \mapsto \alpha^{-1}(a_1)], \ldots, [a_n \mapsto \alpha^{-1}(a_n)] \quad (\mathrm{VAR}_2)$$ where $\{a_1, \ldots, a_n\}$ are all the eigenvariables in $\phi$.
• If $P = \phi^\flat$ where $\phi$ is open, then $P^{\xi_1} = \forall\bar{x}\phi$ and $P^{\xi_2} = (\bar\phi)^{\xi_2}$.
• If $P$ is not in the image of $(-)^\flat$, then $P^{\xi_1}$ and $P^{\xi_2}$ can be any formula, but they must be the same formula (i.e. $P^{\xi_1} = P^{\xi_2}$).

Following the plan by Sandqvist outlined above, we now simulate a proof system for FOL. However, rather than simulating a natural deduction system, we simulate the Hilbert–Frege systems in Section 2.

This definition requires some remarks. Clearly, $(\mathrm{K})^\flat$, $(\mathrm{S})^\flat$, $(\forall\mathrm{E})^\flat$, $(\land\mathrm{I})^\flat$, $(\land\mathrm{E}_1)^\flat$, $(\land\mathrm{E}_2)^\flat$, $(\lor\mathrm{I}_1)^\flat$, $(\lor\mathrm{I}_2)^\flat$, $(\neg\mathrm{I})^\flat$, and $(\mathrm{DNE})^\flat$ are intended to simulate corresponding axioms in Figure 1. The rules $(\mathrm{MP})^\flat$ and $(\mathrm{GEN})^\flat$ are intended to simulate MODUS PONENS and GENERALIZATION in Definition 3. The behaviours HYPOTHESIS and AXIOM follow from REF and APP $_2$, respectively, in Definition 11. We have $(\lor\mathrm{E})^\flat$ and $(\mathrm{EFQ})^\flat$ take the form of "rules" (as opposed to "axioms" like the others) because we require the conclusion to be broader than $\Xi$ so that we can simulate the semantic clause for the rule.

Relative to this setup, we require the following lemmas. The proofs of these lemmas are technical and we defer them to the end of this section.

The completeness argument rests on three lemmas:

• AtComp. For $\mathbb{P} \subseteq \mathrm{CL}(\mathcal{A})$ and $P \in \mathrm{CL}(\mathcal{A})$: $\mathbb{P} \;{\Vdash}_{\!\mathcal{B}}\; P \;\Leftrightarrow\; \mathbb{P} \vdash_\mathcal{B} P$.
• Flat. For any $\mathcal{A}' \supseteq_\mathfrak{B} \mathcal{A}$: ${\Vdash}_{\!\mathcal{A}'} \phi^\flat \;\Leftrightarrow\; {\Vdash}_{\!\mathcal{A}'} \phi$, when (i) $\mathcal{A} = \mathcal{K}$, $\mathfrak{B} = \mathfrak{C}$ if $\phi$ contains only $\bot, \to, \forall$; or (ii) $\mathcal{A} = \mathcal{J}$, $\mathfrak{B} = \mathfrak{I}$ for any $\phi$.
• Nat. Let $\mathbb{P} = \Delta^\flat$ for $\Delta \subseteq \mathrm{CL}(\mathcal{F})$ with no eigenvariables, and $P \in \mathrm{CL}(\mathcal{A})$: if $\mathbb{P} \vdash_\mathcal{K} P$ then $\mathbb{P}^{\xi_1} \vdash_\mathsf{C} P^{\xi_2}$; if $\mathbb{P} \vdash_\mathcal{J} P$ then $\mathbb{P}^{\xi_1} \vdash_\mathsf{I} P^{\xi_2}$.

6 Discussion

We have shown that first-order classical logic is sound and complete for the proof-theoretic semantics given by Sandqvist. Simultaneously, we have extended the result to first-order intuitionistic logic. The proofs are constructive and do not rely on the model-theoretic reading of either logic.

Curiously, the semantics for first-order classical and intuitionistic logic reduces to a difference in the notion of base. The apparently small change—from $\mathfrak{C}$ (zero- and first-level rules) to $\mathfrak{I}$ (also second-level rules)—has precise and large consequences for which logic is expressed by the support relation. This suggests that the semantic content of the logical signs is not entirely encapsulated by their clauses in Figure 2, but also depends on the notion of pre-logical consequence (i.e. derivability in a base). This is witnessed in work on substructural logics in which the notion of base was itself made substructural.

The type of base determines which classical laws hold. DNE ($\Vdash \neg\neg\phi \to \phi$) may be replaced by Peirce's Law:

$$((X \to Y) \to X) \to X$$

and one may ask: what is it about various notions of base that makes them intuitively classical? An alternate "classical" notion of base would be one containing rules with discharge:

$$\dfrac{P_1 \quad \cdots \quad P_m \quad [\mathbb{Q}_1] \quad \cdots \quad [\mathbb{Q}_n]}{C}$$

where $C, P_1, \ldots, P_m, Q_1, \ldots, Q_n \in \mathrm{CL}(\mathcal{A})$. Substituting "classical" for other logics of interest—modal, relevant, linear—opens a general research programme.

Finally, in the completeness proof, certain signs—$\bot$, $\lor$, $\exists$—required distinctive treatment: they demanded proper rules in the simulation base rather than axioms, unlike all other connectives. This may reflect something fundamental about the logical treatment of "choice" and "uncertainty", and connects to the well-known subtlety of negation/absurdity in proof-theoretic semantics.

Acknowledgements

We are grateful to Tao Gu and David J. Pym for the many discussions that led to the development of this paper. This work was supported by the EPSRC grant EP/R006865/1.

References