A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic

Alexander V. Gheorghiu

Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024) · doi:easychair:kQX1

PDF DOI ← All Publications
Abstract

We give an evaluation system for the admissibility of rules in intuitionistic proportional logic. The system is based on recent work on the proof-theoretic semantics of IPL.

1 Introduction

Proof theory is an area of logic concerned with the study of constructions, called proofs, that certify the validity of formulae. In this paper, we restrict attention to the paradigm of natural deduction in the sense of Gentzen [43]. We assume general familiarity with this formalism, as covered in, for example, Troelstra and Schwichtenberg [44] and Negri [19].

A key concept within proof theory is the admissibility of rules. A rule is admissible for a logic when the logic is closed under that rule; that is, whenever the premisses are valid, the conclusion is also valid.

It is well-known that admissibility in intuitionistic propositional logic (IPL) is a subtle problem. Unlike in, for example, classical propositional logic (CPL), where all the admissible rules are derivable, there are rules that are admissible in IPL but not derivable. Perhaps the first such rule known is Harrop's Rule [13],

$$\dfrac{\neg\chi \to (\phi \lor \psi)}{(\neg\chi \to \phi) \lor (\neg\chi \to \psi)}$$

While several extensions of this rule have been studied — see, for example, Mints [18] and Citkin [2] — classifying all the admissible rules is subtle.

Friedman [6] asked if the problem is decidable; that is, is there a decision procedure such that given a rule it outputs 'yes' if the rule is admissible and 'no' otherwise. Rybakov [32] showed that the problem is indeed decidable, but also showed that there is no finite set of admissible rules that 'generates' all the admissible rules. Vissier [45] and de Jongh [3] provided a recursively enumerable set of rules that they conjectured would generate all the admissible rules for IPL. Following work by Ghilardi [10], Iemhoff [15] proved the conjecture correct.

As Schroeder-Heister [40] observe, the traditional approach to the correctness of an inference (i.e., an instance of a rule) concerns the material transmission of validity; that is, a rule is correct just in case the conclusion is valid whenever the premisses are valid. Hence, to address the question of an admissible rule in IPL, it suffices to have a characterization of validity for IPL that is amenable to evaluating such transmissions. In this paper, we consider the approach in which IPL is characterized by valid arguments.

Developed by a separate community in parallel to the question about the admissibility of rules, has been the problem of defining the validity of proofs. Beginning with remarks by Gentzen [43], Prawitz [28] initiated the study of such validity conditions by using his normalization results (see also Dummett [4]). This is now a central topic within the field of proof-theoretic semantics (P-tS) [41].

Since P-tS is broad subject, containing numerous subtle ideas, we restrict details in this paper to those pertinent to evaluating the admissibility of rules. In the Dummett-Prawitz tradition of P-tS, an essential theme is to justify the admissibility of the elimination rules through the introduction rules; for example, on the basis of

$$\dfrac{[\phi]}{\dfrac{\psi}{\phi \to \psi}} \,{\to}\text{I}$$

as the introduction rule for implications $(\to)$, one has the admissibility of the elimination rule for implication,

$$\dfrac{\phi \to \psi \quad \phi}{\psi} \,{\to}\text{E}$$

as follows: if there are proofs $D_1$ and $D_2$ witnessing $\phi \to \psi$ and $\phi$, respectively, then (by ${\to}\text{I}$) one may compose them to yield a proof of $\psi$. Observe that this makes a central use of normalization as is thus intimately linked to the Curry-Howard Correspondence Theorem [14].

While P-tS concerns defining the validity of proofs, it also concerns defining the validity of formulae in terms of proofs. Recently, Sandqvist [35] has given such a P-tS for IPL — the details are given in Section 2 — it is called a base-extension semantics (B-eS) to distinguish it from the Dummett-Prawitz tradition discussed above. Recently, Gheorghiu and Pym [9] have shown that Sandqvist's B-eS [35] expresses the declarative content of the original notion of proof-theoretic validity by Prawitz [24] (see also Schroeder-Heister [38]).

Makinson [17] observes of P-tS/B-eS:

Some readers may not be happy with the term 'semantics' for this construction, feeling that it — and perhaps any inferential semantics — is too syntactic in nature to deserve that title. They may prefer to use the neutral term 'evaluation system'; none of our formal results depend on the choice of terminology.

