From Basic Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic

1 Introduction

One intuition regarding the meaning of logical consequence, $\Gamma \vdash \phi$, is that it holds by virtue of the logical form of $\Gamma$ and $\phi$, rather than their specific content. One way to express this is by considering arbitrary interpretations of the specific content and demonstrating that $\phi$ holds in any situation in which $\Gamma$ holds.

This leads to Tarski's interpretation of consequence based on models $M$, $$\Gamma \vDash \phi \quad \text{iff} \quad \text{for any model } M,\ \text{if } M \vDash \Gamma,\ \text{then } M \vDash \phi$$ which defines model-theoretic semantics (M-tS). Observe that consequence is defined in terms of the transmission of some categorical notion (in this case, truth). Schroeder-Heister [66] has called this the 'standard dogma' of semantics.

As Prawitz [51] explains, M-tS conflates the meaning of the logical constants with the meaning of truth, since logical structure is defined in terms of interpretations. For example, if $T$ is defined as the least set satisfying certain properties, including $\phi \land \psi \in T$ iff $\phi \in T$ and $\psi \in T$, then no information is gained about $\land$ by saying that it satisfies this relationship. Moreover, M-tS fails to provide a genuinely consequential relationship between $\Gamma$ and $\phi$.

Tennant [75] observes that a consequential reading of a consequence judgment $\Gamma \vdash \phi$ implies that $\phi$ follows from $\Gamma$ by some valid reasoning. This requires a notion of a valid argument that encapsulates the forms of valid reasoning. We must, therefore, explicate the semantic conditions required for an argument that demonstrates $\psi_1, \ldots, \psi_n;\ \text{therefore},\ \phi$ to be valid. Following Prawitz [51], these semantic conditions ought to be based on the logical structure of $\psi_1, \ldots, \psi_n$ and some fixed laws of thought.

Consequently, we abandon the denotationalist perspective on logic, on which M-tS rests, where meaning is given relative to interpretation. Instead, we adopt an inferentialist perspective, where meaning is given in terms of inferential relationships—see Brandom [5] and Murzi and Steinberger [5].

In this paper, we work entirely in the setting of natural deduction in the sense of Gentzen [74]. In inferentialism, even atomic propositions gain meaning through their inferential roles. Thus, we use atomic systems to define when the atomic propositions hold (rather than using models). Details are provided in Sect. 2. Heuristically, atomic systems are sets of natural deduction rules restricted to atomic propositions. This embodies a 'meaning-as-use' philosophy.

For example, the proposition 'Tammy is a vixen' means 'Tammy is female' and 'Tammy is a fox', governed by these rules: $$\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}}$$ These rules, from the inferentialist perspective, are understood as supplying the meaning of the proposition. The 'and' above is justified by comparison with the laws governing conjunction $(\land)$ in NJ, $$\dfrac{\phi \quad \psi}{\phi \land \psi} \qquad \dfrac{\phi \land \psi}{\phi} \qquad \dfrac{\phi \land \psi}{\psi}$$ There are important philosophical and mathematical ramifications on the structure of atomic system admitted — see, for example, Sandqvist [58,59] and Piecha and Schroeder-Heister [43,69].

The area of logic concerning such a consequentialist reading of logic is proof-theoretic semantics (P-tS) [16,68,77]. It is the area of semantics concerning proof (as opposed to truth), where 'proof' means 'valid argument' (as opposed to derivation in a fixed system). This includes both semantics of proofs (i.e., validity conditions on 'arguments') and semantics in terms of proofs (i.e., the meaning of logical constants in terms of consequential relationships). We call the first proof-theoretic validity (P-tV) and the second base-extension semantics (Be-S). This nomenclature follows from certain traditions in the literature, but both branches concern validity and make use of base-extensions in doing so.

