A system of inference based on proof search: an
extended abstract

Dale Miller

► To cite this version:

Dale Miller. A system of inference based on proof search: an extended abstract. LICS 2023 - 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2023, Boston, United States. pp.1-11, 10.1109/LICS56636.2023.10175827. hal-04169014v2

HAL Id: hal-04169014

https://inria.hal.science/hal-04169014v2

Submitted on 28 Sep 2023

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A system of inference based on proof search: an extended abstract

Dale Miller

Inria Saclay & LIX, Institut Polytechnique de Paris

Palaiseau France

Orcid: 0000-0003-0274-4954

*Abstract*—Gentzen designed his natural deduction proof system to “come as close as possible to actual reasoning.” Indeed, natural deduction proofs closely resemble the static structure of logical reasoning in mathematical arguments. However, different features of inference are compelling to capture when one wants to support the process of searching for proofs. PSF (Proof Search Framework) attempts to capture these features naturally and directly. The design and metatheory of PSF are presented, and its ability to specify a range of proof systems for classical, intuitionistic, and linear logic is illustrated.

*Index Terms*—proof systems, proof search, logical frameworks

## I. INTRODUCTION

Inference and proofs are often described using proof rules of various shapes. For example, natural deduction and sequent calculus use figures such as

<figure><img src="image_2.png" /></figure>

These figures, introduced by Gentzen [1], rely on several punctuation marks such as the horizontal bar (to separate premises from conclusion), vertical dots (for reasoning from assumptions), parenthesized formulas (for discharging a formula), and the sequent arrow. The logical force implicit in the punctuation marks used to describe proofs can invade the logic specified in that framework. As Wittgenstein once stated: “Signs for logical operations are punctuation marks.” (Tractatus 5.4611, 1922). While such influence of the framework might be hard to avoid in general, we should be aware of its influence and, at times, look for alternative systems of punctuation.

Gentzen declared that his natural deduction system NJ was “a formal system which comes as close as possible to actual reasoning” [1]. Indeed, his natural deduction proof systems have had great success ranging from being used in the teaching of logical reasoning to the formal encoding of proofs as dependently typed λ-terms. However, since Gentzen’s introduction of such notation some four score and eight years ago, many different priorities for logic and proof have appeared.

While natural deduction and sequent calculus have been used successfully to describe the static structure of complete proofs (and their transformation via normalization and cut elimination), the dynamic structure of the search for proofs is less well captured by his systems. Here, issues such as partial

proofs, invertible inference rules, and don't care and don't know non-determinism are particularly important to support.

## II. DESIGN MOTIVATED

Consider a sheet of paper on which a mathematician has written several formulas at the top and one at the bottom. Such a sheet is useful to represent a proof gap, where one needs to find a logical argument that connects the given formulas at the top to the intended consequence written at the bottom. In PSF, the search for a proof is encoded as the rewriting of a collection of such proof gaps recorded on sheets. A sheet might rewrite to no additional sheets if it is recognized as trivially proved: for example, because the formula at the bottom of the sheet is also present at the top. On the other hand, a sheet can rewrite to other sheets if solving those additional sheets is understood as a way to solving the originating sheet. For example, a sheet containing the formula *even(n) ∨ odd(n)* at the top can be rewritten to make two identical copies except that *even(n)* is put at the top in one and *odd(n)* is put at the top into the other. The rule of cases would justify such a rewriting. PSF encodes such sheets as multisets of tagged formulas: if the logical formula *B* appears at the top of the sheet, it is placed into that multiset as ⌊*B*⌋; if it appears at the bottom, it is placed into that multiset as ⌊*B*⌋ (see Section V-B).

A feature of inference rules that PSF puts in prominence is the difference between *multiplicative* and *additive* inference rules. The following are examples of the additive and multiplicative versions of the right introduction for conjunction.

$$ \frac{\Gamma \vdash A, \Delta \quad \Gamma \vdash B, \Delta}{\Gamma \vdash A \wedge B, \Delta} \qquad \frac{\Gamma_1 \vdash A, \Delta_1 \quad \Gamma_2 \vdash B, \Delta_2}{\Gamma_1, \Gamma_2 \vdash A \wedge B, \Delta_1, \Delta_2} $$

More generally, an inference rule is *additive* if every sideformula occurrence (i.e., those in Γ and Δ) also occur in every premise. A rule is called *multiplicative* if every sideformula occurrence (i.e., those in Γ₁, Γ₂, Δ₁, and Δ₂) also occurs in exactly one premise. A rule with exactly one premise is necessarily both additive and multiplicative. PSF contains two operators + and × responsible for injecting additive and multiplicative features into inference systems encoded into it.

The multiplicative features of PSF are easily illustrated by the need to rewrite multisets to other multisets. In particular, multisets will be encoded as expressions built from (some fixed
set of) atomic expressions along with $\times$ for building a non-empty multiset and its unit **1** denoting an empty multiset. For example, if $a, b$, and $c$ are atomic expressions, then $a \times a \times b$ denotes the multiset that contains two occurrences of $a$ and one occurrence of $b$. Rewriting a multiset $M$ to another multiset $N$ using the rule $M_1 \mapsto M_2$ (where $M_1$ and $M_2$ are also multisets) is done using the following steps. (1) Split $M$ into two parts $M'$ and $M''$. (2) Determine that $M'$ is the same multiset as $M_1$. (3) Identify $N$ with the multiset union of $M_2$ and $M''$. The following small proof system (extended in the next section) can be used to describe such a computation.

$$ \frac{\begin{array}{c} \vdash \Delta \\ \vdash \mathbf{1}, \Delta \end{array}}{} \quad \frac{\begin{array}{c} \vdash E_1, E_2, \Delta \\ \vdash E_1 \times E_2, \Delta \end{array}}{} \quad \frac{\begin{array}{c} \overline{E \vdash E} \\ \overline{E_1 \vdash \Delta_1} \quad \vdash E_2, \Delta_2 \quad \mathbf{1} \vdash \Delta_1 \quad E_1 \vdash \Delta_1 \quad E_2 \vdash \Delta_2 \end{array}}{} \quad \frac{\begin{array}{c} \vdash \Delta_1 \quad \vdash \Delta_2, \Delta_2 \quad \mathbf{1} \vdash \Delta_1, \Delta_2 \end{array}}{} $$

The left-introduction rule for $\mapsto$ achieves the three steps mentioned above. Step (1) is captured by splitting a multiset into the union of $\Delta_1$ and $\Delta_2$ in that rule's conclusion. Steps (2) and (3) are captured by the proofs of its left and right premises, respectively. The rewriting of the multiset $\{a, a, b\}$ into $\{a, c\}$ by the rule that replaces $a$ and $b$ with $c$ is witnessed by a derivation of $a \times b \mapsto c \vdash a, a, b$ from the open premise $\vdash a, c$.

Additive features are also incorporated into **PSF** using $+$ and its unit **0**: in particular, collections of multisets are represented as a $+$ of $\times$ of atomic expressions. Below we list three additional features abstracted from searching for proofs based on evolving collections of sheets.

a) *Linear and classical realms:* When rewriting a sheet of paper to possibly other sheets, it is usually the case that some items are retained while others might disappear. In particular, an assumption at the top of a sheet is usually retained on all subproblems that are eventually rewritten from it, while the goal formula on one sheet may or may not change. For example, if the goal formula is $A \supset B$, then that goal is replaced by the goal formula $B$ with $A$ simultaneously added at the top of the sheet. The **PSF** recognizes this distinction by classifying atomic expressions as being in either the *linear realm*—where such expressions might be deleted or replaced—or the *classical realm*—where such expressions persist through all evolutions of a multiset. (There is a strong influence of linear logic [2] on the design of **PSF**.)

b) *Bottom-up and top-down reasoning:* These proof search styles appear in various different disguises in computational logic. They differentiate Prolog from Datalog and tableaux from resolution [3]. Term representation is often described using top-down proof structures, while term representations that allow for explicit sharing can be justified using bottom-up proof structures [4]. In **PSF**, this distinction comes into play using the notions of bias assignment and debts.