Indeed, the B-eS for IPL does provide an evaluation system for the logic, that is the interest in it for the present paper. The question of whether or not it is a 'semantics' is addressed elsewhere — see, for example, Dummett [4], Brandom [1], and Schroeder-Heister [41]. Note that admissibility of rules has been used by Piecha et al. [37, 21, 20, 23] to analyze the merits of various approaches to P-tS, particularly focusing on Harrop's Rule and Pierce's Law.

In this paper, we use the the completeness of valid arguments for IPL to characterize admissibility:

a rule is admissible if whenever the premisses admit a valid argument, the conclusion admits a valid argument

Thus: using the B-eS for IPL as a characterization of the existence of a valid argument through the recent work by Gheorghiu and Pym [9], we immediately have an evaluation system. The resulting evaluation system is quite different from the aforementioned work by Iemhoff [15], and its relationship remains to be determined.

The paper begins in Section 2 with a summary of the required technical background on P-tS for this paper. The main problem (i.e., the admissibility of rules for IPL) is defined in Section 3, and we provide an evaluation system for admissibility (based on the P-tS for IPL). The paper concludes in Section 4 with a summary of contributions and discussion of future work.

We fix some notation conventions used throughout the paper. Throughout, fix a (denumerable) set of atomic propositions ATOM — the elements of which are called 'atoms,' 'propositional letters,' or 'propositional variables.' We take $\land, \lor, \to, \bot$ as the logical connectives of IPL. We use $A, B, C, \ldots$ to denote atoms and $\phi, \psi, \chi, \ldots$ to denote formulae; we may write $\neg\phi$ to abbreviate $\phi \to \bot$. We use $P, Q, R, \ldots$ to denote finite sets of atoms and $\Gamma, \Delta, \Sigma, \ldots$ to denote (possibly infinite) sets of (atomic and complex) formulae.

2 Background: Proof-theoretic Semantics for IPL

In proof-theoretic semantics (P-tS) [38, 5, 46], meaning and validity are characterized in terms of proofs — understood as objects denoting collections of acceptable inferences from accepted premises — and provability. To emphasize: it is not that one provides a proof system for the logic, but rather one explicates the meaning of the connectives in terms of proof systems. Indeed, as Schroeder-Heister [39] observes, since no formal system is fixed (only notions of inference), the relationship between semantics and provability remains the same as it has always been: soundness and completeness are desirable features of formal systems. Essentially, proof in P-tS plays the part of truth in traditional model-theoretic semantics (M-tS).

As a field, P-tS is wide and encompasses several distinct approaches. In this paper, we restrict attention to base-extension semantics (B-eS), which is a particular approach to P-tS. A B-eS is a characterization of a logic by judgment relation called support that is inductively defined according to the syntax of the logic. It is analogous to the satisfaction judgment in M-tS (cf. Kripke [16]). Crucially, the base case is given by 'derivability in a base' which is regarded as a pre-logic notion of proof; that is, bases are proof systems restricted to atoms, no logical constants permitted. Despite being structurally similar to M-tS, the subtle differences in the setup have significant consequences (discussed below).

In this paper, we follow the approach to B-eS by Sandqvist [33, 34, 35], Piecha et al. [21, 20, 23], and Gheorghiu et al. [7, 12]. While there are other versions than presented here (cf. Goldfarb [11] and Stafford and Nascimento [42]), they are not directly relevant for this work.

The B-eS for IPL begins by defining atomic rules. An atomic rule is a natural deduction rule of the following form, in which $p, p_1, \ldots, p_n$ are atoms and $P_1, \ldots, P_n$ are (possibly empty) sets of atoms:

$$\dfrac{[P_1] \quad \cdots \quad [P_n] \quad p_1 \quad \cdots \quad p_n}{p} \; a \qquad\qquad \dfrac{}{p} \; a$$

A base is a set of atomic rules. We write $\mathcal{B}, \mathcal{C}, \ldots$ to denote bases, and $\emptyset$ to denote the empty base (i.e., the base with no rules). We say $\mathcal{C}$ is an extension of $\mathcal{B}$ if $\mathcal{C}$ is a superset of $\mathcal{B}$, denoted $\mathcal{C} \supseteq \mathcal{B}$.

Bases are to be read as natural deduction systems except that atomic rules are taken per se and not closed under substitution when creating derivations.

Definition 1 (Derivability in a Base)

Derivability in a base $\mathcal{B}$ is the smallest relation $\vdash_{\mathcal{B}}$ satisfying the following:

  • ref: $P \vdash_{\mathcal{B}} p$, whenever $p \in P$.
  • app1: If $a \in \mathcal{B}$ (with conclusion $p$, no premisses), then $P \vdash_{\mathcal{B}} p$.
  • app2: If $r \in \mathcal{B}$ and $P, P_1 \vdash_{\mathcal{B}} p_1, \ldots, P, P_n \vdash_{\mathcal{B}} p_n$, then $P \vdash_{\mathcal{B}} p$.