Details of B-eS pertinent to this paper are provided in Sect. 4. Heuristically, a B-eS is defined by a support judgment $\Vdash$, relative to atomic systems $B$, by clauses for logical constants, with the base case given by derivability — that is, if $p$ is an atomic proposition, $${\Vdash}_{\!\mathcal{B}}\, p \quad \text{iff} \quad {\vdash}_{\!\mathcal{B}}\, p$$ (where ${\vdash}_{\!\mathcal{B}}\, p$ indicates $p$ can be proved from the rules in $B$). This mirrors satisfaction in M-tS but can differ significantly. In particular, taking the standard clause for disjunction $${\Vdash}_{\!\mathcal{B}}\, \phi \lor \psi \quad \text{iff} \quad {\Vdash}_{\!\mathcal{B}}\, \phi \ \text{ or }\ {\Vdash}_{\!\mathcal{B}}\, \psi$$ renders IPL incomplete (see Piecha et al. [41,42,44]), unless additional structure is added elsewhere (see, for example, Stafford and Nascimento [37,72]). Sandqvist [59] showed that IPL is sound and complete for a notion of support with an alternative clause, $${\Vdash}_{\!\mathcal{B}}\, \phi \lor \psi \quad \text{iff} \quad \forall C \supseteq B\ \forall p \in A,\ \text{if } \phi \Vdash_{C} p \text{ and } \psi \Vdash_{C} p,\ \text{then } {\Vdash}_{C}\, p$$ This paper gives an operational account of this clause in the sense that it explains what it says about arguments for $\phi \lor \psi$.

Given a notion of P-tV, consequence is defined as follows: $$\Gamma \vdash \phi \quad \text{iff} \quad \text{there is a valid argument from } \Gamma \text{ to } \phi$$ Prawitz [46] conjectured that the original and most widely studied account of P-tV corresponds to IPL, but this remains an open problem. The aforementioned work by Piecha et al. [41,42,44] says that the conjecture fails (i.e., IPL is incomplete with respect to the semantics) when the notion of P-tV is slightly simplified. Stafford [71] has shown that the semantics for Piecha et al. [41,42,44] corresponds to general inquisitive logic — that is, the intermediate logic(s) that extends IPL with the rule $$\dfrac{H \to (\phi \lor \psi)}{(H \to \phi) \lor (H \to \psi)}$$ where $H$ is a hereditary Harrop formula (see Miller [36]). While this rule is admissible in IPL, it is not derivable — see Harrop [26].

In this paper, we consider P-tV in the Dummett-Prawitz tradition. A key motivation lies in the following remarks by Gentzen [74]:

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'

Prawitz [46,48,49] used his normalization theory for NJ to develop a semantic concept reflecting this intuition. Dummett [10] later developed the philosophical underpinnings of the idea.

The basic idea of P-tV in the Dummett-Prawitz tradition is that arguments are valid by virtue of their form. One begins with some class of canonical proofs relative to which validity is computed. Arguments are valid if they represent a canonical proof. Thus, P-tV in the Dummett-Prawitz tradition is based on the following ideas:

• the priority of canonical proofs
• the reduction of closed non-canonical arguments to canonical ones.
• the substitutional view of open arguments — that is, open arguments are justified by considering their closed instances.

We defer to Schroeder-Heister [64] for a formal account of this version of P-tS and its subsequent developments — see, for example, Prawitz [47–49]. This is closely related to the Brouwer-Heyting-Kolmogorov (BHK) interpretation of intuitionism — see Sect. 2.3 and Schroeder-Heister [65].

Typically, normalized closed arguments are valid iff their immediate subproofs are valid, prioritizing introduction rules. Normalized derivations in NJ conclude with introduction rules (see Prawitz [50]). Schroeder-Heister [67] proposed an alternative based on elimination rules, drawing ideas by Prawitz [46]. The logical form of a proposition tells us how we may use it; for example, given an implicational proposition, its logical form says no more than this: one may establish the consequent by establishing the antecedent. This is expressed by the law of modus ponens, $$\dfrac{\phi \to \psi \quad \phi}{\psi}$$ More generally, it is the elimination (not introduction) rules that says how one may use a proposition of a certain logical form. This suggests a version of P-tV based on elimination rules. As Schroeder-Heister [67] observes:

The intuition behind the approach based on elimination rules is that a derivation is valid, if the result of the application of each possible elimination rule to its end-formula is valid.

Thus an argument is no longer valid in virtue of its form or the form to which it can be reduced (as in the introduction-based approach), but rather in virtue of the immediate consequences one can reach starting with this argument. This is a genuinely 'consequentialist' view of validity.

Importantly, basing P-tV on the elimination rules does not necessarily mean that one is taking the elimination rules as prior to the introduction rules. Hallnäs and Schroeder-Heister [23–25,63] have shown the elimination rules arises from the introduction rules by means of Definitional Reflection (DR):