c) *Don't care and don't know non-determinism:* The non-determinism encountered in the search for proofs can be categorized as being either the *don't care* or *don't know* varieties. In **PSF**, inference rules will eventually be organized

### THE RIGHT RULES

$$ \frac{\Gamma \vdash \mathbf{0}, \Delta}{\Gamma \vdash \mathbf{0}, \Delta} \qquad \frac{\Gamma \vdash E_1, \Delta \quad \Gamma \vdash E_2, \Delta}{\Gamma \vdash E_1 + E_2, \Delta} \\ \frac{\Gamma \vdash \Delta}{\Gamma \vdash \mathbf{1}, \Delta} \qquad \frac{\Gamma \vdash E_1, E_2, \Delta}{\Gamma \vdash E_1 \times E_2, \Delta} $$

### THE LEFT RULES

$$ \frac{\Gamma, R_i \vdash \Delta}{\mathbf{1} \vdash \Gamma, R_1 + R_2 \vdash \Delta} \quad \frac{\Gamma_1, R_1 \vdash \Delta_1 \quad \Gamma_2, R_2 \vdash \Delta_2}{\Gamma_1, \Gamma_2, R_1 \times R_2 \vdash \Delta_1, \Delta_2} \\ \frac{\Gamma_1, R \vdash \Delta_1 \quad \Gamma_2 \vdash E, \Delta_2}{\Gamma_1, \Gamma_2, R \mapsto E \vdash \Delta_1, \Delta_2} \quad \frac{R \vdash \Upsilon \quad \Gamma \vdash E, \Delta, \Upsilon}{\Gamma, R \mapsto E \vdash \Delta, \Upsilon} \\ \frac{\Gamma \vdash \Delta}{\vdash \Delta} \quad \begin{array}{l} \text{decide, } \Gamma \subseteq \mathcal{R} \text{ is non-empty and finite} \\ \frac{\Gamma \vdash \bar{A}, \Delta \quad \delta(A) = +1}{\Gamma, A \vdash \Delta} \quad \text{debit}_1 \\ \frac{\vdash \bar{S}, \Upsilon \quad \delta(S) = +2}{S \vdash \Upsilon} \quad \text{debit}_2 \end{array} $$

### THE IDENTITY RULES

$$ \overline{E \vdash E} \quad \text{init} \quad \overline{\vdash \bar{A}, A} \quad \text{iou} $$

### THE STRUCTURAL RULES

$$ \frac{\Gamma \vdash \Delta, S, S}{\Gamma \vdash \Delta, S} \quad cR \quad \frac{\Gamma \vdash \Delta}{\Gamma \vdash \Delta, S} \quad wR $$

<caption>Fig. 1. The **B** proof system.</caption>

into two phases: the *right phase* will capture don't care non-determinism and the *left phase* will capture don't know non-determinism.

**PSF** is presented using two inference system. The basic system, **B**, is presented in Section III while a more structured variant, **F**, is presented in Section IV.

### III. THE BASIC INFERENCE SYSTEM **B**

Fig. 1 contains the inference system **B**, which contains all the features we have motivated so far: additive and multiplicative structures, proof state rewriting, debts, and the linear and classical realms. The schematic variables used in Fig. 1 are the following. The variable $A$ ranges over some fixed set of atomic expressions. The variables $E$ and $R$ range over expressions and rules and are defined as follows.

$$ \begin{array}{l} E ::= A \mid \mathbf{0} \mid E_1 + E_2 \mid \mathbf{1} \mid E_1 \times E_2 \\ R ::= A \mid \mathbf{0} \mid R_1 + R_2 \mid \mathbf{1} \mid R_1 \times R_2 \\ \qquad \mid R \mapsto E \mid R \mapsto E \end{array} $$

The operators $\mapsto$ and $\Rightarrow$ associate to the left while the operators $+$ and $\times$ associate to the right. A *debt* is an expressions of the form $\overline{A}$. The variable $\Gamma$ ranges over multisets containing $R$-expressions, and the variable $\Delta$ ranges over multisets that can contain both $E$-expressions and debts. The variable $\mathcal{R}$ denotes some countable set of $R$-expressions. The function
$\delta(\cdot)$ is a bias assignment: it maps atomic expressions to the set $\{-2, -1, +1, +2\}$ (a similar bias assignment was used in [5]). The atomic expression $A$ is in the linear realm if $\delta(A)$ is $\pm 1$ and in the classical realm if $\delta(A)$ is $\pm 2$. If $\delta(A) > 0$ then a debit rule can be used with $A$. The variable $\Upsilon$ ranges over finite multisets of atomic expressions in the classical realm, and the variable $S$ ranges over atomic expressions in the classical realm.

A **B-proof** is *atomically closed* if all occurrences of the *init* rule in it involve only atomic expressions, i.e., they are of the form $A \vdash A$ for an atomic expression $A$.

**Proposition 1 (Completeness of atomically closed B-proofs):**
If the sequent $\vdash \Delta$ has a **B-proof** then it has an atomically closed **B-proof**.

*Proof.* A simple induction on the structure of $E$ shows that any occurrence of $E \vdash E$ in which $E$ is not an atomic expression can be replaced by a proof that is atomically closed. $\square$

The proofs below concerning the **B** proof system will implicitly apply the structural rules for atomic expressions with bias assignments of $\pm 2$. In particular, the part of a context composed of just such atomic expressions, usually denoted with the $\Upsilon$ variable, will be treated additively even within multiplicative rules.