Derivability in a base $(\vdash_{\mathcal{B}})$ is the base case of support in a base $(\Vdash_{\mathcal{B}})$ that gives the B-eS — that is, for any $p \in \text{ATOM}$, $\Vdash_{\mathcal{B}} p$ iff $\vdash_{\mathcal{B}} p$. The inductive case is given by clauses, analogous to the definition of satisfaction in M-tS.

Definition 2 (Support for IPL)

Support is the smallest relation $\Vdash$ satisfying the clauses of Figure 1.

$\Vdash_{\mathcal{B}} p$ iff $\vdash_{\mathcal{B}} p$ (At)
$\Vdash_{\mathcal{B}} \phi \to \psi$ iff $\phi \Vdash_{\mathcal{B}} \psi$ $(\to)$
$\Vdash_{\mathcal{B}} \phi \land \psi$ iff $\Vdash_{\mathcal{B}} \phi$ and $\Vdash_{\mathcal{B}} \psi$ $(\land)$
$\Vdash_{\mathcal{B}} \phi \lor \psi$ iff $\forall \mathcal{C} \supseteq \mathcal{B}\ \forall p \in \text{ATOM}$, if $\phi \Vdash_{\mathcal{C}} p$ and $\psi \Vdash_{\mathcal{C}} p$, then $\Vdash_{\mathcal{C}} p$ $(\lor)$
$\Vdash_{\mathcal{B}} \bot$ iff $\Vdash_{\mathcal{B}} p$ for any $p \in \text{ATOM}$ $(\bot)$
$\Gamma \Vdash_{\mathcal{B}} \phi$ iff $\forall \mathcal{C} \supseteq \mathcal{B}$, if $\Vdash_{\mathcal{C}} \psi$ for any $\psi \in \Gamma$, then $\Vdash_{\mathcal{C}} \phi$ (Inf)
$\Gamma \Vdash \phi$ iff $\Gamma \Vdash_{\mathcal{B}} \phi$ for all bases $\mathcal{B}$
Figure 1: Base-extension Semantics for IPL
Lemma 3 (Sandqvist [36])

$\Gamma \vdash_{\mathrm{IPL}} \phi$ iff $\Gamma \Vdash \phi$.

Soundness — that is, $\Gamma \vdash_{\mathrm{IPL}} \phi$ implies $\Gamma \Vdash \phi$ — follows from showing that support admits all the rules of Gentzen's NJ [43]. Completeness — that is, $\Gamma \Vdash \phi$ implies $\Gamma \vdash_{\mathrm{IPL}} \phi$ — is more subtle. One constructs a special base $N$ that 'simulates' Gentzen's NJ [43] and uses the clauses of the semantics to show that support in $N$ is indeed equivalent to provability in NJ.

Remark 4.

The B-eS for IPL has the following clauses for disjunction $(\lor)$:

$$\Vdash_{\mathcal{B}} \phi \lor \psi \quad\text{iff}\quad \forall \mathcal{C} \supseteq \mathcal{B}\ \forall p \in \text{ATOM},\ \text{if } \phi \Vdash_{\mathcal{C}} p \text{ and } \psi \Vdash_{\mathcal{C}} p, \text{ then } \Vdash_{\mathcal{C}} p$$

This is one significant consequence of the inferentialist setup: Piecha et al. [21, 20, 23] have shown that the standard meta-level 'or' clause — that is, $\Vdash_{\mathcal{B}} \phi \lor \psi$ iff $\Vdash_{\mathcal{B}} \phi$ or $\Vdash_{\mathcal{B}} \psi$ — yields incompleteness. Observe the clause is closely related to the 'second-order' definition of disjunction (see Prawitz [28]) — that is,

$$U + V = \forall X\,((U \to X) \to (V \to X) \to X)$$

This adumbrates the categorical perspective on B-eS given by Pym et al. [31, 30]. ◁

Remark 5.

The treatment of non-empty context is given by a base-extension,

$$\Gamma \Vdash_{\mathcal{B}} \phi \quad\text{iff}\quad \forall \mathcal{X} \supseteq \mathcal{B},\ \text{if } \Vdash_{\mathcal{X}} \psi \text{ for all } \psi \in \Gamma, \text{ then } \Vdash_{\mathcal{X}} \phi$$