whatever follows from all the defining conditions of an assertion, follows from the assertion itself

For example, disjunction $(\lor)$ has the following introduction rules: $$\dfrac{\phi}{\phi \lor \psi} \qquad \dfrac{\psi}{\phi \lor \psi}$$ Therefore, the defining conditions of $\phi \lor \psi$ are $\phi$ and $\psi$. Thus, DR warrants the following rule recognizable as the standard elimination rule: $$\dfrac{\phi \lor \psi \quad [\phi] \; \chi \quad [\psi] \; \chi}{\chi}$$ Importantly, DR amounts to a closed-world assumption — in the sense of Reiter [56] — on introduction rules as definitions.

As for P-tV based on the introduction rules, it is an open problem what logic P-tV based on the elimination rules represents. This paper shows that, assuming certain conditions about the notion of reduction on arguments and base, this version of P-tV corresponds to the B-eS for intuitionistic propositional logic (IPL) by Sandqvist [59]. That is, one derives the semantic clauses of the B-eS from the semantic clauses of the P-tV. Hence, this version of P-tV based on the elimination rules corresponds to IPL.

In other words, this paper says that the semantics of the logical constants (as expressed in the B-eS) is indeed given by their consequential relationships. Conversely, taking the semantics of the logical constants (as expressed in the B-eS) as conceptually prior to logical consequence, this paper shows that consequence in IPL indeed obtain by virtue of the logical form of the propositions involved. Consequently, the elimination-based approach provides a more 'consequentialist' reading of validity, focusing on the immediate uses of a proposition.

Much of the analysis in this paper concerns understanding precisely how the choice of reduction and base recover intuitionism. It begins with unpacking BHK, constructivism, and intuitionism. This is the subject of Sect. 5. However, further clarity might be gained by looking at constructivism in a classical sense. We discuss this further in Sect. 7.

We begin in Sect. 2 with an overview of natural deduction, the setting in which this paper takes place. In Sect. 3, we define P-tV as used in this paper. In Sect. 4, we give the B-eS for IPL by Sandqvist [59]. The main contribution of the paper is in Sect. 5 where we formally relate P-tV and B-eS. In Sect. 6, we discuss the position of negation in P-tS, which is known to be a subtle issue (see, for example, Kürbis [32]), relative to the work of this paper. Finally, in Sect. 7, we give a summary and conclusion to the paper. Throughout, we fix a denumerable set of atomic propositions $A$.

Relative to such a set we define $F$ by the following grammar: $$\phi ::= p \in A \mid \phi \lor \phi \mid \phi \land \phi \mid \phi \to \phi \mid \bot$$ We may use meta-variables $\Gamma$ and $\Delta$ (possibly adorned with subscripts or primed) to denote sets of formulas; we use $P$, $Q$, $S$ (possibly adorned with subscripts or primed) to denote sets of atoms. We may write $\neg\phi$ to abbreviate $\phi \to \bot$.

2 Background

2.1 Natural Deduction

We require some familiarity with natural deduction in the style of Gentzen [50, 62,74]. In this section, we give a terse but complete summary to keep the paper self-contained. The objects studied in natural deduction are arguments:

2.2 System NJ

There are many presentations of IPL in the literature. Therefore, we begin by fixing the relevant concepts and terminology for this paper. In this paper, IPL is a certain consequence judgement $\vdash$ on sequents. Our principal characterization will be through a natural deduction system.

2.3 The BHK Interpretation

Intuitionism, as defined by Brouwer [6], is the view that an argument is valid when it provides sufficient evidence for its conclusion. This is IL. Famously, as a consequence, IL rejects the law of the excluded middle — that is, the meta-theoretic statement that either a statement or its negation is valid. This law is equivalent to the principle that in order to prove a proposition it suffices to show that its negation is contradictory. In IL, such an argument does not constitute sufficient evidence for its conclusion.

Heyting [27] and Kolmogorov [31] provided a semantics for intuitionistic proof that captures the evidential character of intuitionism, called the Brouwer-Heyting-Kolmogorov (BHK) interpretation of IL. It is now the standard explanation of the logic. Supposing a notion of proof for atomic formulae,