**Proposition 2 (Clip-admissibility for B-proofs):** The following inference rule (a simpler version of Gentzen's cut rule) is admissible in **B**.

$$ \frac{\Gamma_1 \vdash \Delta_1, E, \Upsilon \quad \Gamma_2, E \vdash \Delta_2, \Upsilon}{\Gamma_1, \Gamma_2 \vdash \Delta_1, \Delta_2, \Upsilon} \text{ clip} $$

*Proof.* Consider the following **B**-proof with exactly one occurrence of the *clip* rule.

$$ \frac{\Xi_1 \quad \Xi_2}{\Gamma_1 \vdash \Delta_1, E, \Upsilon \quad \Gamma_2, E \vdash \Delta_2, \Upsilon} \text{ clip} $$

By Proposition 1, we can assume that both $\Xi_1$ and $\Xi_2$ are atomically closed. We proceed by considering the structures of $\Xi_1$ and $\Xi_2$. If either of these proofs ends in a right rule for $\Delta_1$ or $\Delta_2$, we can permute those rule occurrences down. Thus, we can assume that $\Delta_1$ and $\Delta_2$ are multisets of atomic expressions. Under this assumption, we can also permute down any left rule that might terminate $\Xi_2$. In this case, we can assume that $\Gamma_2$ is empty. All that is left is showing how to permute the *clip* rule up into the left premise proof.

Consider the following instance of *clip*. Here, $E$ is either not atomic or it is atomic and $\delta(E) = \pm 1$.

$$ \frac{\frac{\Xi_1 \quad \Xi_2}{R \vdash \Upsilon \quad \Gamma_1 \vdash E, E', \Delta_1, \Upsilon} \quad \Xi_3}{\Gamma_1, R \Rightarrow E' \vdash E, \Delta_1, \Upsilon \quad E \vdash \Delta_2, \Upsilon} \text{ clip} $$

This instant can be rewritten to be

$$ \frac{\Xi_1 \quad \Xi_2 \quad \Xi_3}{R \vdash \Upsilon \quad \frac{\Gamma_1 \vdash E, E', \Delta_1, \Upsilon \quad E \vdash \Delta_2, \Upsilon}{\Gamma_1, R \Rightarrow E' \vdash \Delta_1, \Delta_2, \Upsilon}} \text{ clip} $$

In the case that $E$ is an atomic expression and $\delta(E) = \pm 2$ then the last inference rule of is either *init* (in which case, *clip* is easily removed since $E \in \Upsilon$) or *debit*$_2$ and, in that case, $\Delta_2$ is empty (or a structural rule). In this final case, the proof above can be rewritten as

$$ \frac{\frac{\Xi_1 \quad \Xi_3}{R \vdash E, \Upsilon \quad E \vdash \Upsilon} \text{ clip}}{R \vdash \Upsilon} \quad \frac{\frac{\Xi_1 \vdash E, E', \Delta_1, \Upsilon \quad E \vdash \Upsilon}{\Gamma_1 \vdash E', \Delta_1, \Upsilon} \text{ clip}}{R \Rightarrow E' \vdash \Delta_1, \Upsilon} $$

The other cases regarding the structure of the *R*-expression in $\Gamma$ are simple and direct.

The only remaining cases to consider is when $\Xi_1$ is a right rule introducing $E$ and $\Xi_2$ is a left rule introducing $E$. These cases are discussed below (remembering that $\Gamma_2$ is empty).

It is not possible for $E$ to be **0** since there is no such proof $\Xi_2$. If $E$ is **1**, then $\Delta_2$ is empty and $\Xi_1$ replaces the *clip* rule. If $E$ is $E_1 + E_2$ then we must have

$$ \frac{\frac{\Xi_1' \quad \Xi_1''}{\Gamma_1 \vdash \Delta_1, E_1 \quad \Gamma_1 \vdash \Delta_1, E_2}}{\Gamma_1 \vdash \Delta_1, E_1 + E_2} \quad \frac{\Xi_2' \quad \Xi_2''}{E_1 \vdash \Delta_2 \quad E_1 + E_2 \vdash \Delta_2} \text{ clip} $$

(where $\Delta_1$ and $\Delta_2$ contain only atomic expressions). This instance of *clip* can be replaced by the following instance of *clip* on smaller expressions.

$$ \frac{\Xi_1' \quad \Xi_2''}{\Gamma_1 \vdash \Delta_1, E_1 \quad E_1 \vdash \Delta_2} \text{ clip} $$

The symmetric case is handled the same. If $E$ is $E_1 \times E_2$ then we must have

$$ \frac{\frac{\Xi_1' \quad \Xi_2' \quad \Xi_2''}{\Gamma_1 \vdash \Delta_1, E_1, E_2 \quad E_1 \vdash \Delta_2' \quad E_2 \vdash \Delta_2''}}{\Gamma_1 \vdash \Delta_1, E_1 \times E_2} \text{ clip} $$

(where $\Delta_1$ and $\Delta_2$ contain only atomic expressions). This instance of *clip* can be replaced by the following instance of *clip* on smaller expressions.

$$ \frac{\frac{\Xi_1' \quad \Xi_2'}{\Gamma_1 \vdash \Delta_1, E_1, E_2 \quad E_1 \vdash \Delta_2'}}{\Gamma_1 \vdash \Delta_1, \Delta_2', E_2 \quad E_2 \vdash \Delta_2''} \text{ clip} $$

In general, one occurrence of *clip* can be replaced by two *clips*. Standard induction arguments can now be used to complete this proof. $\square$

**Proposition 3 (Right rules are invertible):** The right rules are invertible. In particular, if $E$ is not atomic and the sequent $\vdash E, \Delta$ is provable, then there is a proof of this sequent in which the last inference rule is an introduction rule for $E$.
**Proof** Let $\Xi$ be a proof of $\vdash E_1 \times E_2, \Delta$. Consider

$$ \frac{\Xi \quad \frac{\overline{E_1 \vdash E_1} \text{ init}}{\vdash E_1 \times E_2, \Delta} \quad \frac{\overline{E_2 \vdash E_2} \text{ init}}{\Gamma \vdash E_1, E_2}}{\frac{\Gamma \vdash E_1, E_2, \Delta}{\Gamma \vdash E_1 \times E_2, \Delta}} \text{ clip} $$

By Proposition 2, this proof with *clip* can be replaced by a proof without *clip*: that proof ends in the introduction of $E_1 \times E_2$. The case where $E$ is **1** is similar and simpler. Let $\Xi$ be a proof of $\vdash E_1 + E_2, \Delta$. Consider

$$ \frac{\Xi \quad \frac{\overline{E_1 \vdash E_1} \text{ init}}{\vdash E_1 + E_2, \Delta} \quad \frac{\overline{E_1 + E_2 \vdash E_1}}{\Gamma \vdash \Delta, E_1}}{\frac{\Gamma \vdash \Delta, E_1 + E_2}{\Gamma \vdash \Delta, E_1 + E_2}} \text{ clip} \quad \frac{\text{similar}}{\text{clip}} $$

By Proposition 2, this proof with *clip* can be replaced by a proof without *clip*. The case where $E$ is **0** is immediate. □

**Proposition 4 (Clipping out debt):** Let $C$ be an atomic expression. If $\delta(C) = +1$, the following $dclip_1$ rule is admissible.

$$ \frac{\vdash \Delta_1, C \quad \vdash \Delta_2, \bar{C}}{\vdash \Delta_1, \Delta_2} dclip_1 $$

If $\delta(C) = +2$, the following $dclip_2$ rule is admissible.

$$ \frac{\vdash \Delta, C \quad \vdash \Upsilon, \bar{C}}{\vdash \Delta, \Upsilon} dclip_2 $$

**Proof** Consider the following **B**-proof with one occurrence of $dclip_1$: here, $\delta(C) = +1$.

$$ \frac{\Xi_1 \quad \Xi_2}{\vdash \Delta_1, C \quad \vdash \Delta_2, \bar{C}} \quad dclip_1 $$

This proof can be rewritten as

$$ \frac{\Xi_1 \quad \Xi_2}{\vdash \Delta_1, C \quad \frac{\vdash \Delta_2, \bar{C}}{C \vdash \Delta_2}} \quad \begin{array}{l} \text{debit}_1 \\ \text{clip} \end{array} $$

Apply Proposition 2 to finish this case. Consider the following proof with one occurrence of $dclip_2$: here, $\delta(C) = +2$.

$$ \frac{\Xi_1 \quad \Xi_2}{\vdash \Delta, C \quad \vdash \Upsilon, \bar{C}} \quad dclip_2 $$

This proof can be rewritten as

$$ \frac{\Xi_1 \quad \Xi_2}{\vdash \Delta, C \quad \frac{\vdash \Upsilon, \bar{C}}{C \vdash \Upsilon}} \quad \begin{array}{l} \text{debit}_2 \\ \text{clip} \end{array} $$

Apply Proposition 2 to finish this case. □

If an atomic expression $A$ has a positive bias value, the *debit* rule allows turning an obligation into find $A$ in the current multiset into a promise to pay that obligation later, possibly

after additional rewriting takes place. The proposition theorem states that once a complete proof is built, possibly using the *debit* rules, it is possible to reorganize that proof so that no *debit* rules are used.

**Proposition 5 (Completeness without debit):** If the sequent $\vdash \Delta$ has a **B**-proof, it has a proof without the $debit_1$ and $debit_2$ rules.

**Proof** We systematically replace an occurrence of the $debit_1$ inference rule (above a *decide* rule) with *init* and $dclip_1$ (below the *decide* rule). That is, we transform

$$ \frac{\Xi \quad \frac{\overline{\Delta}, \Delta_0}{A \vdash \Delta_0} \quad debit_1}{\dots \quad \vdots \quad \dots} \quad \frac{\Gamma \vdash \Delta_0, \Delta_1}{\vdash \Delta_0, \Delta_1} \quad decide $$

into the following proof containing $dclip_1$. Here, we replaced $\Delta_0$ with $A$ in some of the sequents and then used the *clip* rule to reintroduce the $\Delta_0$ expressions.

$$ \frac{\overline{A \vdash A} \text{ init}}{\dots \quad \vdots \quad \dots} \quad \frac{\frac{\Gamma \vdash A, \Delta_1}{\vdash A, \Delta_1} \quad decide \quad \Xi}{\vdash \Delta_0, \Delta_1} \quad dclip_1 $$

We also can systematically replace an occurrence of the $debit_2$ inference rule (above a *decide* rule) with *init* and $dclip_2$ (below the *decide* rule). That is, we transform a **B**-proof of the form

$$ \frac{\Xi \quad \frac{\overline{\Delta}, \Upsilon}{A \vdash \Upsilon} \quad debit_1}{\dots \quad \vdots \quad \dots} \quad \frac{\Gamma \vdash \Upsilon, \Delta}{\vdash \Upsilon, \Delta} \quad decide $$

with the following proof with $dclip_2$ below. Here, we replaced $\Upsilon$ with $A$ in some of the sequents and used the $dclip_2$ rule to reintroduce the $\Upsilon$ expressions.

$$ \frac{\overline{A \vdash A} \text{ init}}{\dots \quad \vdots \quad \dots} \quad \frac{\frac{\Gamma \vdash A, \Delta}{\vdash A, \Delta} \quad decide \quad \Xi}{\vdash \Upsilon, \Delta} \quad dclip_2 $$

Thus, we have replaced one occurrence of either $debit_1$ or $debit_2$ with one occurrence of $dclip_1$ or $dclip_2$, respectively. Using Proposition 4, we have a *clip*-free proof with one fewer *debit* rules. Note that *clip* elimination does not introduce *debit* when there is no *debit* in the original proof. □
A **B-proof** Ξ is reduced if every occurrence of the **decide** rule has a right-hand side containing only atomic expressions or debts.

The major premises of the left rules are defined as follows. Those rules with only a single premise have that sole premise as their major premise. Both premises of the left-introduction rule for × are major premises. Finally, the left-most premise is the major premise for the introduction rules for ↦ and ⇄. Note that if the right-hand side of the conclusion of a left rule occurrence contains only atomic expressions, then this is true of the major premises of that rule occurrence.

**Proposition 6 (Completeness of reduced B-proofs):** If the sequent $\vdash \Delta$ has a **B-proof**, it has a reduced proof.

*Proof* An occurrence of a sequent in Ξ is bad if that sequent is the conclusion of a left rule and a major premise of that rule is the conclusion of a right-introduction rule. Note that the right-hand side of a bad sequent occurrence must contain a non-atomic expression. The measure of a bad occurrence of a sequent is the height of its subproof in Ξ. The measure of the **B-proof** Ξ is the multiset of the measure of all bad sequents in Ξ. We prove that if the measure of Ξ is not the empty multiset, then we can replace Ξ with another proof of the same end- sequent but with strictly smaller multiset ordering.

Assume that the measure of Ξ is non-empty. Then there exists a sequent with a bad occurrence in Ξ. Pick one of these with minimal height and assume that that sequent is of the form $\Gamma \vdash \Delta$. As noted above, there must be a non-atomic expression in $\Delta$. Hence, the last left rule cannot be either *debit*₂ or the left-introduction rule for **1**. Thus, we only need to consider six left rules (*decide*, *debit*₁, and one each for ×, +, ↦, ⇄). Since there are four right introduction rules (one for each of **1**, ×, 0, +) then we have 24 possible combinations of rules that can yield the bad occurrence $\Gamma \vdash \Delta$. If the upper rule is the right-introduction of **0** or **1**, then we can trivially permute that rule down. We illustrate a few more cases. The remaining ones are similar.

$$ 
\begin{array}{c}
\begin{array}{ccc}
\frac{\begin{array}{c} \Xi_1 \\ R_1 \vdash E_1, \Delta_1 \end{array} & \begin{array}{c} \Xi_2 \\ R_1 \vdash E_2, \Delta_1 \end{array} & \begin{array}{c} \Xi_3 \\ R_2 \vdash \Delta_3 \end{array} \\
\hline
\frac{R_1 \vdash E_1 + E_2, \Delta_1}{R_1 \times R_2 \vdash E_1 + E_2, \Delta_1, \Delta_2}
\end{array} \rightarrow \\
\\
\begin{array}{ccc}
\frac{\begin{array}{c} \Xi_1 \\ R_1 \vdash E_1, \Delta_1 \end{array} & \begin{array}{c} \Xi_3 \\ R_2 \vdash \Delta_2 \end{array} & \begin{array}{c} \Xi_2 \\ R_1 \vdash E_2, \Delta_1 \end{array} & \begin{array}{c} \Xi_3 \\ R_2 \vdash \Delta_2 \end{array} \\
\hline
\frac{R_1 \times R_2 \vdash E_1, \Delta_1, \Delta_2}{R_1 \times R_2 \vdash E_1 + E_2, \Delta_1, \Delta_2}
\end{array} & R_1 \times R_2 \vdash E_1 + E_2, \Delta_1, \Delta_2 \\
\\
\begin{array}{ccc}
\frac{\begin{array}{c} \Xi_1 \\ R \vdash E_1, E_2, \Delta_1 \end{array} & \begin{array}{c} \Xi_2 \\ R \vdash E_1 \times E_2, \Delta_1 \end{array} & \begin{array}{c} \Xi_3 \\ R \vdash E_1 \times E_2, \Delta_1, \Delta_2 \end{array} \\
\hline
\frac{R \vdash E_1 \times E_2, \Delta_1}{R \vdash E_1 \vdash E_1 \times E_2, \Delta_1, \Delta_2}
\end{array} \rightarrow \\
\\
\begin{array}{ccc}
\frac{\begin{array}{c} \Xi_1 \\ R \vdash E_1, E_2, \Delta_1 \end{array} & \begin{array}{c} \Xi_2 \\ R \vdash E_1, E_2, \Delta_1 \end{array} & \begin{array}{c} \Xi_2 \\ R \vdash E_1, E_2, \Delta_1, \Delta_2 \end{array} \\
\hline
\frac{R \vdash E_1 \vdash E_1, E_2, \Delta_1, \Delta_2}{R \vdash E_1 \vdash E_1 \times E_2, \Delta_1, \Delta_2}
\end{array} & R \vdash E_1 \vdash E_1 \times E_2, \Delta_1, \Delta_2
\end{array}
$$

(We have assumed that these sequents have a left-hand side with at most two expressions: these cases are easily extended

to the more general case.) Note that in the last pair of proofs, for example, the bad occurrence of the sequent is moved up, but the sequent $R \mapsto E \vdash E_1, E_2, \Delta_1$ may be a bad occurrence in the result: if that is the case, its measure has decreased. In this way, the measure decreases whenever we permute such rules. □

Since the *decide* rule in **B** allows for deciding on $\Gamma$ with multiple expressions, we say that **B-proofs** are, in general, *multi-decide* proofs. A **B-proof** is a *single-decide* proof if every occurrence of the *decide* rule in it decides on exactly one expression. While allowing multi-decide proofs was a convenience for proving the clip-elimination result (Proposition 2), we maintain completeness by restricting to single-decide proofs.

**Proposition 7 (Completeness of single-decide proofs):** A **B** provable sequent has single-decide **B-proof**.

*Proof* In principle, deciding on multiple expressions can be done sequentially. Since all left rules permute over each other, we can assume that the left rules are done in a *focused* manner: that is, the immediate subexpressions of an *R*-expressions in major premises can be introduced in the proof of that major premise (we also include the use of *init* or a *debit* rule). Schematically, we can then take instances of the *decide* rule of the form

$$ \frac{\frac{\Gamma_i \vdash \Delta_i}{\vdots} \dots}{R, \Gamma \vdash \Delta \quad \vdash \Delta} \quad \text{decide} $$

where $\Gamma$ is non-empty and $\Gamma_i$ is a sub-multiset of $\Gamma$ and where $i \in \{1, \dots, n\}$ for some positive $n$. If $\Gamma_i$ is non-empty, then we can transform this proof into

$$ \frac{\frac{\Gamma_i \vdash \Delta_i}{\vdots} \dots}{R \vdash \Delta \quad \vdash \Delta} \quad \text{decide} $$

An inductive argument can be used to remove all *decide* rules that decide on more than one rule. □

## IV. THE TWO-PHASE INFERENCE SYSTEM **F**

The **B** inference system supports the basic features we motivated in Section II that should be present in an inference system that supports the search for proofs. At the same time, **B** can be improved significantly to better support such search.

In the previous section, we have taken steps in that direction already. The completeness of single-decide proofs means that we do not need to consider selecting collections of rules at a time because selecting them one at a time is just as complete. Similarly, the completeness of reduced proofs implies that the search for proofs can be done by first doing all possible right rules, then selecting one *R*-expression for the *decide* rule, and then doing only left rules along the major premises.
<figure><img src="image_3.png" /><figcaption>Fig. 2. The two-phase inference system F. The proviso $\dagger$ for the release rule states that $E$ is either not atomic or it is atomic and $\delta(E) < 0$.</figcaption></figure>

There are, however, still defects in the search for proofs since there remains some non-determinism in the search for (reduced and single-decide) B-proofs that can be removed. For example, $A \vdash A$ can be proved using *init*, but, if $\delta(A) = +1$, it can also be proved using both *debit*₁ and *iou*. Also, the rules of contraction and weakening can be applied at almost any moment during search.

The two-phased proof system in F, given in Fig. 2, captures only reduced and single-decide proofs and where these two non-deterministic choices are resolved. There are two kinds of sequents in F, namely $\vdash \Delta$ and $\vdash R \vdash A$, where $\Delta$ is a multiset of E-expressions, R is an R-expression, and A is a multiset of atomic expressions. When comparing this proof system to B, there is a clear separation on left and right rules. A sequent of the form $\vdash A$ is called a *border sequent*.

Note that in F, if $\delta(A) = +1$ and we encounter $\vdash A \vdash A$, then only the *debit*₁ and *iou* rules can be used to prove it: the *initL* rule is not available. Also, the two structural rules are built into this proof system using the schematic variable $\Upsilon$ to denote a multiset of atomic expressions in the classical realm: this is achieved by treating the part of the context identified as $\Upsilon$ as additive even in multiplicative rules.

The proof of the following relative completeness theorem for F proofs follows from the completeness for reduced and single-decide proofs (Propositions 6 and 7).

**Proposition 8:** Let $\Delta$ be a multiset containing E-expressions and debits. Then, $\vdash \Delta$ is provable in B if and only if $\vdash \Delta$ is provable in F.

The proof system F is a two-phase proof system since all

of its inference rules can be organized into the following two phases. A *left phase* is a derivation composed of only left rules and $\vdash$ sequents: this phase has a border sequent as its conclusion, and its premises are the conclusion of either *release*, *debit*₁, or *debit*₂. There are possibly many choices to make during the construction of a left phase (the choice of $R \in \mathcal{R}$, the choice of $i$ in the left rule for $+$, and the choice of how to split the side expressions among premises) and, as a result, this phase encapsulates *don't know non-determinism*. A *right phase* is a derivation composed of only right rules: all of the premises of this phase are border sequents, and its conclusion is either the conclusion of the full proof or is the premise of either *release*, *debit*₁, or *debit*₂. Note that there might be many ways to build a right phase formally but they all relate their conclusion to the same collection of premises. In this sense, right phases encapsulate *don't care non-determinism*.

A synthetic rule is composed of one left phase and zero or more right phases, one for each premise of the left phase. In particular, the conclusion and all the premises of a synthetic rule are border sequents. We say that a synthetic rule is for R if the last rule (necessarily a *decide rule*) decides on R.

Note that the right rules and, hence, the right phase seen as a single rule, is additive (see Section II). If there are no atomic expressions with bias assignment $\pm 2$ then the left rules, and the left phase seen as a single rule, are multiplicative. If atomic expressions have bias $\pm 2$ then these are treated additively even in otherwise multiplicative rules.

The primary purpose of the F proof system over the B proof system is that the former is used to generate synthetic inference rules from R expressions. In the next section, we provide several illustrations of how R expressions can be used to specify various proof systems involving logical formulas.

## V. APPLICATIONS OF B AND F

### A. Specifying Fibonacci numbers

Denote by $f(n)$ the $n^{th}$ Fibonacci number and let $\mathcal{R}$ be the union of $\{F(0,0), F(1,1)\}$ and the set

$$ \{F(n + 2, x + y) \mapsto F(n + 1, x) \mapsto F(n, y) \mid n, x, y \in \mathbb{Z}\}. $$

To determine the synthetic rules that can arise from $\mathcal{R}$, consider the three cases for the value of $\delta(F(\cdot, \cdot))$.

If $\delta(F(\cdot, \cdot)) < 0$ then the synthetic rules are

$$ \begin{array}{ccc} \vdash F(0, 0) & \vdash F(1, 1) & \begin{array}{l} \vdash F(n + 1, x) \vdash F(n, y) \\ \vdash F(n + 2, x + y) \end{array} \end{array} $$

The sequent $\vdash F(n, f(n))$ has a unique proof using these rules, and its size is exponential in $n$.

If $\delta(F(\cdot, \cdot)) = +1$: then the synthetic rules are

$$ \begin{array}{ccc} \vdash \Delta, \overline{F(0, 0)} & \vdash \Delta, \overline{F(1, 1)} & \begin{array}{l} \vdash \overline{F(n + 2, x + y)}, \Delta \\ \vdash \overline{F(n + 1, x)}, \overline{F(n, y)}, \Delta \end{array} \end{array} $$

The sequent $\vdash F(n, f(n))$ is provable and the sizes of such proofs are exponential in $n$. While bottom-up reasoning is
taking place, contraction is not available on debts. As a result, there is no sharing of previous computations.

Finally, if $\delta(F(\cdot, \cdot)) = +2$, then the synthetic rules are the same as the previous case except that $\Delta$ must be replaced with $\Upsilon$.

$$ \frac{\vdash \Upsilon, \overline{F(0,0)}}{\vdash \Upsilon} \qquad \frac{\vdash \Upsilon, \overline{F(1,1)}}{\vdash \Upsilon} \qquad \frac{\vdash \overline{F(n+2, x+y)}, \Upsilon}{\vdash \overline{F(n+1, x)}, \overline{F(n, y)}, \Upsilon} $$

The sequent $\vdash F(n, f(n))$ is provable only when $n \le 3$.

Another specification of the Fibonacci series uses a more deliberate reuse strategy. Let $n \ge 0$ and let $\mathcal{R}_n$ be the set of rules that is the union of the singleton $\{F(n, f(n)) \mapsto \mathbf{0}\}$ and all the rules of the form

$$ F(m+1, x) \times F(m, y) \mapsto F(m+2, x+y) \times F(m+1, x) $$

where $m, x, y$ are natural numbers. In this case, the sequent $\vdash F(0, 0) \times F(1, 1)$ is provable from $\mathcal{R}_n$ with a proof of size linear in $n$.

## B. Classical and intuitionistic logic

The main reason to introduce **PSF**, via the **B** and **F** proof systems, is to provide a specification framework for inference rules. When comparing different proof systems (e.g., a target and an encoding of it), three levels of adequacy naturally arise [6]. The weakest level of adequacy is relative completeness, which considers only provability: a formula has a proof in one system if it has a proof in the other system. A stronger level of adequacy is of full completeness of proofs: the proofs in one system are in one-to-one correspondence with proofs in the other system. If one uses the term “derivation” for possibly incomplete proofs (proofs that may have open premises), then the strongest version of adequacy is that of full completeness of derivations, where every derivation (such as inference rules themselves) are in one-to-one correspondence with those in the other system.

Unless otherwise mentioned, the encodings of proof systems described below will all be at the highest level of adequacy. In particular, one inference rule in a target proof system (say, a rule in natural deduction) will correspond to a synthetic rule in **F**.

Recalling now the discussion in Section II regarding representing the state of the search for a proof as a collection of sheets, these sheets are represented as multisets of atomic expressions of the form $\lfloor B \rfloor$ and $\lceil B \rceil$, where $B$ denotes a logical formula. Here, the expression $\lfloor B \rfloor$ tags $B$ as coming at the top of a sheet while $\lceil B \rceil$ tags $B$ as coming at the bottom of a sheet.

The rules in Fig. 3 can be used to describe natural deduction in intuitionistic logic and the sequent calculus for both intuitionistic and classical logic. In all of these cases, classical logic is captured using the polarities $\delta(\lfloor \cdot \rfloor) = \pm 2$ and $\delta(\lceil \cdot \rceil) = \pm 2$. In contrast, intuitionistic logic is captured using the polarities $\delta(\lfloor \cdot \rfloor) = \pm 2$ and $\delta(\lceil \cdot \rceil) = \pm 1$. Here, we are considering only propositional logic with the logical constants $\supset$ (implication), $\wedge$ (conjunction), $\vee$ (disjunction), $\vdash$ (truth), and $\perp$ (false). (First-order quantification is addressed in Section V-H.)

$$ \begin{array}{lclcl} (\supset L^m) & \lfloor A \supset B \rfloor & \mapsto & \lfloor A \rfloor & \Rightarrow \lfloor B \rfloor \\ (\supset R^m) & \lfloor A \supset B \rfloor & \mapsto & \lfloor A \rfloor & \times \lfloor B \rfloor \\ (\wedge L^a) & \lfloor A \wedge B \rfloor & \mapsto & \lfloor A \rfloor & \\ (\wedge R^a) & \lfloor A \wedge B \rfloor & \mapsto & \lfloor A \rfloor & + \lfloor B \rfloor \\ (\wedge L^a) & \lfloor A \wedge B \rfloor & \mapsto & \lfloor B \rfloor & \\ (\vee L^a) & \lfloor A \vee B \rfloor & \mapsto & \lfloor A \rfloor & + \lfloor B \rfloor \\ (\vee R^a) & \lfloor A \vee B \rfloor & \mapsto & \lfloor A \rfloor & \\ (\vee R^a) & \lfloor A \vee B \rfloor & \mapsto & \lfloor B \rfloor & \\ (\perp L^a) & \lfloor \perp \rfloor & \mapsto & \mathbf{0} & \\ (\top R^a) & \lfloor \top \rfloor & \mapsto & \mathbf{0} & \\ (\mathrm{Id}_1) & \lfloor C \rfloor & \times \lfloor C \rfloor & & \\ (\mathrm{Id}_2) & \mathbf{1} & \mapsto \lfloor C \rfloor & \Rightarrow \lfloor C \rfloor & \end{array} $$

<caption>Fig. 3. Rules used to specify classical and intuitionistic logic. The superscript $a$ and $m$ on the names associated to $\mathcal{R}$-expressions identify that rule as either additive or multiplicative.</caption>

$$ \frac{\Gamma \vdash A \supset B \downarrow \quad \Gamma \vdash A \uparrow}{\Gamma \vdash B \downarrow} \quad (\supset E) \qquad \frac{\Gamma, A \vdash B \uparrow \quad \Gamma \vdash A \supset B \uparrow}{\Gamma \vdash A \supset B \uparrow} \quad (\supset I) \\ \frac{\Gamma \vdash A \wedge B \downarrow \quad \Gamma \vdash A \wedge B \downarrow}{\Gamma \vdash A \downarrow \quad \Gamma \vdash B \downarrow} \quad (\wedge E) \qquad \frac{\Gamma \vdash A \uparrow \quad \Gamma \vdash B \uparrow}{\Gamma \vdash A \wedge B \uparrow} \quad (\wedge I) \\ \frac{\Gamma \vdash A \uparrow \quad \Gamma \vdash A \downarrow}{\Gamma \vdash A \uparrow \quad \Gamma \vdash A \downarrow} \quad (\top I) \qquad \frac{\Gamma \vdash A \uparrow \quad \Gamma \vdash A \uparrow}{\Gamma \vdash A \downarrow \quad \Gamma \vdash A \downarrow} \quad (\bot I) \\ \frac{\Gamma \vdash A \uparrow \quad \Gamma \vdash A \downarrow}{\Gamma \vdash A \uparrow \quad \Gamma \vdash A \downarrow} \quad (\top E) \qquad \frac{\Gamma \vdash A \downarrow \quad \Gamma \vdash A \downarrow}{\Gamma \vdash C \uparrow \quad \Gamma \vdash C \uparrow} \quad (\bot E) $$

<caption>Fig. 4. The rules for the $\supset$, $\forall_i$, and $\wedge$ fragment of intuitionistic natural deduction NJ.</caption>

$$ \frac{\Gamma \vdash A \vee B \downarrow \quad \Gamma, A \vdash C \uparrow(\downarrow) \quad \Gamma, B \vdash C \uparrow(\downarrow)}{\Gamma \vdash C \uparrow(\downarrow)} \quad (\vee E) \\ \frac{\Gamma \vdash A_i \uparrow \quad \Gamma \vdash A_1 \vee A_2 \uparrow}{\Gamma \vdash A_1 \vee A_2 \uparrow} \quad (\top I) $$

<caption>Fig. 5. The rules for $\vee$ for intuitionistic natural deduction. In $[\vee L]$, $i \in \{1, 2\}$.</caption>

## C. Natural deduction for intuitionistic logic

If we set $\delta(\lfloor \cdot \rfloor) = +2$ and $\delta(\lceil \cdot \rceil) = -1$, then the synthetic rules derived in **F** for the rule expressions in Fig. 3 describe natural deduction proofs in intuitionistic logic. To prove this claim, we take the rules in Fig. 4 as the formal definition of natural deduction [7].

Let $\Gamma \cup \{C\}$ be a set of propositional formulas and assume that all $\delta(\lfloor \cdot \rfloor) = +2$ and $\delta(\lceil \cdot \rceil) = -1$. The two judgments in Fig. 4 will be encoded as follows. The up-arrow judgment $\Gamma \vdash C \uparrow$ is encoded using $\vdash \lfloor \Gamma \rfloor, \lfloor C \rfloor$. The down-arrow judgment $\Gamma \vdash C \downarrow$ is encoded using $\vdash \lfloor \Gamma \rfloor, \lceil C \rceil$.
<figure><img src="image_4.png" /><figcaption>Fig. 6. Some rewrite rules used to specify sequent calculus proofs in intuitionistic logic entirely in the linear realm.</figcaption></figure>

we change the bias assignment so that $\delta(\lfloor \cdot \rfloor) = -2$, then the rules in Fig. 3 encode a sequent calculus proof system (similar to Gentzen's **LK** proof system) which is complete for classical logic.

By using Propositions 5, 9, and 10, we can conclude immediately that if a formula has a natural deduction proof then it has a sequent calculus proof, since the only difference between these two encodings is the use of the debit rules.

It is worth noting that if $\delta(\cdot)$ is modified so that for some atomic expressions $A$, the value of $\delta(A)$ changes from $-1$ to $-2$, then proofs in **B** remain proofs. Thus, it is immediate that sequent provability in intuitionistic logic yields sequent provability in classical logic.

It is possible to encode the sequent calculus for both classical and intuitionistic logic at a more primitive level: that is, by using only the linear realm. In particular, consider the specification in Fig. 6. If $\delta(\lfloor \cdot \rfloor) = -1$ and $\delta(\lceil \cdot \rceil) = -1$, then these rules yield sequent calculus proofs for intuitionistic logic. Dropping the use of the classical realm affected this specification in two ways. First, we needed to add explicit weakening and contraction rules for left formula (the rules (LW) and (LC), respectively). Second, in encoding the implication-left rule and the cut rule, the occurrences of the right-side formula must be explicitly addressed in the rule's specification. In order to capture classical sequent calculus, we can modify the rules in Fig. 6 by replacing the left rule for implication and the $(Id_2)$ rule with the rules

<figure><img src="image_5.png" /></figure>

and by adding the following explicit rules for weakening and contraction for right tagged formulas.

$$ (RW) \quad [B] \mapsto \mathbf{1} \quad (RC) \quad [B] \mapsto [B] \times [B] $$

### E. Alternative encodings of proof rules

Fig. 7 contains alternative specifications of the introduction rules for some propositional logic constants. In particular,

<figure><img src="image_6.png" /><figcaption>Fig. 7. Some alternative version of inference rules.</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Fig. 8. Specification of the free deduction for classical logic.</figcaption></figure>

while Fig. 3 provides multiplicative rules for implication and additive rules for conjunction, disjunction, true, and false, in Fig. 7, we find additive rules for implication and multiplicative rules for conjunction, disjunction, true, and false. As is well known, the presence of the structural rules (of weakening and contraction) allows some pairing of these rules to be interadmissible.

If we switch from the additive rules for conjunction ($\wedge L^a$ and $\wedge R^a$ in Fig. 3) to the multiplicative rules ($\wedge L^m$ and $\wedge R^m$ in Fig. 7), then the conjunction elimination rule of intuitionistic natural deduction can be computed as follows.

$$ \frac{\frac{\vdash [A \wedge B], \Upsilon \quad \frac{\vdash [A] \times [B], \Delta, \Upsilon}{\vdash [A \wedge B] \vdash \Upsilon} \quad \text{debit}_2 \quad \frac{\vdash [A] \times [B], \Delta, \Upsilon}{\vdash [A] \vdash \Delta, \Upsilon} \quad \text{release}}{\vdash [A \wedge B] \mapsto [A] \times [B] \vdash \Delta, \Upsilon} $$

Since $\Delta$ could be either $\overline{[C]}$ or $\lceil [C] \rceil$ for some formula $C$, the left-introduction for conjunction can appear in either the $\downarrow$ or $\uparrow$ style judgments.

$$ \frac{\Gamma \vdash A \wedge B \downarrow \quad \Gamma, A, B \vdash C \uparrow (\downarrow)}{\Gamma \vdash C \uparrow (\downarrow)} $$

This natural deduction rule is an example of a generalized elimination rule [8], [9].

### F. Free deduction in classical logic

Given the interpretation of $(Id_1)$ and $(Id_2)$ as the $[M]$ and $[S]$ inference rules in natural deduction, it is tempting to consider both $[B]$ and $\overline{[B]}$ and both $[B]$ and $\overline{[B]}$ as equivalent in some sense. Such possible equivalences do not immediately apply to rules, however, since rule expressions do
<figure><img src="image_8.png" /><figcaption>Fig. 9. Several simple expressions provable from C.</figcaption></figure>

not contain debt expressions. It might be possible, however, to link proofs using a rule of the form $[A] \mapsto [B]$ with a proof using a rule of the form $\mathbf{1} \mapsto [A] \mapsto [B]$. We illustrate such considerations in this section.

The Free Deduction proof system [10] can be encoded as follows. Let $\mathcal{FD}$ be the set of rules that results from taking the rules in Fig. 8 along with $(Id_1)$ the following variant of $(Id_2)$:

$$ (Id_3) \quad \mathbf{1} \mapsto [C] \mapsto [C]. $$

Also, let $C$ be composed of the rules in Fig. 3. When using both of these sets of rules, we assume that $\delta(\cdot|\cdot) = \delta(\cdot|\cdot) = -2$. As we have seen, under this bias assignment, the rules in $C$ encode a classical sequent system. It is a simple exercise to show that all of the expressions in Fig. 9 are provable from $C$. Also, note the strong similarities between the rules in Fig. 8 and the expressions in Fig. 9: by dropping the $\mathbf{1} \mapsto$ prefix, changing the remaining occurrences of $\mapsto$ to $\times$, and flipping the left and right tags, we can convert rules in Fig. 8 to expressions in Fig. 9.

It is easy to show that every use of a rule in $\mathcal{FD}$ can be emulated by deciding on an expression in Fig. 9. For example, the synthetic rule that results from the first rule in Fig. 8 is

$$ \frac{\vdash [A \land B], \Delta_1 \vdash [A], \Delta_2 \vdash [B], \Delta_3 \quad \vdash \Delta_1, \Delta_2, \Delta_3}{\vdash [A \land B]} $$

This inference rule can be modeled in $\mathbf{B}$ by deciding on the first expression in Fig. 9 and using $(Id_1)$ three times (and with shifting the polarity to $\delta(\cdot|\cdot) = \delta(\cdot|\cdot) = +2$):

$$ \frac{\vdash [A \land B], \Delta_1 \vdash [A], \Delta_2 \vdash [B], \Delta_3 \quad \frac{[A \land B] \times [A] \times [B] \vdash \Delta_1, \Delta_2, \Delta_3}{\vdash \Delta_1, \Delta_2, \Delta_3}}{\vdash [A \land B]} $$

By using decide on the rule $(Id_3)$ on all three premises above, we can build a $\mathbf{B}$ derivation that flips the debt $\overline{A \land B}$ to the atomic expression $[A \land B]$ (as in the $[S]$ inference rule in Section V-C). It is now a simple matter to use the clip-elimination theorem to remove the intermediate lemmas listed in Fig. 9 for direct $\mathbf{B}$-proofs. Once we have such $\mathbf{B}$-proofs, Theorem 8 can provide an $\mathbf{F}$ proof corresponding to classical sequent calculus proof.

<figure><img src="image_9.png" /><figcaption>Fig. 10. Specification of linear logic.</figcaption></figure>

## G. Linear logic

Fig. 10 contains a specification for linear logic. This specification makes use of four tags: $[\cdot]$, $[\cdot]$, $[[\cdot]]$, and $[[\cdot]]$. Here, $[\cdot]$ and $[\cdot]$ construct atomic expressions that should be in the linear realm while $[[\cdot]]$ and $[[\cdot]]$ construct atomic expressions that should be in the classical realm. A sequent calculus for linear logic arises when we use the bias assignment $\delta(\cdot|\cdot) = \delta(\cdot|\cdot) = -1$ and $\delta(\cdot[[\cdot]]) = \delta(\cdot[[\cdot]]) = -2$.

## H. Quantification

Some of the earliest work on logic frameworks (for example, using $\lambda$Prolog [11] and the dependently typed LF [12], [13]) provided elegant approaches to the treatment of quantifiers in the specification of proof systems. The essence of these treatments of quantifiers is described via the notion of *binder mobility* [14], a concept we illustrate briefly here. We first extended the grammar of $E$ and $R$ formulas to allow both $Qx.(E x)$ and $Qx.(R x)$, where $Qx.$ is a binder for $x$ over expressions and rules. Next, we need to add to sequents a place for expression-level binders to move. To this end, we attach a variable-binding context $\Sigma$ to all sequents. Thus, sequents have the structure $\Sigma: \Gamma \vdash \Delta$ and $\Sigma: \vdash \Gamma \vdash \Delta$. In both of these cases, $\Sigma$ is a list of distinct variables, all with scope intended over the formulas in the respective sequent. We assume the usual notions of $\alpha, \beta$, and $\eta$ conversion. The following two rules can be added to $\mathbf{B}$ to treat quantifiers.

$$ \frac{\Sigma, x : \Gamma \vdash E x, \Delta}{\Sigma : \Gamma \vdash Q x.E x, \Delta} \qquad \frac{\Sigma : \Gamma, R t \vdash \Delta}{\Sigma : \Gamma, Q x.R x \vdash \Delta} \quad t \text{ is a } \Sigma\text{-term} $$
In the first rule, we assume that $x$ is not already bound by $\Sigma$. In that rule, the expression-level binder for $x$ in the conclusion is moved to a sequent-level binder for $x$ in the premise. The proviso in the second inference rule means that the free variables of the (first-order) term $t$ are all taken from $\Sigma$.

Finally, to illustrate how quantifiers can be used to specify rules, we first explicitly quantify over schema variables in the specification of rules. For example, the rule ($\supset L^m$) in Fig. 3 should be written more explicitly as

$$Q A.Q B. [A \supset B] \mapsto [A] \mapsto [B]$$

Adding universal and existential quantification to the intuitionistic and classical logic of Section V-B can be done using the (closed) R-expressions

$$ \begin{align*} Q B.Q t. & \quad [\forall x.Bx] \mapsto [Bt] \\ Q B. & \quad [\forall x.Bx] \mapsto Q x.[Bx] \\ Q B. & \quad [\exists x.Bx] \mapsto Q x.[Bx] \\ Q B.Q t. & \quad [\exists x.Bx] \mapsto [Bt] \end{align*} $$

## VI. RELATED WORK

The two-phase proof system **F** resembles *uniform proofs*, which were used to describe logic programming as the search for proofs in a two-phase proof system that alternated between a *goal-reduction* phase and a *backchaining* phase [15]. Andreoli's focused proof system [16] for Girard's linear logic [2] also inspired design aspects of **PSF**. The closest related work, however, is the following collection of papers that have used linear logic as a logical framework for specifying proof systems. The author showed how a version of linear logic based on only the negative connectives could be used to specify Gentzen-style sequent calculus and natural deduction proof systems [17]. Nigam, Pimentel, and others significantly extended such specifications, especially once subexponentials were added to linear logic [18], [19], [20], [6], [21], [22], [23]. Implementations and formal results surrounding such linear logic specifications have also been built [24], [25]. A design goal for **PSF** was to use it to replace linear logic as the meta-logic while attempting to find the fewest features of linear logic that made it successful for specifying proof systems.

## VII. CONCLUSION

The state of the search for proofs in classical and intuitionistic logic can be viewed as a collection of sheets of paper, each containing assumptions and a conclusion: such sheets denote a gap in the proof to be completed. An inference rule is encoded in reverse as a rule for rewriting a sheet into 0 or more other sheets. **PSF** starts with this simple perspective of inference and formalizes inference as the rewriting of collections of multisets of tagged formulas. In doing so, the multiplicative and additive structures behind logical inference are treated as primitive. This framework also uses a bias assignment for tagged formulas that captures the notions of linear and classical realm and of debt. We have also illustrated how **PSF** specifications of inference rules can be used to represent a range of known proof systems modularly. We demonstrated this modularity by showing that one set of rewrite rules can

account for sequent calculus and natural deduction proofs in classical and intuitionistic logic.

## REFERENCES

[1] G. Gentzen, "Investigations into logical deduction," in *The Collected Papers of Gerhard Gentzen*, M. E. Szabo, Ed. North-Holland, 1935, pp. 68-131.

[2] J.-Y. Girard, "Linear logic," *Theoretical Computer Science*, vol. 50, no. 1, pp. 1-102, 1987.

[3] K. Chaudhuri, F. Pfenning, and G. Price, "A logical characterization of forward and backward chaining in the inverse method," *J. of Automated Reasoning*, vol. 40, no. 2-3, pp. 133-177, 2008.

[4] D. Miller and J.-H. Wu, "A positive perspective on term representations," in *31st EACSL Annual Conference on Computer Science Logic (CSL 2023)*, B. Klin and E. Pimentel, Eds., LIPIcs 252, 2023, pp. 3:1-3:21.

[5] C. Liang and D. Miller, "A focused approach to combining logics," *Annals of Pure and Applied Logic*, vol. 162, no. 9, pp. 679-697, 2011.

[6] V. Nigam and D. Miller, "A framework for proof systems," *J. of Automated Reasoning*, vol. 45, no. 2, pp. 157-188, 2010. [Online]. Available: http://springerlink.com/content/m12014474287n423/

[7] W. Sieg and J. Byrnes, "Normal natural deduction proofs (in classical logic)," *Studia Logica*, vol. 60, no. 1, pp. 67-106, 1998.

[8] P. Schroeder-Heister, "A natural extension of natural deduction," *Journal of Symbolic Logic*, vol. 49, no. 4, pp. 1284-1300, 1984.

[9] J. von Plato, "Natural deduction with general elimination rules," *Archive for Mathematical Logic*, vol. 40, no. 7, pp. 541-567, 2001.

[10] M. Parigot, "Free deduction: An analysis of "computations" in classical logic," in *Proceedings of the First Russian Conference on Logic Programming*, ser. LNAI, no. 592. Springer, 1992, pp. 361-380.

[11] A. Felty and D. Miller, "Specifying theorem provers in a higher-order logic programming language," in *Ninth International Conference on Automated Deduction*, E. Lusk and R. Overbeck, Eds., LNCS 310. Argonne, IL: Springer, May 1988, pp. 61-80.

[12] R. Harper, F. Honsell, and G. Plotkin, "A framework for defining logics," *Journal of the ACM*, vol. 40, no. 1, pp. 143-184, 1993.

[13] A. Felty and D. Miller, "Encoding a dependent-type $\lambda$-calculus in a logic programming language," in *Proc. of the 1990 Conference on Automated Deduction*, M. Stickel, Ed., LNAI 449, Springer, 1990, pp. 221-235.

[14] D. Miller, "Mechanized metatheory revisited," *Journal of Automated Reasoning*, vol. 63, no. 3, pp. 625-665, Oct. 2019.

[15] D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, "Uniform proofs as a foundation for logic programming," *Annals of Pure and Applied Logic*, vol. 51, no. 1-2, pp. 125-157, 1991.

[16] J.-M. Andreoli, "Logic programming with focusing proofs in linear logic," *J. of Logic and Computation*, vol. 2, no. 3, pp. 297-347, 1992.

[17] D. Miller, "Forum: A multiple-conclusion specification logic," *Theoretical Computer Science*, vol. 165, no. 1, pp. 201-232, 1996.

[18] E. G. Pimentel, "Lógica linear e a especificação de sistemas computacionais," Ph.D. dissertation, Universidade Federal de Minas Gerais, Belo Horizonte, M.G., Brasil, Dec. 2001, written in English.

[19] V. Nigam, "Exploiting non-canonicity in the sequent calculus," Ph.D. dissertation, Ecole Polytechnique, Sep. 2009. [Online]. Available: http://www.nigam.info/thesis/Vivek_Nigam_phd.pdf

[20] V. Nigam and D. Miller, "Algorithmic specifications in linear logic with subexponentials," in *ACM SIGPLAN Conference on Principles and Practice of Derivative Programming (PPDP)*, A. Porto and F. J. López-Fraguas, Eds. ACM, 2009, pp. 129-140.

[21] V. Nigam, E. Pimentel, and G. Reis, "Specifying proof systems in linear logic with subexponentials," in *Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop (LSFA 2010)*, ser. ENTCS, vol. 269. Elsevier, 2011, pp. 109-123.

[22] D. Miller and E. Pimentel, "A formal framework for specifying sequent calculus proof systems," *Theoretical Computer Science*, vol. 474, pp. 98-116, 2013. [Online]. Available: http://hal.inria.fr/hal-00787586

[23] V. Nigam, E. Pimentel, and G. Reis, "An extended framework for specifying and reasoning about proof systems," *J. of Logic and Computation*, 2014.

[24] G. Reis and V. Nigam, "TATU: Online system for reasoning about sequent calculus specifications in linear logic with subexponentials," http://www logic.at/people/giselle/tatu/, Mar. 2010.

[25] C. Olarte, E. Pimentel, and C. Rocha, "A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems," *Journal of Logical and Algebraic Methods in Programming*, vol. 130, 2023.