While prima facie this use of base-extension appears to be related to pre-order in the standard possible-world semantics of IPL (cf. Kripke [16]), that remains to be determined. ◁

Remark 6.

Piecha et al. [21, 20, 22, 23] has questioned the use of 'extension' in (Inf) and argue that the non-extension clause

$$\Gamma \Vdash_{\mathcal{B}} \phi \quad\text{iff}\quad \text{if } \Vdash_{\mathcal{B}} \psi \text{ for all } \psi \in \Gamma, \text{ then } \Vdash_{\mathcal{B}} \phi$$

perhaps better captures a 'definitional' view of atomic systems (as opposed to a 'knowledge' view). ◁

While the B-eS for IPL is intended as an inferential semantics (see, for example, Brandom [1] and Schroeder-Heister [41]), we reiterate the skepticism suggested by Makinson [17] (see Section 1): these 'inferential semantics' may simply be used as evaluation systems without any further philosophical discussion. This is the attitude we take in the present paper. We will use the B-eS of IPL to evaluate the admissibility of rules for IPL.

3 Evaluating the Admissibility of Rules

Having provided the technical background in Section 2, we now proceed to discuss how the B-eS for IPL by Sandqvist [35] may be used to evaluate the admissibility of rule for IPL. In Section 3.1, we setup the problem: What is a rule? What is admissibility? In Section 3.2 we provide an evaluation system for admissibility.

3.1 Rules, Substitution, and Admissibility

In this section, we make precise the notion of rule and admissibility — see also Iemhoff [15]. The discussion is terse as the ideas are doubtless familiar and we only require to fix a particular presentation of them.

Definition 7 (Rule)

A rule is an expression of the form

$$\dfrac{\phi_1 \quad \cdots \quad \phi_n}{\phi}$$

We may write $\phi_1, \ldots, \phi_n / \phi$ to denote the same rule.