• a proof $\mathcal{A}$ of $\phi \land \psi$ is a pair $\mathcal{B}_1, \mathcal{B}_2$ such that $\mathcal{B}_1$ is a proof of $\phi$ and $\mathcal{B}_2$ is a proof of $\psi$;
• a proof $\mathcal{A}$ of $\phi \lor \psi$ is either a pair $\langle 0, \mathcal{B} \rangle$ such that $\mathcal{B}$ is a proof of $\phi$ or a pair $\langle 1, \mathcal{B} \rangle$ such that $\mathcal{B}$ is a proof of $\psi$;
• a proof of $\phi \to \psi$ is a method $f$ for constructing a proof of $\psi$ from a proof of $\phi$;
• nothing is a proof of $\bot$.

The propositions-as-types correspondence — see Howard, Barendregt, and others [1–3,29] — gives a standard way of instantiating the BHK interpretation as terms in the simply-typed $\lambda$-calculus. Technically, the set-up can be sketched as follows: a judgement that $D$ is an NJ-proof of the sequent $\phi_1, \ldots, \phi_k \vdash \phi$ corresponds to a typing judgement $x_1 : A_1, \ldots, x_k : A_k \vdash M(x_1, \ldots, x_k) : A$ where the $A_i$s are types corresponding to the $\phi_i$s, the $x_i$s correspond to placeholders for proofs of the $\phi_i$s, the $\lambda$-term $M(x_1, \ldots, x_k)$ corresponds to $D$, and the type $A$ corresponds to $\phi$.

Lambek [33] gave a more abstract account by showing that simply-typed $\lambda$-calculus is the internal language of cartesian closed categories (CCCs), thereby giving a categorical semantics of proofs for IPL. In this set-up, a

morphism $[[\phi]]$ in a CCC, where $\times$ denotes cartesian product, that interprets the NJ-proof $D$ of $\phi_1, \ldots, \phi_k \vdash \phi$ also interprets the term $M$, where the $[[\phi_i]]$s interpret also the $A_i$s and $[[\phi]]$ also interprets $A$. Altogether, this describes the Curry-Howard-Lambek correspondence for IPL as summarized in Fig. 2 in which:

• $D \Rightarrow \Gamma \vdash \phi$ denotes that $D$ is an NJ-derivation of $\phi$ from $\Gamma$;
• $x : A, \Gamma \vdash M(x) : A_\phi$ denotes a typing judgment, as described above, corresponding to $D$; and
• $[[\Gamma]] \xrightarrow{[[D]]} [[\phi]]$ denotes that $[[D]]$ is a morphism from $[[\Gamma]]$ to $[[\phi]]$ in a CCC.

To generalize to full IL (and beyond), Seely [70] modified this categorical set-up and introduced hyperdoctrines — indexed categories of CCCs with coproducts over a base with finite products. Martin-Löf [35] gave a formulae-as-types correspondence for predicate logic using dependent type theory. Barendregt [1] gave a systematic treatment of type systems and the propositions-as-types correspondence. A categorical treatment of dependent types came with Cartmell [7] — see also, for examples among many, work by Streicher [73], Pavlović [39], Jacobs [30], and Hofmann [28]. In total, this gives a semantic account of proof for first- and higher-order predicate intuitionistic logic based on the BHK interpretation.

Pym and Ritter [53] have provided a generalization of the BHK interpretation closely related to P-tV. The original motivation was as a semantics of reductive logic.

The traditional approach to logic is through the deductive paradigm in which conclusions are inferred from established premises. However, in practice, logic typically proceeds through the dual paradigm known as reductive logic: sufficient premises are inferred from putative conclusions by means of 'backwards' inference rules. Pym and Ritter [53] have given a semantics to

a generalization of BHK in a way that recalls P-tV. Specifically, they give the constructions-as-realizers-as-arrows correspondence Fig. 3 based on polynomial categories, which extend a category in which arrows denote proofs for a logic by additional arrows that supply 'proofs' for propositions that do not have proofs but appear during reduction:

• $\Phi \Rightarrow \Gamma \vdash \phi$ denotes that $\Phi$ is a sequence of reductions for the sequent $\Gamma \vdash \phi$;
• $[\Gamma] \vdash [\Phi] : [\phi]$ denotes that $[\Phi]$ is a realizer of $[\phi]$ with respect to the assumptions $[\Gamma]$; and
• $[[\Gamma]] \xrightarrow{[[\Phi]]} [[\phi]]$ denotes that $[[\Phi]]$ is a morphism from $[[\Gamma]]$ to $[[\phi]]$ in the appropriate polynomial category.

They also defined a judgement $w \vdash_\Theta (\Phi : \phi)\,\Gamma$ which says that $w$ is a world witnessing that $\Phi$ is a reduction of $\phi$ to $\Gamma$, relative to the indeterminates of $\Theta$.

We observe in this characterization obvious similarities with the BHK interpretation of IL (see Sect. 2.2). Specifically, it coheres with the generalization by Pym and Ritter [53]:

• the judgment $\Phi \Rightarrow \Gamma \vdash \phi$ corresponds to P-tV,
• the judgment $[\Gamma] \vdash [\Phi] : [\phi]$ corresponds to the realizers interpretation of arguments in Sect. 5, and
• the judgment $[[\Gamma]] \xrightarrow{[[\Phi]]} [[\phi]]$ corresponds to B-eS.

Thus, in this paper, we move from the realizers perspective, in which the witnessing arguments must be constructed explicitly to the types perspective in which the witnessing arguments are observed implicitly as arrows.

3 Proof-theoretic Validity

There are several accounts of proof-theoretic validity—see, for example, Prawitz [46–48,50] and Schroeder-Heister [64,68]. Typically, they are based on the introduction rule and can be seen as a way to realize the sentiment expressed by Gentzen [74] (see Sect. 1) that the introduction rules represent definitions of the connectives involved. Prawitz's Conjecture [48] is the statement that IPL is complete with respect to P-tV based on the introduction rules.

As explained in Sect. 1, Piecha et al. [42] show that Prawitz's Conjecture fails when P-tV is slightly simplified. Indeed, Stafford [71] has shown that the logic described by the simplified version of P-tV is a (general) inquisitive logic. In contrast, Takemura [57] suggests that the conjecture holds without the simplification.

In this paper, we consider an alternate version of P-tV that is based on the elimination rules. In contrast to the treatment of P-tV based on the introduction rules, we show that this version of P-tV does correspond to IPL when certain details of the setup are met.

In Sect. 2, we introduced the idea of an atomic system. These atomic systems will form the base case of validity. However, we do not necessarily want to consider all atomic systems, but rather some specific forms—see, for example, Piecha and Schroeder-Heister [43,69]. Therefore, fix a notion of base $\mathcal{B}$ (i.e., a subset of all atomic systems). It is these systems that will form the basis of validity. Henceforth, we consider only atomic systems that are bases. Thus, given a base $B$, we may write $C \supseteq B$ to express that $C$ is a superset of $B$ that is also a base. Furthermore, in Sect. 2, we discussed the idea of reduction by Prawitz [50]. This also forms an essential part of the definition of proof-theoretic validity. Presently, we will not fix some particular set of reductions, but rather work relative to such sets as a parameter. Thus, let $R$ be a set of reductions—that is, functions from arguments to arguments. While specific features of the elements of $R$ may be desirable (e.g., that they are computable), we shall not impose any such restrictions until they become necessary.

Condition 21. The set of reductions $R$ is such that the use of disjunction elimination (i.e., $\lor E$) is a $B$-valid argument. That is, the argument $$\dfrac{\chi_1 \lor \chi_2 \quad \substack{\Gamma,[\chi_1]\;B_1 \\ \chi} \quad \substack{\Gamma,[\chi_2]\;B_2 \\ \chi}}{\chi}$$ is $B$-valid whenever $B_1$ and $B_2$ are $B$-valid. Furthermore, for any $C \supseteq B$, $$\dfrac{\chi_1 \lor \chi_2 \quad \substack{\Gamma,[\chi_1]\;B_1 \\ \chi} \quad \substack{\Gamma,[\chi_2]\;B_2 \\ \chi}}{\chi}$$ is $C$-valid whenever $B$ is $B$-valid, and $B_1$ and $B_2$ are $C$-valid.

We return to the issue of reduction operators and bases in Sect. 5. Presently, we require only that the notion of reduction can eliminate any extraneous logical content from a $B$-valid argument:

Condition 22. If there is a $B$-valid argument from $P \subseteq A$ to $p \in A$, then there is a $B$-derivation from $P$ to $p$.

The same idea allows us to characterize exactly what it means for a formula $\chi$ to be a vacuous assumption in an argument. This means either that there already exists a valid argument for it relative to the current assumptions, so that it needs not be assumed itself; or it means that whenever there is a valid argument from it, there is a valid argument without it. These two cases correspond to the left and right directions of the following condition:

Condition 23. The set of reductions $R$ is such that the following holds: $$\Gamma \vdash_B \chi \quad \text{iff} \quad \forall C \supseteq B,\ \forall p \in A,\ \text{if } \chi, \Gamma \vdash_C p,\ \text{then } \Gamma \vdash_C p$$ This completes the definition of P-tV.

4 Base-extension Semantics

As explained in Sect. 1, by 'base-extension semantics' we mean semantics for a logic in terms of proofs in a base. There are many varied examples of B-eS in the literature including, inter alia, Eckhardt and Pym [12] for modal logic, Gheorghiu et al. [18,19] for substructural logic, Makinson [34] for classical logic, Nascimento [37,72] using multi-bases, and Piecha et al. [41,42,44] and Stafford [71] for super-intuitionistic logics. Also related, taking a slightly more general scope, is work by Goldfarb [22]. In this paper, we follow the version of B-eS by Sandqvist [58,59].

The B-eS for IPL given by Sandqvist [59] only admits certain atomic systems. A Sandqvist Base is an atomic system containing only atomic rules of the form $$\dfrac{c}{p} \qquad \dfrac{c \quad [Q_1]\;p_1 \quad \cdots \quad [Q_n]\;p_n}{c}$$ where $Q_1, \ldots, Q_n$ are (possibly empty) finite sets of atoms. The set of Sandqvist bases is denoted $S$. The B-eS for IPL is defined by the following support judgment:

5 From Proof-Theoretic Validity to Base-Extension Semantics

5.1 Constructivity, Intuitionism, and Validity

Schroeder-Heister [65] observes that P-tV represents a 'constructive' notion of validity. In this section, we explore this idea as it explicates how P-tV relates to B-eS. We can understand this through realizability: formulas are realized by objects, known as realizers, whose existence certifies the validity of the formula. In the BHK interpretation of IPL, a realizer of a formula $\phi \to \psi$ is a function that takes as inputs a realizer of $\phi$ and outputs a realizer of $\psi$ — see Sect. 2.3. This functional relation is what makes the semantics constructive, as the functions construct a realizer for $\psi$ from a realizer for $\phi$. In P-tV, a realizer for $\phi \to \psi$ is a valid argument for $\phi \to \psi$. This is identified with a valid argument from $\phi$ to $\psi$. Thus, in adopting P-tV, we move from functions to arguments as the method for creating realizers.

Recall that P-tV (Definition 19) is parameterized on a set of reductions $R$. Precisely what notion of constructivity it expresses depends on what reductions are adopted. Presently, we present some conditions that should express the intuitionistic notion of constructivity. In Sect. 7, we discuss how this analysis changes as the target logic changes.

Firstly, for intuitionism, we expect at least the introduction rules to be valid constructors. Thus:

Condition 28. The set of reductions $R$ is such that uses of the introduction rules comprise valid arguments. For example, the argument $$\dfrac{\phi_1 \quad \phi_2}{\phi_1 \land \phi_2}$$ is a valid argument for any $\phi$. By Definition 19, this means that for any $B$-valid arguments for $\phi$ and $\psi$, one has a $B$-valid argument for $\phi \land \psi$.

Observe that the traditional reduction operators by Prawitz [50] suffice for Condition 28. This follows as Definition 19 essentially requires one to assume a $B$-valid argument for the premises and then apply an elimination rule, and the reductions precisely return the assumed argument.

Secondly, we require understanding the conditions under which one has a realizer for $\bot$. In contrast to BHK, the answer ought not to be 'never' in P-tV, as presumably one should be able to conclude $\bot$ from an inconsistent set of assumptions. We return to this in Sect. 6. Dummett [10] proposes the following for intuitionism:

Condition 29. The set of reductions $R$ is such that the following holds: $$\Gamma \vdash_B \bot \quad \text{iff} \quad \Gamma \vdash_B p \text{ for all } p \in A$$