Example 8 (Harrop's Rule)

Harrop's Rule $h$ may be presented as follows:

$$\dfrac{\neg A \to (B \lor C)}{(\neg A \to B) \lor (\neg A \to C)}$$

It may be expressed inline as follows: $\neg A \to (B \lor C) \,/\, (\neg A \to B) \lor (\neg A \to C)$. The propositional letters $A$, $B$, and $C$ may be replaced by any other pairwise different propositional variable $A'$, $B'$, $C'$ without loss of generality. Any other replacement denotes a different rule. ◁

A rule is regarded as a general principle. A particular instance of a rule is given by uniformly replacing the propositional variables by formulas. To this end, we require the notion of substitution:

Definition 9 (Substitution)

A substitution is a map $\sigma : \text{ATOM} \to \text{FORMULA}$. It extends to formulas inductively through the syntax:

$$\sigma(\phi) := \begin{cases} \sigma(A) & \text{if } \phi = A \in \text{ATOM} \\ \sigma(\phi_1) \mathbin{\circ} \sigma(\phi_2) & \text{if } \phi = \phi_1 \circ \phi_2 \text{ for } \circ \in \{\land, \lor, \to\} \\ \bot & \text{if } \phi = \bot \end{cases}$$
Example 10 (Admissibility of Harrop's Law)

Let $\sigma$ be a substitution such that $A \mapsto A'$, $B \mapsto B'$, and $C \mapsto C'$. The following is an instance of $h$:

$$\dfrac{\neg A' \to (B' \lor C')}{(\neg A' \to B') \lor (\neg A' \to C')}$$

◁

A rule is admissible for IPL iff any instance of it preserves validity for IPL:

Definition 11 (Admissible)

A rule $\phi_1, \ldots, \phi_n / \phi$ is admissible iff for all substitutions $\sigma$, if $\vdash \sigma(\phi_i)$ for $i = 1, \ldots, n$, then $\vdash \sigma(\phi)$.

Example 12 (Example 10 cont'd)

Harrop [13] has shown that rule $h$ is admissible. ◁

Example 13.

The following rule $w$ (i.e., weakening) is admissible (see, for example, Gentzen [43]):

$$\dfrac{A \to B}{A \to (C \to B)}$$

◁

This suffices for the background on admissibility. In the remainder of the paper, we characterize the admissibility through the proof-theoretic semantics of IPL.

3.2 Evaluation System

Since NJ characterizes IPL (see Gentzen [43]) we have the following: A rule $\phi_1, \ldots, \phi_n / \phi$ is admissible iff, for any substitution $\sigma$, if $\sigma(\phi_i)$ is NJ-provable for $i = 1, \ldots, n$, then $\sigma(\phi)$ is NJ-provable. (AdmiProv)

On its own, this is neither a novel or insightful observation. However, coupled with P-tS, it becomes powerful: the point is that it only remains to characterize proofs for IPL and this is a central topic within P-tS — see, for example, Prawitz [24, 25, 26, 27, 29] and Schroeder-Heister [38]. Given a base $\mathcal{B}$, Prawitz [24] provides a basic definition of a $\mathcal{B}$-valid argument. We elide the details as they do not matter. For present purposes, it suffices to regard a $\mathcal{B}$-valid argument as an $\mathrm{NJ} \cup \mathcal{B}$-derivation; in particular, a $\emptyset$-valid argument corresponds to a NJ-derivation. Gheorghiu and Pym [9] have shown that the B-eS for IPL captures the basic notion of valid argument. Thus it characterizes provability for IPL.

Definition 14 (Entailment)

Entailment is the smallest relation $\models$ satisfying the clauses of Figure 2.

$\models_{\mathcal{B}} p$ iff $\vdash_{\mathcal{B}} p$
$\models_{\mathcal{B}} \phi \land \psi$ iff $\models_{\mathcal{B}} \phi$ and $\models_{\mathcal{B}} \psi$
$\models_{\mathcal{B}} \phi \lor \psi$ iff $\models_{\mathcal{B}} \phi$ or $\models_{\mathcal{B}} \psi$
$\models_{\mathcal{B}} \phi \to \psi$ iff $\phi \Vdash_{\mathcal{B}} \psi$
$\models_{\mathcal{B}} \bot$ iff never
Figure 2: Proof-theoretic Validity for IPL
Remark 15.

Observe in Figure 2 that in the clause for $\to$, the definition shifts from $\models$ to $\Vdash$. This is an essential step for Lemma 16 below, as discussed by Gheorghiu and Pym [9] (cf. Piecha et al. [21, 20, 23]). ◁

Lemma 16 (Gheorghiu and Pym [9])

$\Gamma \models_{\mathcal{B}} \phi$ iff there is a $\mathcal{B}$-valid argument from $\Gamma$ to $\phi$.

Remark 17.

Observe that entailment (Figure 2) and support (Figure 1) differ in the clause governing disjunction $(\lor)$: the former uses an 'introduction' clause and the latter uses an 'elimination' clause (in the sense of Gentzen's NJ). This is subtle and has been discussed by Gheorghiu et al. [9, 7, 8]. As observed in Remark 4, the elimination-form in support is essential for the completeness of support with respect to IPL, but the introduction-form in entailment delivers Lemma 16. ◁

It remains only to formally apply Lemma 16 to the problem of admissibility. We have the following: for finite $\Gamma$,

$$\Gamma \mathrel{\sim\!\!\!\mid} \phi \quad\text{iff}\quad \text{if } \models_\emptyset \psi \text{ for all } \psi \in \Gamma, \text{ then } \models_\emptyset \phi$$

The choice of $\mathrel{\sim\!\!\!\mid}$ for this symbol is a homage to Iemhoff [15] as it characterizes admissibility:

Theorem 18.

A rule $\phi_1, \ldots, \phi_n / \psi$ is admissible iff $\sigma(\phi_1), \ldots, \sigma(\phi_n) \mathrel{\sim\!\!\!\mid} \sigma(\psi)$ for any substitution $\sigma$.

Proof.

Let $\phi_1, \ldots, \phi_n / \psi$ be an admissible rule. By Definition 11, for any substitution $\sigma$, if $\vdash \sigma(\phi_i)$ for $i = 1, \ldots, n$, then $\vdash \sigma(\psi)$. By the soundness and completeness of Gentzen's NJ [43] with respect to IPL: for any formula $\chi$, $\vdash \chi$ iff there is an NJ-proof of $\chi$. We have thus established AdmiProv. By Lemma 16, there is an NJ-proof of $\chi$ iff $\models_\emptyset \chi$. Applying this to AdmiProv yields the desired result.

The point of Theorem 18 is to connect admissibility with P-tS. However, the universal quantification over substitutions renders the theorem impractical for actually evaluating the admissibility of rules. Therefore, we use the following simplification that says it suffices to consider the form of the rule:

□
Corollary 19.

A rule $\phi_1, \ldots, \phi_n / \psi$ is admissible iff $\phi_1, \ldots, \phi_n \mathrel{\sim\!\!\!\mid} \psi$.

Using Theorem 18 and Corollary 19, Figure 2 becomes an characterizes admissibility in IPL. To end this section, we now illustrate it by evaluating the admissibility of Harrop's Rule:

Example 20 (Admissibility of Harrop's Rule)

By Corollary 19, we assume $\models_\emptyset \neg A \to (B \lor C)$ and require to show $\models_\emptyset (\neg A \to B) \lor (\neg A \to C)$. Using the clauses of Figure 2, it suffices to assume $\neg A \Vdash_\emptyset B \lor C$ and show $\neg A \Vdash_\emptyset B$ or $\neg A \Vdash_\emptyset C$. We will argue for the contra-positive:

$$\text{if } \neg A \not\Vdash_\emptyset B \text{ and } \neg A \not\Vdash_\emptyset C, \text{ then } \neg A \not\Vdash_\emptyset B \lor C. \tag{$*$}$$

To this end it suffices to find a base in which everything is derived if $A$ is derived, but does not derive $B$, nor $C$, and does not support $B \lor C$.

Since (Inf) contains a universal quantifier over bases and $(*)$ is expressed in terms of the negation of the support judgement, we require to witness a base $\mathcal{X}$ such that $\Vdash_{\mathcal{X}} \neg A$, $\not\Vdash_{\mathcal{X}} B$, $\not\Vdash_{\mathcal{X}} C$, and $\not\Vdash_{\mathcal{X}} B \lor C$. Let $\mathcal{X}$ be the following rules for any $X \in \text{ATOM}$:

$$\dfrac{A}{X} \qquad \dfrac{B}{D} \qquad \dfrac{C}{D}$$

It is easy to check that $\Vdash_{\mathcal{X}} \neg A$, $\not\Vdash_{\mathcal{X}} B$ and $\not\Vdash_{\mathcal{X}} C$; so, it remains only to check that $\not\Vdash_{\mathcal{X}} B \lor C$. By the $\lor$-clause in Figure 1, we require to show that there exists $Y \in \text{ATOM}$ such that $B \Vdash_{\mathcal{X}} Y$ and $C \Vdash_{\mathcal{X}} Y$ but $\not\Vdash_{\mathcal{X}} Y$.

Choose $Y = D$. Clearly, $\not\Vdash_{\mathcal{X}} D$. Hence, it remains to verify $B \Vdash_{\mathcal{X}} D$ and $C \Vdash_{\mathcal{X}} D$. By (Inf) in Figure 1, for any $\mathcal{Y}_1, \mathcal{Y}_2 \supseteq \mathcal{X}$, if $\Vdash_{\mathcal{Y}_1} B$ and $\Vdash_{\mathcal{Y}_2} C$, then $\Vdash_{\mathcal{Y}_1} D$ and $\Vdash_{\mathcal{Y}_2} D$. This is immediate because of the rules in $\mathcal{X}$,

$$\dfrac{B}{D} \qquad \dfrac{C}{D}$$

That is, these rules are contained in both $\mathcal{Y}_1$ and $\mathcal{Y}_2$ which also prove their premisses, respectively. ◁

Remark 21.

Inspecting the evaluation in Example 20, we may wonder about the role of the negation in Harrop's Rule. For the argument to work, it is essential that the special base $\mathcal{X}$ does not, on its own, derive any atom. Hence, for example, the following rule is not admissible:

$$\dfrac{A \to (B \lor C)}{(A \to B) \lor (A \to C)}$$

It is to satisfy the condition for $\bot$ in the B-eS of IPL that we end up with the treatment of $A$ in $\mathcal{X}$ — that is, as a premiss of a rule, rather than as an axiom. However, for the argument to go through, there's no need for $A$ to be so prolific in $\mathcal{X}$. Accordingly, mutatis mutandis on Example 20, we see that the following rule is admissible:

$$\dfrac{(A \to P) \to (B \lor C)}{((A \to P) \to B) \lor ((A \to P) \to C)}$$

This is Mint's Rule [18]. It generalizes Harrop's Rule in the sense that instances of the latter are a subset of instances of the form in which $P \mapsto \bot$. ◁

4 Conclusion

The admissibility of rules in intuitionistic logic is subtle. Unlike in classical logic, there's no finite system where all admissible rules are derivable, as shown by Rybakov [32]. However, Iemhoff [15] demonstrated that a recursively enumerable system (given by Vissier [45], de Jongh [3]) fully characterizes admissibility for IPL, building on the work of Ghilardi [10].

A rule is admissible for a logic if the conclusion is valid in the logic whenever (i.e., for any substitution instance) the premises are valid. One way to characterize validity for a logic is through proof theory; for example, Gentzen [43] gave a natural deduction system NJ that characterizes IPL. Hence, a proof-theoretic approach to the question of whether or not a given rule is admissible in IPL amounts to showing that there is a proof of the conclusion whenever there is a proof of the premises. Following work by Prawitz [24, 25, 26, 27] (see also Schroeder-Heister [38, 41]), the field of proof-theoretic semantics (P-tS) has emerged, in which one of the central problems is to characterize 'proof' for a logic. Recent advances in proof-theoretic semantics, notably by Sandqvist [35] and Gheorghiu and Pym [9], offer an evaluation system for admissibility in IPL, building on the foundational work of Prawitz [24]. However, the precise relationship between this evaluation system and Iemhoff's calculus [15] remains an open question.

While the system is user-friendly, there's still a need to develop algorithmic methods for its application. The inherent non-determinism, particularly in the quantification of bases, prompts a call for systematic approaches to navigate these choices. This avenue remains a focus for future research, alongside investigations into the computational complexity of such procedures.

Acknowledgements We are grateful to Gabriele Brancati, Tim Button, Yll Buzoku, Timo Eckhardt, Timo Lang, Elaine Pimentel, David Pym, Eike Ritter, Edmund Robinson, and Tao Gu for discussions of various aspects of this work.

References

  1. Robert Brandom. Articulating Reasons: An Introduction to Inferentialism. Harvard University Press, 2000.
  2. Alexander I. Citkin. On Admissible Rules of Intuitionistic Propositional Logic. Mathematics of the USSR-Sbornik, 31(2):279, 1977.
  3. D.H.J. De Jongh. A Characterization of the Intuitionistic Propositional Calculus. In Studies in Logic and the Foundations of Mathematics, volume 60, pages 211–217. Elsevier, 1970.
  4. Michael Dummett. The Logical Basis of Metaphysics. Harvard University Press, 1991.
  5. Nissim Francez. Proof-theoretic Semantics, volume 573. College Publications London, 2015.
  6. Harvey Friedman. The Disjunction Property implies the Numerical Existence Property. Proceedings of the National Academy of Sciences, 72(8):2877–2878, 1975.
  7. Alexander V. Gheorghiu, Tao Gu, and David J. Pym. Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic. In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods — TABLEAUX, pages 367–385. Springer, 2023.
  8. Alexander V. Gheorghiu, Tao Gu, and David J. Pym. A Note on the Practice of Logical Inferentialism. 2nd Logic and Philosophy conference, 2024. In Press — arXiv:2403.10546.
  9. Alexander V. Gheorghiu and David J. Pym. From Basic Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic. arXiv:2210.05344, 2024. Accessed April 2024.
  10. Silvio Ghilardi. Unification in Intuitionistic Logic. The Journal of Symbolic Logic, 64(2):859–880, 1999.
  11. Warren Goldfarb. On Dummett's "Proof-theoretic justifications of logical laws". In Advances in Proof-theoretic Semantics, pages 195–210. Springer, 2016.
  12. Tao Gu, Alexander V. Gheorghiu, and David J Pym. Proof-theoretic Semantics for the Logic of Bunched Implications. arXiv:2311.16719, 2023. Accessed February 2024.
  13. Ronald Harrop. Concerning Formulas of the Types $A \to B \lor C$, $A \to (\exists x)B(x)$ in Intuitionistic Formal Systems. The Journal of Symbolic Logic, 25(1):27–32, 1960.
  14. W.A. Howard. The Formulae-as-Types Notion of Construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 480–490. Academic Press, 1980.
  15. Rosalie Iemhoff. On the Admissible Rules of Intuitionistic Propositional Logic. The Journal of Symbolic Logic, 66(1):281–294, 2001.
  16. Saul A Kripke. Semantical Analysis of Intuitionistic Logic I. In Studies in Logic and the Foundations of Mathematics, volume 40, pages 92–130. Elsevier, 1965.
  17. David Makinson. On an Inferential Semantics for Classical Logic. Logic Journal of IGPL, 22(1):147–154, 2014.
  18. Grigori E. Mints. Derivability of Admissible Rules. Journal of Soviet Mathematics, 6(4):417–421, 1976.
  19. Sara Negri and Jan von Plato. Structural Proof Theory. Cambridge University Press, 2008.
  20. Thomas Piecha. Completeness in Proof-theoretic Semantics. In Advances in Proof-theoretic Semantics, pages 231–251. Springer, 2016.
  21. Thomas Piecha, Wagner de Campos Sanz, and Peter Schroeder-Heister. Failure of Completeness in Proof-theoretic Semantics. Journal of Philosophical Logic, 44(3):321–335, 2015.
  22. Thomas Piecha and Peter Schroeder-Heister. The Definitional View of Atomic Systems in Proof-theoretic Semantics. In The Logica Yearbook 2016, pages 185–200. College Publications London, 2017.
  23. Thomas Piecha and Peter Schroeder-Heister. Incompleteness of Intuitionistic Propositional Logic with Respect to Proof-theoretic Semantics. Studia Logica, 107(1):233–246, 2019.
  24. Dag Prawitz. Ideas and Results in Proof Theory. In Studies in Logic and the Foundations of Mathematics, volume 63, pages 235–307. Elsevier, 1971.
  25. Dag Prawitz. The Philosophical Position of Proof Theory. In R. E. Olson and A. M. Paul, editors, Contemporary Philosophy in Scandinavia, pages 123–134. John Hopkins Press, 1972.
  26. Dag Prawitz. Towards a Foundation of a General Proof Theory. In Studies in Logic and the Foundations of Mathematics, volume 74, pages 225–250. Elsevier, 1973.
  27. Dag Prawitz. On the Idea of a General Proof Theory. Synthese, 27(1/2):63–77, 1974.
  28. Dag Prawitz. Natural Deduction: A Proof-theoretical Study. Courier Dover Publications, 2006 [1965].
  29. Dag Prawitz. An approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited. Advances in Natural Deduction: A Celebration of Dag Prawitz's Work, pages 269–279, 2014.
  30. David Pym, Eike Ritter, and Edmund Robinson. Categorical Proof-theoretic Semantics. Studia Logica, pages 1–38, 2024.
  31. David J. Pym, Eike Ritter, and Edmund Robinson. Proof-theoretic Semantics in Sheaves (Extended Abstract). In Proceedings of the Eleventh Scandinavian Logic Symposium — SLSS, 2022.
  32. Vladimir V. Rybakov. Admissibility of Logical Inference Rules. Elsevier, 1997.
  33. Tor Sandqvist. An Inferentialist Interpretation of Classical Logic. PhD thesis, Uppsala University, 2005.
  34. Tor Sandqvist. Classical Logic without Bivalence. Analysis, 69(2):211–218, 2009.
  35. Tor Sandqvist. Base-extension Semantics for Intuitionistic Sentential Logic. Logic Journal of the IGPL, 23(5):719–731, 2015.
  36. Tor Sandqvist. Hypothesis-discharging Rules in Atomic Bases. In Dag Prawitz on Proofs and Meaning, pages 313–328. Springer, 2015.
  37. Wagner de Campos Sanz, Thomas Piecha, and Peter Schroeder-Heister. Constructive Semantics, Admissibility of Rules and the Validity of Peirce's Law. Logic Journal of the IGPL, 22(2):297–308, 2014.
  38. Peter Schroeder-Heister. Validity Concepts in Proof-theoretic Semantics. Synthese, 148(3):525–571, 2006.
  39. Peter Schroeder-Heister. Proof-Theoretic versus Model-Theoretic Consequence. In Michal Pelis, editor, The Logica Yearbook 2007. Filosofia, 2008.
  40. Peter Schroeder-Heister. The Categorical and the Hypothetical: A Critique of Some Fundamental Assumptions of Standard Semantics. Synthese, 187(3):925–942, 2012.
  41. Peter Schroeder-Heister. Proof-Theoretic Semantics. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Spring 2018 edition, 2018.
  42. Will Stafford and Victor Nascimento. Following all the Rules: Intuitionistic Completeness for Generalized Proof-theoretic Validity. Analysis, 07 2023.
  43. M. E. Szabo, editor. The Collected Papers of Gerhard Gentzen. North-Holland Publishing Company, 1969.
  44. A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2000.
  45. Albert Visser. Rules and Arithmetics. Notre Dame Journal of Formal Logic, 40(1):116–140, 1999.
  46. Heinrich Wansing. The Idea of a Proof-theoretic Semantics and the Meaning of the Logical Operations. Studia Logica, 64:3–20, 2000.

This paper belongs to Gheorghiu’s research in proof-theoretic semantics; the key terms are defined in the glossary.

Related papers: Defining Logical Systems via Algebraic Constraints on Proofs · Definite Formulae, Negation-as-Failure, and Base-extension Semantics