Thirdly, Schroeder-Heister [66] observes that constructive semantics follows the standard dogma of semantics in which the validity of a consequence is understood as the transmission of the validity of assumptions to the conclusion. Hence, by Definition 19, a $B$-valid argument from $\phi$ to $\psi$ transmits $C$-validity of $\phi$ to $\psi$ for $C \supseteq B$. Hence, accepting this standard dogma, we impose the following:

Condition 30. The set of reductions $R$ is such that the following holds: $$\Gamma \vdash_B \phi \quad \text{iff} \quad \forall C \supseteq B,\ \text{if } {\Vdash}_C\, \psi \text{ for } \psi \in \Gamma,\ \text{then } {\Vdash}_C\, \phi$$ This concludes the analysis of constructiveness, intuitionism, and validity.

5.2 From Proof-Theoretic Validity to Support

In summary, the conditions for reductions $R$ are such that for any base $B$:

• (Condition 21) The full disjunction-elimination rule applies, not only when it has atomic conclusions.
• (Condition 22) If there is a $B$-valid argument from atomic assumptions to an atomic conclusion, then there is a $B$-derivation from those assumptions to the conclusion.
• (Condition 23) A formula is not required as an assumption if there is a $B$-valid argument with the same open assumptions except the formula.
• (Condition 28) The introduction rules construct $B$-valid arguments.
• (Condition 29) There is a $B$-valid argument concluding $\bot$ iff there are $B$-valid arguments concluding $p$ for any atom $p \in A$.
• (Condition 30) The standard dogma of semantics — that is, the transmission view of consequence — applies to $B$-validity.

We call a set of reductions satisfying these conditions supportive. Relative to such reductions, entailment (P-tV) and support (B-eS) coincide. This is the content of Theorem 34, below.

6 Ex Falso Quodlibet?

In Sect. 5, we accepted the meaning of $\bot$ in terms of ex falso quodlibet (EFQ), $$\bot \vdash \phi$$ The section is motivated by the BHK interpretation of intuitionism (Sect. 2.3) in which 'nothing is a proof of $\bot$'. This causes an apparent conflict in this paper that requires some explanation. While realizability and proof-theoretic validity are deeply connected, they are not the same thing. The realizability interpretation takes place at an essentially classical meta-level, while proof-theoretic validity takes place at an essentially intuitionistic meta-level.

What we mean when we say that realizability is classical is that the 'if…, then…' in its clauses are classical. In the parlance of realizability, EFQ says the following: If there is a realizer for $\bot$, then there is a realizer for $\phi$. Since the antecedent is false, the implication holds vacuously.

By contrast, when we say that proof-theoretic validity is intuitionistic, we mean that we have chosen the notion of validity to be such that: given a $B$-valid argument for $\bot$, one may construct a $B$-valid argument for $\phi$. For this condition to be a definition, we apply a closed-world assumption in the form of definitional reflection (DR). In this case, the expression of DR is somewhat different from the version given in Sect. 1.

Schroeder-Heister [67] has given a detailed account and observes that for the particular version of DR we use, our bias is 'to consider "consequential" clauses' as definitions, rather than introduction. This is captured in Condition 29 (Sect. 5), which establishes EFQ as the definition of $\bot$.

This distinction between realizability and proof-theoretic validity is why IPL is not 'structurally' complete — see, for example, Pogorzelski [45]. While the horizontal bar in natural deduction corresponds to realizability — that is, the existence of realizers for the things above it guarantee the existence of the things below it — the implication corresponds to proof-theoretic validity — that is, there is a $B$-valid argument for $\phi \to \psi$ iff there is a $B$-valid argument from $\phi$ to $\psi$.

To end this section, we note that the remarks about the constructiveness of EFQ being classically justified is not new. Indeed, it is an essential part of the standard analysis on the relationship between EFQ and the disjunctive syllogism (DS), $$\dfrac{\phi \lor \psi \quad \neg\phi}{\psi}$$ — see, for example, Johansson and Heyting [8] and Pereira et al. [40]. How does the existence of valid arguments for $\phi \lor \psi$ and $\neg\phi$ necessitate the existence of a valid argument for $\psi$? It is not that one is constructed from them, rather it is that in this situation, on the basis of the classical reasoning at the meta-level in which the arguments exist, we conclude that there must be a valid argument for $\psi$. The details are as described below.

Suppose one has $B$-valid arguments $D_1$ and $D_2$ for $\phi \lor \psi$ and $\neg\phi$, respectively. The existence of $D_1$ suggests that there is a $B$-valid argument $D_1'$ for either $\phi$ or $\psi$. Suppose that $D_1'$ is a $B$-valid argument for $\phi$, then using $D_2$, we can construct a $B$-valid argument for $\bot$ using $\to E$, $$\dfrac{[\phi]\;D_2 \atop \neg\phi}{\bot}\,{\to}E$$ However, there is no $B$-valid argument for $\bot$. Contradiction! Hence, we must reject our assumption, and the only remaining possibility is that $D_1'$ is a $B$-valid argument for $\psi$ (not $\phi$). We thus conclude, by classical reasoning, from the existence of a $B$-valid argument for $\phi \lor \psi$ and $\neg\phi$ that there is a $B$-valid argument for $\psi$ without constructing one.

This work on EFQ adumbrates the readings of $\bot$ by Tennant [75,76] and Fukuda and Igarashi [17] in which it is a declaration about the state of a construction. More generally, Berto [4] has developed a reading of negation as a 'modal' operator making a declaration about the set of accessible worlds.

7 Conclusion

Proof-theoretic semantics is the approach to meaning based on proof (as opposed to truth). There are two broad approaches to it in the literature: proof-theoretic validity (P-tV) and base-extension semantics (B-eS). The former is a semantics of arguments, and the latter is a semantics of a logic in terms of arguments. Heuristically, P-tV provides a semantics by taking a sequent as valid iff it admits a valid argument. In this paper, we demonstrate that a certain version of P-tV provided by Prawitz [46] (see also Schroeder-Heister [67]) contains the same semantic content as the B-eS for IPL provided by Sandqvist [59]. This explains why this B-eS is complete.

To make the connection between P-tV and the B-eS of IPL, the paper considers carefully the notions of reduction and base that capture the 'constructive' content of intuitionistic proof. This follows from the BHK interpretation of intuitionism (see Sect. 2). This, of course, raises the question of whether or not the other logics can be similarly captured. For example, there are B-eS for a variety of modal [12] and intuitionistic substructural logics [18,19] relative to which the kind of analysis in this paper could be performed. Thus, future work includes extending the analysis herein to these domains and thereby understanding the consequential reading and constructive content of these logics.

On this note, we may particularly ask for a truly consequential reading of classical entailment. According to Dummett [9]:

In the resolution of the conflict between these two views [the truth-theoretic reading of classical connectives, and the demand that it be explained without recourse to the principle of bivalence] lies, as I see it, one of the most fundamental and intractable problems in the theory of meaning; indeed in all philosophy.

Sandqvist [58] addressed this with a B-eS akin to the one in this paper. This work takes $\to$ and $\bot$ as the only primitive connectives and provides the same B-eS for IPL, but with atomic systems restricted to rules without discharge (other choices are also possible — see Sandqvist [60,61]). This provided an anchor relative to which one can investigate classical logic.

In parallel, Gheorghiu and Pym [21] have shown that the key factor driving the proof-theoretic semantic distinction between intuitionistic and classical logic lies in the interpretation of disjunction (cf. Dummett [11]). Moreover, just as intuitionistic logic corresponds to the (simply typed) $\lambda$-calculus as a canonical instantiation of the realizability (i.e., BHK) interpretation, classical logic corresponds to the $\lambda\mu$-calculus (see Parigot [38]). In this context, Pym and Ritter [52] have shown that one can give two natural interpretations of disjunction, both of which are constructive, through $\lambda\mu$-terms, one corresponding to intuitionistic disjunction and the other corresponding to classical disjunction. Investigating the concept of proof-theoretic validity for classical logic relative to these findings remains future work.

Acknowledgements. We are grateful to the reviewers on an earlier edition of this article for their thorough and thoughtful comments on this work.

Declarations

This work has been partially supported by the UK EPSRC grants EP/S013008/1 and EP/R006865/1, and by Gheorghiu's EPSRC Doctoral Studentship.

Open Access. This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.

Publisher's Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.