# Combinatorial Proofs and Decomposition Theorems for First-order Logic

Dominic J D Hughes, Lutz Strassburger, Jui-Hsuan Wu

► To cite this version:

Dominic J D Hughes, Lutz Strassburger, Jui-Hsuan Wu. Combinatorial Proofs and Decomposition Theorems for First-order Logic. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-13, 10.1109/LICS52264.2021.9470579 . hal-03369764

HAL Id: hal-03369764

https://inria.hal.science/hal-03369764

Submitted on 7 Oct 2021

**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
This is where combinatorial proofs come in. They were introduced by Hughes [9] for classical propositional logic as a syntax-free notion of proof, and as a potential solution to Hilbert's 24th problem [10] (see also [11]). The basic idea is to abstract away from the syntax of the inference rules used in inductively-generated proofs and consider the proof as a combinatorial object, more precisely as a special kind of graph homomorphism. For example, a propositional combinatorial proof of Peirce's law ((p⇒q)⇒p)⇒p = ((p ∨ q) ∧ p) ∨ p is shown mid-left in Fig. 1, a homomorphism from a 4-vertex graph with two colours (above) to a 4-vertex graph labelled with propositional variables (below); dotted vertical lines define the homomorphism, from above to below.

Several authors have illustrated how syntactic proofs in various proof systems can be translated to propositional combinatorial proofs: for sequent proofs in [10], for deep inference proofs in [12], for Frege systems in [13], and for tableaux systems and resolution in [14]. This enables a natural definition of proof identity for propositional logic: two proofs are the same if they are mapped to the same combinatorial proof. For example, the left side of Fig. 1 translates syntactic proofs from sequent calculus and the calculus of structures into the same combinatorial proofs, witnessing that the two syntactic proofs, from different systems, are the same.

Recently, Acclavio and Straßburger extended this notion to relevant logics [15] and to modal logics [16], and Heijltjes, Hughes and Straßburger have provided combinatorial proofs for intuitionistic propositional logic [17].

In this paper we advance the idea that combinatorial proofs can provide a notion of proof identity for first-order logic. First-order combinatorial proofs were introduced by Hughes in [18]. For example, a first-order combinatorial proof of Smullyan's drinker paradox ∃x px ⇒ ∀y py) = ∃x.($\overline{p}$x ∨ (∀y.py)) is shown on the right of Fig. 1, a homomorphism from a 5-vertex partially coloured graph (with one colour) to a 4-vertex labelled graph. However, even though Hughes proves soundness and completeness, the proof is unsatisfactory: (1) the soundness argument is long, intricate and cumbersome, and (2) the completeness proof does not allow a syntactic proof to be read back from a combinatorial proof, i.e., completeness is not sequentializable [19] nor full [20]. A fundamental problem is that not all combinatorial proofs can be obtained as translations of sequent calculus proofs.

We solve these issues by moving to a deep inference system. More precisely, we introduce a new proof system, KS1, for first-order logic, that (a) reflects every combinatorial proof, i.e., there is a surjection from KS1 proofs to combinatorial proofs, (b) yields simpler proofs of soundness and completeness for combinatorial proofs, and (c) admits new decomposition theorems establishing a precise correspondence between certain syntactic inference rules and certain combinatorial notions. The right of Fig. 1 illustrates surjection in (a), and since the syntactic proofs in the two systems translate to the same combinatorial proof, they can be considered the same.

In general, a decomposition theorem provides normal forms of proofs, separating subsets of inference rules of a proof

system. A prominent example of a decomposition theorem is Herbrand's theorem [21], which allows a separation between the propositional part and the quantifier part in a first-order proof [4], [22]. Through the advent of deep inference, new kinds of proof decompositions became possible, most notably the separation between the linear part of a proof and the resource management of a proof. It has been shown by Straßburger [23] that a proof in classical propositional logic can be decomposed into a proof of multiplicative linear logic, followed by a proof consisting only of contractions and weakenings (see also [10, §4]). In this paper we show that the same is possible for first-order logic.

Combinatorial proofs and deep inference can be seen as opposite ends of a spectrum: whereas deep inference allows for a very fine granularity of inference rules—one inference rule in a standard formalism, like sequent calculus or semantic tableaux, is usually simulated by a sequence of different deep inference rules—combinatorial proofs have completely abolished the concept of inference rule. And yet, there is a close relationship between the two, realized through a decomposition theorem, as we establish in this paper.

**Outline:** This paper has three parts. First, in Sections II–V we present the preliminaries on first-order logic, first-order graphs, first-order combinatorial proofs, and the first-order proof system KS1. Second, in Section VI we state the main results. And third, in Sections VII–X we give their proofs.

## II. PRELIMINARIES: FIRST-ORDER LOGIC

### A. Terms and Formulas

Fix pairwise disjoint countably infinite sets $VAR = \{x, y, z, ...\}$ of variables, $FUN = \{f, g, ...\}$ of function symbols, and $PRED = \{p, q, ...\}$ of predicate symbols. Each function symbol and each predicate symbol has a finite arity. Each predicate symbol $p$ has a **dual** $\overline{p}$ with $\overline{p} \neq p$. The grammars below generate the set **TERM** of **terms**, denoted by $s, t, u, ...$, the set **ATOM** of **atoms**, denoted by $a, b, c, ...$, and the set **FORM** of **formulas**, denoted by $A, B, C, ...$:

$$t ::= x \mid f(t_1, \dots, t_n)$$

$$a ::= t \mid f \mid p(t_1, \dots, t_n) \mid \overline{p}(t_1, \dots, t_n)$$

$$A ::= a \mid A \land A \mid A \lor A \mid \exists x.A \mid \forall x.A$$

where the arity of $f$ and $p$ is $n$. For better readability we often omit parentheses and write $ft_1...t_n$ or $pt_1...t_n$. We consider the truth constants $t$ (true) and $f$ (false) as additional atoms, and consider all formulas in negation normal form, where **negation** ($\neg$) is defined on atoms and formulas via De Morgan's laws:

$$\overline{t} = f$$

$$\overline{f} = t$$

$$\exists x. \overline{A} = \forall x. \overline{A}$$

$$\forall x. \overline{A} = \exists x. \overline{A}$$

$$\overline{p}(t_1, \dots, t_n) = \overline{p}(t_1, \dots, t_n)$$

$$\overline{p}(t_1, \dots, t_n) = p(t_1, \dots, t_n)$$

$$\overline{A} \land \overline{B} = \overline{A} \lor \overline{B}$$

$$\overline{A} \lor \overline{B} = \overline{A} \land \overline{B}$$

Note $\overline{a} = a$. We write $A \Rightarrow B$ as an abbreviation for $\overline{A} \lor B$.
A formula is **rectified** if all bound variables are distinct from one another and from all free variables. Every formula can be transformed into a logically equivalent rectified form by bound variable renaming, e.g. $(px \lor \exists xqx) \land \exists xr \mapsto (px \lor \exists yqy) \land \exists zrz$. If we consider formulas equivalent modulo bound variable renaming (α-conversion), the rectified form of a formula A is unique, and we denote it by $\hat{A}$.

A **substitution** is a function $\sigma: \text{VAR} \to \text{TERM}$ that is the identity almost everywhere. We denote substitutions as $\sigma = [x_1/t_1, \dots, x_n/t_n]$, where $\sigma(x_i) = t_i$ for $i = 1..n$ and $\sigma(x) = x$ for all $x \notin \{x_1, \dots, x_n\}$. Write $A\sigma$ for the formula obtained from A by applying $\sigma$, i.e., by simultaneously replacing all occurrences of $x_i$ by $t_i$. A **variable renaming** is a substitution $\rho$ with $\rho(x) \in \text{VAR}$ for all variables $x$.

## B. Sequent Calculus LK1

Sequents, denoted by $\Gamma, \Delta, \dots$, are finite multisets of formulas, written as lists, separated by comma. The corresponding formula of a (non-empty) sequent $\Gamma = A_1, A_2, \dots, A_n$ is the disjunction of its formulas: $\bigvee(\Gamma) = A_1 \vee A_2 \vee \dots \vee A_n$. A sequent is **rectified** iff its corresponding formula is.

In this paper we use the sequent calculus LK1, shown in Figure 2, which is a one-sided variant of Gentzen's original calculus [3] for first-order logic. To simplify some technicalities later in this paper, we include the mix rule.

**Theorem 1.** LK1 is sound and complete for first-order logic.

For a proof, see any standard textbook, e.g. [24].

The linear fragment of LK1, i.e., the fragment without the rules ctr (contraction) and wk (weakening) defines first-order multiplicative linear logic [19], [25] with mix [26], [27] (MLL1+mix). We denote that system here with MLL1<sup>X</sup> (shown in Figure 2 in the dashed box).

We will use the cut elimination theorem. The **cut** rule is

$$ \text{cut} \quad \frac{\vdash \Gamma, A \quad \vdash \bar{A}, \Delta}{\vdash \Gamma, \Delta} \qquad (1) $$

**Theorem 2.** If a sequent $\vdash \Gamma$ is provable in LK1+cut then it is also provable in LK1. Furthermore, if $\vdash \Gamma$ is provable in MLL1<sup>X</sup>+cut then it is also provable in MLL1<sup>X</sup>.

As before, this is standard, see e.g. [24] for a proof.

# III. PRELIMINARIES: FIRST-ORDER GRAPHS

## A. Graphs

A **graph** $\mathcal{G} = \langle V_{\mathcal{G}}, E_{\mathcal{G}} \rangle$ is a pair where $V_{\mathcal{G}}$ is a finite set of vertices and $E_{\mathcal{G}}$ is a finite set of edges, which are two-element subsets of $V_{\mathcal{G}}$. We write $vw$ for an edge $\{v, w\}$.

Let $\mathcal{G} = \langle V_{\mathcal{G}}, E_{\mathcal{G}} \rangle$ and $\mathcal{H} = \langle V_{\mathcal{H}}, E_{\mathcal{H}} \rangle$ be graphs such that $V_{\mathcal{G}} \cap V_{\mathcal{H}} = \emptyset$. A **homomorphism** $\varphi: \mathcal{G} \to \mathcal{H}$ is a function $\varphi: V_{\mathcal{G}} \to V_{\mathcal{H}}$ such that if $vw \in E_{\mathcal{G}}$ then $\varphi(v)\varphi(w) \in E_{\mathcal{H}}$. The **union** $\mathcal{G} + \mathcal{H}$ is the graph $\langle V_{\mathcal{G}} \cup V_{\mathcal{H}}, E_{\mathcal{G}} \cup E_{\mathcal{H}} \rangle$ and the **join** $\mathcal{G} \times \mathcal{H}$ is the graph $\langle V_{\mathcal{G}} \cup V_{\mathcal{H}}, E_{\mathcal{G}} \cup E_{\mathcal{H}} \cup \{vw \mid v \in V_{\mathcal{G}}, w \in V_{\mathcal{H}}\} \rangle$. A graph $\mathcal{G}$ is **disconnected** if $\mathcal{G} = \mathcal{G}_1 + \mathcal{G}_2$ for two non-empty graphs $\mathcal{G}_1, \mathcal{G}_2$, otherwise it is **connected**.

A graph $\mathcal{G}$ is **labelled** in a set $L$ if each vertex $v \in V_{\mathcal{G}}$ has an associated **label** $\ell(v) \in L$. A graph $\mathcal{G}$ is (partially

<figure><img src="image_2.png" /><figcaption>Fig. 2. Sequent calculi LK1 (all rules) and MLL1<sup>X</sup> (rules in the dashed box)</figcaption></figure>

coloured if it carries a partial equivalence relation $\sim_G$ on $V_{\mathcal{G}}$; each equivalence class is a **colour**.<fnref n="1" /> A **vertex renaming** of $\mathcal{G} = \langle V_{\mathcal{G}}, E_{\mathcal{G}} \rangle$ along a bijection $\langle \cdot \rangle: V_{\mathcal{G}} \to \hat{V}_{\mathcal{G}}$ is the graph $\hat{\mathcal{G}} = \langle \hat{V}_{\mathcal{G}}, \{\hat{v}\hat{w} \mid vw \in E_{\mathcal{G}}\} \rangle$, with colouring and/or labelling inherited (i.e., $\hat{v} \sim \hat{w}$ if $v \sim w$, and $\ell(\hat{v}) = \ell(v)$). Following standard graph theory, we identify graphs modulo vertex renaming.

A **directed graph** $\mathcal{G} = \langle V_{\mathcal{G}}, E_{\mathcal{G}} \rangle$ is a set $V_{\mathcal{G}}$ of **vertices** and a set $E_{\mathcal{G}} \subseteq V_{\mathcal{G}} \times V_{\mathcal{G}}$ of **direct edges**. A **directed graph homomorphism** $\varphi: \langle V_{\mathcal{G}}, E_{\mathcal{G}} \rangle \to \langle V_{\mathcal{H}}, E_{\mathcal{H}} \rangle$ is a function $\varphi: V_{\mathcal{G}} \to V_{\mathcal{H}}$ such that if $(v, w) \in E_{\mathcal{G}}$ then $(\varphi(v), \varphi(w)) \in E_{\mathcal{H}}$.

## B. Cographs

A graph $\mathcal{H} = \langle V_{\mathcal{H}}, E_{\mathcal{H}} \rangle$ is a **subgraph** of a graph $\mathcal{G} = \langle V_{\mathcal{G}}, E_{\mathcal{G}} \rangle$ if $V_{\mathcal{H}} \subseteq V_{\mathcal{G}}$ and $E_{\mathcal{H}} \subseteq E_{\mathcal{G}}$. It is **induced** if $v, w \in V_{\mathcal{H}}$ and $vw \in E_{\mathcal{G}}$ implies $vw \in E_{\mathcal{H}}$. An induced subgraph of $\mathcal{G} = \langle V_{\mathcal{G}}, E_{\mathcal{G}} \rangle$ is uniquely determined by its set of vertices $V$ and we denote it by $\mathcal{G}[V]$. A graph is **$\mathcal{H}$-free** if it does not contain $\mathcal{H}$ as an induced subgraph. The graph $\mathbf{P}_4$ is the (undirected) graph $\langle \{v_1, v_2, v_3, v_4\}, \{v_1v_2, v_2v_3, v_3v_4\} \rangle$. A **cograph** is a $\mathbf{P}_4$-free undirected graph. The interest in cographs for our paper comes from the following well-known fact.

**Theorem 3** ([28], [29]). A graph is a cograph iff it can be constructed from the singletons via the operations $+$ and $\times$.

In a graph $\mathcal{G}$, the **neighbourhood** $N(v)$ of a vertex $v \in V_{\mathcal{G}}$ is $\{w \mid vw \in E_{\mathcal{G}}\}$. A **module** is a set $M \subseteq V_{\mathcal{G}}$ with $N(v) \setminus M = N(w) \setminus M$ for all $v, w \in M$. A module $M$ is **strong** if for every module $M'$ we have $M' \subseteq M, M \subseteq M'$ or $M \cap M' = \emptyset$. A module is **proper** if it has two or more vertices.

## C. Fographs

A cograph is **logical** if every vertex is labelled by either an atom or variable, and it has at least one atom-labelled vertex. An atom-labelled vertex is a **literal** and a variable-labelled vertex is a **binder**. A binder labelled with $x$ is an **$x$-binder**. The **scope** of a binder $b$ is the smallest proper strong module

<footnote n="1">¹In [9] and [18] adjacent vertices must have distinct colours, following the standard definition of colouring in graph theory. We choose to omit this condition here, as it is implied by the preclusion of bimatchings in Def. 10.</footnote>
containing b. An **x-literal** is a literal whose atom contains the variable x. An **x-binder** binds every x-literal in its scope. In a logical cograph G, a binder b is **existential** (resp. **universal**) if, for every other vertex v in its scope, we have $bv \in E_G$ (resp. $bv \notin E_G$). An **x-binder** is **legal** if its scope contains no other x-binder and at least one literal.

**Definition 4** ([18, §3]). A first-order graph or fograph G is a logical cograph whose binders are all legal. The binding graph of G is the directed graph $\tilde{G} = \langle V_G, \{(b, l) \mid b \text{ binds } l\} \rangle$.

We define a mapping $[\cdot]$ from formulas to (labelled) graphs, inductively as follows:

$$[a] = \bullet a \quad (\text{for any atom } a)$$

$$[A \lor B] = [A] + [B] \qquad [\exists x.A] = \bullet x \times [A]$$

$$[A \land B] = [A] \times [B] \qquad [\forall x.A] = \bullet x + [A]$$

where we write $\bullet \alpha$ for a single-vertex labelled by $\alpha$.

**Example 5.** Here is the fograph of the drinker formula $\exists x (px \Rightarrow \forall y py) = \exists x. (\bar{p}x \lor (\forall y.py))$:

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

**Lemma 6.** If A is a rectified formula then $[A]$ is a fograph.

*Proof.* That $[A]$ is a logical cograph follows immediately from the definition and Theorem 3. The fact that every binder of $[A]$ is legal can be proved by structural induction on A. $\square$

**Remark 7.** Note that $[A]$ need not be a fograph if A is not rectified. If $A = (\forall x.px) \lor (\forall x.qx)$, then $[A] = \bullet x \bullet px \bullet x \bullet qx$, the scope of each x-binder contains all the vertices, in particular, the other x-binder. On the other hand, there are non-rectified formulas which are translated to fographs by $[\cdot]$. For example, in the graph of $(\exists x.px) \lor (\exists x.qx)$, both x-binders are legal, as they are not in each other's scope: $x \bullet \bullet px \bullet x \bullet \bullet qx$.

We define a congruence relation $\equiv$ on formulas, called **equiv-alence**, by the following equations:

$$ \begin{array}{l@{\qquad}l} A \land B \equiv B \land A & (A \land B) \land C \equiv A \land (B \land C) \\ A \lor B \equiv B \lor A & (A \lor B) \lor C \equiv A \lor (B \lor C) \\ \forall x. \forall y. A \equiv \forall y. \forall x. A & \forall x. (A \lor B) \equiv (\forall x. A) \lor B \\ \exists x. \exists y. A \equiv \exists y. \exists x. A & \exists x. (A \land B) \equiv (\exists x. A) \land B \end{array} \qquad (2) $$

where x must not be free in B in the last two equations.

**Theorem 8** ([18, §10]). Let A, B be rectified formulas. Then

$$A \equiv B \iff [A] = [B]$$

*Proof.* A straightforward structural induction on formulas. $\square$

**Example 9.** $\exists x. (\bar{p}x \lor (\forall y.py)) \equiv \exists x \forall y (py \lor \bar{p}x)$, and both formulas have the same (rectified) fograph D, below-left.

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

Above-center we show the cotree of the underlying cograph (illustrating the idea behind Theorem 3) and above-right is its binding graph $\vec{D}$.

<figure><img src="image_5.png" /><figcaption>Fig. 3. A fonet (left) with dualizer $[x/z, y/fz]$ and its leap graph (right).</figcaption></figure>

# IV. FIRST-ORDER COMBINATORIAL PROOFS

## A. Fonets

Two atoms are **pre-dual** if they are not t or f, and their predicate symbols are dual (e.g. $p(x, y)$ and $\bar{p}(y, z)$) and two literals are **pre-dual** if their labels (atoms) are pre-dual. A **linked fograph** $\langle C, \sim_C \rangle$ is a coloured fograph C such that every colour (i.e., equivalence class of $\sim_C$), called a **link**, consists of two pre-dual literals, and every literal is either t-labelled or in a link. Hence, in a linked fograph no vertex is labelled f.

Let C be a linked fograph. The set of links can be seen as a unification problem by identifying dual predicate symbols. A **dualizer** of C is a substitution $\delta$ unifying all the links of C. Since a first-order unification problem is either unsolvable or has a most general unifier, we can define the notion of **most general dualizer**. A **dependency** is a pair $\{\bullet x, \bullet y\}$ of an existential binder $\bullet x$ and a universal binder $\bullet y$ such that the most general dualizer assigns to x a term containing y. A **leap** is either a link or a dependency. The **leap graph** $C^L$ of C is the undirected graph $\langle V_C, L_C \rangle$ where $L_C$ is the set of leaps of C. A vertex set $W \subseteq V_C$ induces a **matching** in C if $W \neq \emptyset$ and for all $w \in W$, $N(w) \cap W$ is a singleton. We say that W induces a **bimatching** in C if it induces a matching in C and a matching in $C^L$.

**Definition 10** ([18, §5]). A first-order net or fonet is a linked fograph which has a dualizer but no induced bimatching.

Figure 3 shows a fonet with its dualizer and leap graph.

## B. Skew Bifibrations

A graph homomorphism $\varphi: \langle V_G, E_G \rangle \to \langle V_H, E_H \rangle$ is a **fibration** [30], [31] if for all $v \in V_G$ and $w\varphi(v) \in E_H$, there exists a unique $\tilde{w} \in V_G$ such that $\tilde{w}v \in E_G$ and $\varphi(\tilde{w}) = w$ (indicated below-left), and is a **skew fibration** [9, §3] if for all $v \in V_G$ and $w\varphi(v) \in E_H$ there exists $\tilde{w} \in V_G$ such that $\tilde{w}v \in E_G$ and $\varphi(\tilde{w})w \notin E_H$ (indicated below-centre). A directed graph homomorphism is a **fibration** if for all $v \in V_G$ and $(w, \varphi(v)) \in E_H$, there exists a unique $\tilde{w} \in V_G$ such that $(\tilde{w}, v) \in E_G$ and $\varphi(\tilde{w}) = w$ (indicated below-right).

<figure><img src="image_6.png" /></figure>
<figure><img src="image_7.png" /><figcaption>Fig. 4. Four combinatorial proofs, each shown above the formula proved. Here $x$ and $y$ are variables, $f$ is a unary function symbol, $a$ and $b$ are constants (nullary function symbols), $p$ is a unary predicate symbol, and $q$ is a binary predicate symbol. For each skew bifibration $\varphi$, the variable substitution $\rho_\varphi$ is an identity, thus we can omit labels from each (coloured) source fograph (since the label of $v$ in the source is that of $\varphi(v)$ in the target).</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>Fig. 5. Condensed forms of the four combinatorial proofs in Figure 4. We do not show the lower graph, and indicate the mapping by the position of the vertices of the upper graph.</figcaption></figure>

A **fograph homomorphism** $\varphi = \langle\varphi, \rho_{\varphi}\rangle$ is a pair where $\varphi: G \to \mathcal{H}$ is a graph homomorphism between the underlying graphs, and $\rho_{\varphi}$, also called the **substitution induced by** $\varphi$, is a variable renaming such that for all $v \in V_G$ we have $\ell(\varphi(v)) = \rho_{\varphi}(\ell(v))$, and $\rho_{\varphi}$ is the identity on variables not in $G$. Note that $\varphi$ necessarily maps binders to binders and literals to literals. Since $\rho_{\varphi}$ is fully determined by $\varphi$ alone, we often leave $\rho_{\varphi}$ implicit. A fograph homomorphism $\varphi: G \to \mathcal{H}$ **preserves existentials** if for all existential binders $b$ in $G$, the binder $\varphi(b)$ is existential in $\mathcal{H}$.

**Definition 11** ([18, §4]). Let $G$ and $\mathcal{H}$ be fographs. A skew bifibration $\varphi: G \to \mathcal{H}$ is an existential-preserving fograph homomorphism that is a skew fibration on $\langle V_G, E_G \rangle \to \langle V_{\mathcal{H}}, E_{\mathcal{H}} \rangle$ and a fibration on the binding graphs $\tilde{G} \to \tilde{\mathcal{H}}$.

**Example 12.** Below-left is a skew bifibration, whose binding fibration is below-centre. When the labels on the source fograph can be inferred (modulo renaming), we often omit the labelling in the upper graph, as below-right.

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

**Definition 13** ([18, §6]). A first-order combinatorial proof (FOCP) of a fograph $G$ is a skew bifibration $\varphi: C \to G$ where $C$ is a fonet. A first-order combinatorial proof of a formula $A$ is a combinatorial proof of its graph $[[A]]$.

Figure 4 shows examples of FOCPs (taken from [18]), each above the formula it proves. The same FOCPs are in Figure 5 in condensed form, with the formula graph left implicit.

**Theorem 14** ([18, §6]). FOCPs are sound and complete for first-order logic.

**Remark 15.** Our definition of FOCP is slightly more lax

$$ \forall \frac{S\{t\}}{S\{\forall x.t\}} \quad \text{ai} \quad \frac{S\{t\}}{S\{a \lor \bar{a}\}} \quad \text{t} \quad \frac{S\{A\}}{S\{A \land t\}} $$

$$ s \frac{S\{A \land (B \lor C)\}}{S\{(A \land B) \lor C\}} \quad \text{mix} \quad \frac{S\{A \land B\}}{S\{A \lor B\}} $$

$$ \exists \frac{S\{A[x/t]\}}{S\{\exists x.A\}} \quad \equiv \quad \frac{S\{B\}}{S\{A\}} \quad (\text{where } A \equiv B) $$

$$ w \frac{S\{A\}}{S\{A \lor B\}} \quad m \frac{S\{(A \land C) \lor (B \land D)\}}{S\{(A \lor B) \land (C \lor D)\}} \quad ac \frac{S\{a \lor a\}}{S\{a\}} $$

$$ m\forall \frac{S\{(\forall x.A) \lor (\forall x.B)\}}{S\{\forall x.(A \lor B)\}} \quad m\exists \quad \frac{S\{(\exists x.A) \lor (\exists x.B)\}}{S\{\exists x.(A \lor B)\}} $$

$$ w\forall \frac{S\{A\}}{S\{\forall x.A\}} \quad (x \text{ not free in } A) \quad c\forall \frac{S\{\forall x.\forall x.A\}}{S\{\forall x.A\}} $$

<caption>Fig. 6. Deep inference systems KS1 (all rules) and MLS1$^X$ (rules in the dashed box)</caption>

than the original definition of [18], as we allow for a variable renaming $\rho_{\varphi}$ which was restricted to be the identity in [18].

## V. FIRST-ORDER DEEP INFERENCE SYSTEM KS1

In contrast to standard proof formalisms, like sequent calculi or tableaux, where inference rules decompose the principal formula along its root connective, deep inference rules apply like rewriting rules inside any (positive) formula or sequent context, which is denoted by $S\{\cdot\}$, and which is a formula (resp. sequent) with exactly one occurrence of the hole $\{\cdot\}$ in the position of an atom. Then $S\{A\}$ is the result of replacing the hole $\{\cdot\}$ in $S\{\cdot\}$ with $A$.

Figure 6 shows the inference rules for the deep inference system KS1 introduced in this paper. It is a variation of the systems presented by Brünnler [32] and Ralph [33] in their
PhD-theses. The main differences are (i) the explicit presence of the mix-rule, (ii) a different choice of how the formula equivalence $≡$ is defined, (iii) an explicit rule for the equivalence, and (iv) new inference rules $w_∀$ and $c_∀$. The reason behind these design choices is to obtain the correspondence with combinatorial proofs and the full completeness result.

We consider here only the cut-free fragment, as cut-elimination for deep inference systems has already been discussed elsewhere (e.g. [22], [34]).<fnref n="2" /> As with the sequent system LK1, we also need for KS1 the linear fragment, MLS1<sup>X</sup>, and that is shown in Figure 6 in the dashed box.

$B$

We write $s \parallel \Phi$ to denote a derivation $\Phi$ from $B$ to $A$ using the rules from system S. A formula $A$ is **provable** in a system S if there is a derivation in S from $t$ to $A$.

We will for some results also employ the general (non-atomic) version of the contraction rule:

$$c \frac{S\{A \lor A\}}{S\{A\}} \qquad (3)$$

## VI. MAIN RESULTS

We state the main results of this paper here, and prove them in later sections. The first is routine and expected, but must be proved nonetheless:

**Theorem 16.** KS1 is sound and complete for first-order logic.

Our second result is more surprising, as it is a very strong decomposition result for first-order logic.

**Theorem 17.** For every derivation $\kappa_{S1} \parallel \Phi$ there are $f$-free formulas $A_1, \dots, A_5$ and a derivation

$$ \begin{array}{l} t \\ \{\forall,ai,t\} \parallel A_5 \\ \{s,mix,\equiv\} \parallel A_4 \\ \{\exists\} \parallel A_3 \\ \{m,m_\forall,m_\exists,\equiv\} \parallel A_2 \\ \{ac,c_\forall\} \parallel A_1 \\ \{w,w_\forall,\equiv\} \parallel A \end{array} $$

This theorem is stronger than the existing decompositions for first-order logic, which either separate only atomic contraction and atomic weakening [32] or only contraction [33] or only the quantifiers in form of a Herbrand theorem [35], [33].

$$ \begin{align*} & \frac{\forall \frac{t}{\forall y.t} \qquad \frac{t}{\forall y.(t \land t)} \qquad \frac{\forall y.((\bar{p}y \lor py) \land t)}{\forall y.((\bar{p}y \lor py) \land t)}}{\text{ai}} \\ & \equiv \frac{\forall y.((\bar{p}y \lor py) \land (py \lor \bar{p}fy))}{\forall y.((\bar{p}y \lor (py \land (py \lor \bar{p}fy))) \land (py \lor \bar{p}fy))} \\ & \equiv \frac{\forall y.((\bar{p}y \lor \bar{p}fy) \lor (py \land pfy))}{\exists \frac{\forall y.((\bar{p}y \lor (\exists x.\bar{p}x)) \lor (py \land pfy))}{\forall y.((((\exists x.\bar{p}x) \lor (\exists x.\bar{p}x)) \lor (py \land pfy)) \land (\exists x.\bar{p}x) \lor (\exists y.(py \land pfy)))}} \\ & \equiv \frac{((\exists x.\bar{p}x) \lor (\exists x.\bar{p}x)) \lor (\forall y.(py \land pfy))}{m_\exists \frac{(\exists x.((\bar{p}x \lor \bar{p}x) \lor (\forall y.(py \land pfy)))}{ac \frac{(\exists x.((\bar{p}x \lor \bar{p}x) \lor (\forall y.(py \land pfy)))}{(\exists x.\bar{p}x) \lor (\forall y.(py \land pfy))}} \end{align*} $$

<caption>Fig. 7. Example derivation in decomposed form of Theorem 17</caption>

Theorem 17 is also the reason why we have the rules $w_∀$ and $c_∀$ in system KS1, as these rules are derivable with the other rules. However, they are needed to obtain this decomposition. Figure 7 shows an example of a decomposed derivation in KS1 of the formula $(\exists x.\bar{p}x) \lor (\forall y.(py \land pfy))$.

A weaker version of Theorem 17 will also be useful:

**Theorem 18.** For every derivation $\kappa_{S1} \parallel \Phi$ there is a formula $A'$ with no occurrence of $f$ and a derivation

$$ \begin{array}{l} t \\ \text{MLS1}^x \parallel A' \\ \{w,c,\equiv\} \parallel A \end{array} $$

Here $A'$ corresponds to $A_3$ of Theorem 17.

We now establish the connection between derivations in KS1 and combinatorial proofs.

**Theorem 19.** Let $\varphi: C \to A$ be a combinatorial proof and let $A$ be a formula with $A = [[A]]$. Then there is a derivation

$$ \begin{array}{l} t \\ \text{MLS1}^x \parallel \Phi_1 \\ A' \\ \{w,w_\forall,ac,c_\forall,m,m_\forall,m_\exists,\equiv\} \parallel \Phi_2 \\ A \end{array} \qquad (4) $$

for some $A' \equiv C\rho_\varphi$ where $C$ is a formula with $[[C]] = C$ and $\rho_\varphi$ is the variable renaming substitution induced by $\varphi$. Conversely, whenever we have a derivation as in (4) above, such that $f$ does not occur in $A'$, then there is a combinatorial proof $\varphi: C \to [[A]]$ such that $C = [[A']]}$.

Furthermore, in the proof of Theorem 19, we will see that (i) the links in the fonet $C$ correspond precisely to the pairs of atoms that meet in the instances of the $ai$-rule in the derivation $\Phi_1$, and (ii) the "flow-graph" of $\Phi_2$ that traces the quantifier-

<footnote n="2">²In the deep inference literature, the cut-free fragment is also called the down-fragment. But as we do not discuss the up-fragment here, we omit the down-arrows $\downarrow$ in the rule names.</footnote>
and atom-occurrences in the derivation corresponds exactly to the vertex-mapping induced by $\varphi$. To give an example, consider the derivation in Figure 7 which corresponds to the left-most combinatorial proof in Figures 4 and 5.

Thus, combinatorial proofs are closely related to derivations of the form (4), and since by Theorem 17 every derivation can be transformed into that form, we can say that combinatorial proofs provide a canonical proof representation for first-order logic, similarly to what proof nets are for linear logic [36].

Finally, Theorems 16, 17 and 19 imply Theorem 14, which means that we have here an alternative proof of the soundness and completeness for first-order combinatorial proofs which is simpler than the one given in [18], and improves with completeness being full (a surjection from syntactic KS1 proofs onto combinatorial proofs).

## VII. TRANSLATING BETWEEN LK1 AND KS1

We prove Theorems 16, 17, and 18, mainly by translating derivations to and from the sequent calculus, and by rule permutation arguments.

### A. The Linear Fragments MLL1$^x$ and MLS1$^x$

We show that MLL1$^x$ and MLS1$^x$ are equivalent.

**Lemma 20.** If $\vdash \Gamma$ is provable in MLL1$^x$ then $\forall(\Gamma)$ is provable in MLS1$^x$.

*Proof.* This is a straightforward induction on the proof of $\vdash \Gamma$ in MLL1$^x$, making a case analysis on the bottommost rule instance. We show here only the case of $\forall \frac{\vdash \Delta, A}{\vdash \Delta, \forall x.A}$ (all other cases are simpler or have been shown before, e.g. [32]): By induction hypothesis, there is a proof of $\forall(\Delta) \lor A$ in MLS1$^x$. We can prefix every line in that proof by $\forall x$ and then compose the following derivation:

$$ \begin{array}{rcl} & \forall \frac{t}{\forall x.t} & \\ \multicolumn{2}{l}{\mathrm{MLS1}^x} & \\ & \equiv \frac{\forall x. \forall(\Delta) \lor A}{\forall(\Delta) \lor \forall x.A} & \end{array} $$

where we can apply the $\equiv$-rule because $x$ is not free in $\Delta$. $\square$

**Lemma 21.** Let $\frac{S\{A\}}{S\{B\}}$ be an inference rule in MLS1$^x$. Then the sequent $\vdash \bar{A}, B$ is provable in MLL1$^x$.

*Proof.* A routine exercise. $\square$

**Lemma 22.** Let $A, B$ be formulas, and let $S\{\cdot\}$ be a (positive) context. If $\vdash \bar{A}, B$ is provable in MLL1$^x$, then so is $\vdash \overline{S\{A\}}, S\{B\}$.

*Proof.* A straightforward induction on $S\{\cdot\}$. (see e.g. [37]) $\square$

**Lemma 23.** If a formula $C$ is provable in MLS1$^x$ then $\vdash C$ is provable in MLL1$^x$.

*Proof.* We proceed by induction on the number of inference steps in the proof of $C$ in MLS1$^x$. Consider the bottommost

rule instance $\frac{S\{A\}}{S\{B\}}$. By induction hypothesis we have a MLL1$^x$ proof $\Pi$ of $\vdash S\{A\}$. By Lemmas 21 and 22, we have a MLL1$^x$ proof of $\vdash \overline{S\{A\}}, S\{B\}$. We can compose them via

$$ \text{cut} \frac{\vdash S\{A\} \quad \vdash \overline{S\{A\}}, S\{B\}}{\vdash S\{B\}} $$

and then apply Theorem 2. $\square$

### B. Contraction and Weakening

The first observation here is that Lemmas 20–23 from above also hold for LK1 and KS1. We therefore immediately have:

**Theorem 24.** For every sequent $\Gamma$, we have that $\vdash \Gamma$ is provable in LK1 if and only if $\forall(\Gamma)$ is provable in KS1.

Then Theorem 16 is an immediate consequence. Let us now proceed with providing further lemmas that will be needed for the other results.

**Lemma 25.** The c-rule is derivable in $\{ac, m, m_\forall, m_\exists, \equiv\}$.

*Proof.* This can be shown by a straightforward induction on $A$ (for details, see e.g. [32]). $\square$

**Lemma 26.** $w_\forall, c_\forall, m, m_\forall, m_\exists$ are derivable in $\{w, c, \equiv\}$.

*Proof.* We only show the cases for $w_\forall$ and $c_\forall$ (for the others see [32]):

$$ \begin{align} & \frac{A}{w} \equiv \frac{A \lor (\forall x.A)}{\forall x.(A \lor A)} \equiv \frac{\forall x.\forall x.A}{c} \tag{5} \\ & \frac{\forall x.((\forall x.A) \lor A)}{c} \equiv \frac{(\forall x.A) \lor (\forall x.A)}{\forall x.A} \end{align} $$

where in the first derivation, $x$ is not free in $A$, and in the second one not free in $\forall x.A$. $\square$

**Lemma 27.** Let $A$ and $B$ be formulas. Then

$$ \frac{A}{\{w,c,\equiv\}} \iff \frac{A}{\{w,w_\forall,ac,c_\forall,m,m_\forall,m_\exists,\equiv\}} \frac{A}{B} $$

*Proof.* Immediately from Lemmas 25 and 26. $\square$

**Remark 28.** Observe that Lemma 27 would also hold with the rules $w_\forall$ and $c_\forall$ removed.

### C. Rule Permutations

**Theorem 29.** Let $\Gamma$ be a sequent. If $\vdash \Gamma$ is provable in LK1 (as depicted on the left below) then there is a sequent $\Gamma'$ not containing any $f$, such that there is a derivation as shown on the right below:

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

*Proof.* First, we can replace every instance of the $f$-rule in $\Phi$ by $wk$. Then the instances of $wk$ and $ctr$ are replaced by
w and c, which can then be permuted down. Details are in Appendix A. □

**Lemma 30.** For every derivation $\text{MLS1}^x \parallel_A$ there are formulas $t$

A' and A'' such that

$$ \begin{array}{l} t \\ \{\forall,ai,t\} \parallel_A A'' \\ \{s,mix,\equiv\} \parallel_A A' \\ \{\exists\} \parallel_A A \end{array} $$

*Proof.* First, observe that the $∃$ rule can be permuted under all the other rules since $A[x/t]$ has the same structure as A and none of the other rules has a premise of the form $S\{∃x.A\}$. It suffices now to prove that all rules in $\{\forall, ai, t\}$ can be permuted over the rules in $\{s, mix, \equiv\}$, which is straightforward. For s, mix, and the $\equiv$-instances that do not involve the quantifiers, the details can be found in [38]. The $\equiv$-instances concerning the quantifiers are admissible if the $∃$-rule is not present. □

**Lemma 31.** For every derivation $\{w,w_\forall,ac,c_\forall,m,m_\forall,m_\exists,\equiv\} \parallel_B$

there are formulas $A'$ and $B'$ such that

$$ \begin{array}{l} A \\ \{m,m_\forall,m_\exists,\equiv\} \parallel_{A'} \\ \{ac,c_\forall\} \parallel_{B'} \\ \{w,w_\forall,\equiv\} \parallel_B \end{array} $$

*Proof.* Permute all w and $w_\forall$ instances to the bottom of the derivation, then permute all c and $c_\forall$ below $\{m, m_\forall, m_\exists\}$. This involves a tedious but routine case analysis. However, unlike most other rule permutations in this paper, this has not been done before in the deep inference literature. For this reason, we give the full case analysis in Appendix B. This Lemma is the reason for the presence of the rules $w_\forall$ and $c_\forall$, as without them the permutation cases in (5) could not be resolved. □

We can now complete the proof of Theorems 17 and 18.

*Proof of Theorem 18.* Assume we have a proof of A in KS1. By Theorem 24 we have a proof of $\vdash A$ in LK1 to which we can apply Theorem 29. Finally, we apply Lemma 20 to get the desired shape. □

*Proof of Theorem 17.* Assume we have a proof of A in KS1. We first apply Theorem 18, and then Lemma 30 to the upper half and Lemmas 27 and 31 to the lower half. □

### A. From MLL1<sup>X</sup> Proofs to Fonets

Let $\Pi$ be a MLL1<sup>X</sup> proof of a rectified sequent $\vdash \Gamma$ not containing $f$. We now show how $\Pi$ is translated into a linked fograph $[[\Pi]] = \langle [[\Gamma]], \sim_{\Pi} \rangle$. We proceed inductively, making a case analysis on the last rule in $\Pi$. At the same time we are constructing a dualizer $\delta_{\Pi}$, so that in the end we can conclude that $[[\Pi]]$ is in fact a fonet.

1) $\Pi$ is $ax \frac{\vdash a, \bar{a}}{\vdash a}$ : Then the only link is $\{a, \bar{a}\}$, and $\delta_{\Pi}$ is empty.

2) $\Pi$ is $t \frac{\vdash t}{\vdash t}$ : Then $\sim_{\Pi}$ and $\delta_{\Pi}$ are both empty.

3) The last rule in $\Pi$ is $mix \frac{\vdash \Gamma', \Gamma''}{\vdash \Gamma', \Gamma''}$ : By induction hypothesis, we have proofs $\Pi'$ and $\Pi''$ of $\Gamma'$ and $\Gamma''$, respectively. We have $[[\Gamma]] = [[\Gamma']'] + [[\Gamma'']]$ and we can let $\sim_{\Pi} = \sim_{\Pi'} \cup \sim_{\Pi''}$ and $\delta_{\Pi} = \delta_{\Pi'} \cup \delta_{\Pi''}$.

4) The last rule in $\Pi$ is $\vee \frac{\vdash \Gamma_1, A, B}{\vdash \Gamma_1, A \vee B}$ : By induction hypothesis, there is a proof $\Pi'$ of $\Gamma' = \Gamma_1, A, B$. We have $[[\Gamma]] = [[\Gamma']]$ and let $\sim_{\Pi} = \sim_{\Pi'}$ and $\delta_{\Pi} = \delta_{\Pi'}$.

5) The last rule in $\Pi$ is $\wedge \frac{\vdash \Gamma_1, A \quad \vdash B, \Gamma_2}{\vdash \Gamma_1, A \wedge B, \Gamma_2}$ : By induction hypothesis, we have proofs $\Pi'$ and $\Pi''$ of $\Gamma' = \Gamma_1, A$ and $\Gamma'' = B, \Gamma_2$, respectively. We have $[[\Gamma]] = [[\Gamma_1]] + ([[A]] \times [[B]]) + [[\Gamma_2]]$ and we let $\sim_{\Pi} = \sim_{\Pi'} \cup \sim_{\Pi''}$ and $\delta_{\Pi} = \delta_{\Pi'} \cup \delta_{\Pi''}$.

6) The last rule in $\Pi$ is $\exists \frac{\vdash \Gamma_1, A[x/t]}{\vdash \Gamma_1, \exists x.A}$ : By induction hypothesis, there is a proof $\Pi'$ of $\Gamma' = \Gamma_1, A[x/t]$. For each atom in $\Gamma' = \Gamma_1, A[x/t]$, there is a corresponding atom in $\Gamma = \Gamma_1, \exists x.A$. We can therefore define the linking $\sim_{\Pi}$ from the linking $\sim_{\Pi'}$ via this correspondence. Then, we let $\delta_{\Pi}$ be $\delta_{\Pi'} + [x/t]$. Since $\Gamma$ is rectified $x$ does not yet occur in $\delta_{\Pi'}$. Hence $\delta_{\Pi}$ is a dualizer of $[[\Pi]]$.

7) The last rule in $\Pi$ is $\forall \frac{\vdash \Gamma_1, A}{\vdash \Gamma_1, \forall x.A}$ ($x$ not free in $\Gamma_1$) : By induction hypothesis, there is a proof $\Pi'$ of $\Gamma' = \Gamma_1, A$, which has the same atoms as in $\Gamma = \Gamma_1, \forall x.A$. Hence, we can let $\sim_{\Pi} = \sim_{\Pi'}$ and $\delta_{\Pi} = \delta_{\Pi'}$.

**Theorem 32.** If $\Pi$ is a MLL1<sup>X</sup> proof of a rectified f-free sequent $\vdash \Gamma$, then $[[\Pi]]$ is a fonet and $\delta_{\Pi}$ a dualizer for it.

*Proof.* We must show that none of the operations above introduces a bimatching. For cases 1–6, this is immediate. For case 7, observe that there is a potential dependency from each existential binder in $[[\Gamma']]$ to the new $x$-binder $\bullet x$ in $[[\Gamma]]$. However, observe that this $\bullet x$ vertex is not connected to any vertex in $[[\Gamma']]$, and hence no such new dependency can be extended to a bimatching. That $\delta_{\Pi}$ is a dualizer for $[[\Pi]]$ follows immediately from the construction. Hence, $[[\Pi]]$ is a fonet. □
## B. From MLS1<sup>X</sup> Proofs to Fonets

There is a more direct path from a MLL1<sup>X</sup> proof Π of a rectified sequent Γ to the linked fograph [[Π]]: take the fograph [[Γ]], and let the equivalence classes of ~Π be all the atom pairs that meet in an instance of ax, and δ<sub>Π</sub> comprises the substitutions at the ∃-rules in Π. We chose the more cumbersome path above because it gives us a direct proof of Theorem 32. However, for translating MLS1<sup>X</sup> derivation into fonets, we employ exactly that direct path.

In a derivation in MLS1<sup>X</sup> where the conclusion is rectified, every line is also rectified, as the only rules involving bound variables are ∀ and ∃ which (upwards) both remove a binder. Therefore, we can call such a derivation rectified, and for a non-rectified MLS1<sup>X</sup> derivation Φ we can define its rectification Φ̂ inductively, by rectifying each line, proceeding step-wise from conclusion to premise.<fnref n="3" />

A rectified derivation MLS1<sup>X</sup> ‖Φ determines a substitution
A
t

which maps the existential bound variables occurring in A to the terms substituted for them in the instances of the ∃-rule in Φ. We denote this substitution by δ<sub>Φ</sub> and call it the **dualizer** of Φ. Furthermore, every atom occurring in the conclusion A must be consumed by a unique instance of the rule ai in Φ. This allows us to define a (partial) equivalence relation ~<sub>Φ</sub> on the atom occurrences in A by a ~<sub>Φ</sub> b if a and b are consumed by the same instance of ai in Φ. We call ~<sub>Φ</sub> the **linking** of Φ, and define [[Φ]] = ⟨[A], ~<sub>Φ</sub>⟩.

t
Theorem 33. Let MLS1<sup>X</sup> ‖<sub>A</sub> Φ be a rectified derivation where A
is f-free. Then [[Φ]] is a fonet and δ<sub>Φ</sub> a dualizer for it.

To prove this theorem, we have to show that no inference
rule in MLS1<sup>X</sup> can introduce a bimatching. To simplify the
argument, we introduce the **frame** [39] of the linked fograph
C, which is a linked (propositional) cograph in which the
dependencies between the binders in C are encoded as links.

More formally, let C be a formula with [[C]] = C, to which
we exhaustively apply the following subformula rewriting
steps, to obtain a sequent C*:

1) **Encode dependencies as fresh links.** For each dependency {•xᵢ, •yⱼ} in C, with corresponding subformulas ∃xᵢ.A and ∀yⱼ.B in C, we pick a fresh (nullary) predicate symbol qᵢ,ⱼ, and then replace ∃xᵢ.A by qᵢ,ⱼ ∧ ∃xᵢ.A, and replace ∀yⱼ.B by qᵢ,ⱼ ∨ ∀yⱼ.B.

2) **Erase quantifiers.** After step 1, remove all the quantifiers, i.e., replace ∃xᵢ.A by A and replace ∀yⱼ.B by B everywhere.

3) **Simplify atoms.** After step 2, replace every predicate pt₁...tₙ (resp. p̄t₁...tₙ) with a nullary predicate symbol p (resp. p̄)

Then ~C\* consists of the pairs induced by ~C and the new
pairs {qᵢ,ⱼ, q̄ᵢ,ⱼ} introduced in step 1 above. We call C\* the
frame of C and we define the frame of C, denoted C\*, as
⟨[C\*], ~C\*⟩.

**Lemma 34.** If a linked fograph C has an induced bimatching then so does its frame C\*.

*Proof.* Immediately from the construction of the frame. □

*Proof of Theorem 33.* From Φ we construct a derivation Φ\* of A\* in the propositional fragment of MLS1\*, such that [[Φ\*]] = [[Φ]\*]. The rules ai, t, mix and s are translated trivially, and for ≡, it suffices to observe that the frame construction is invariant under ≡. Finally, for the rules ∀ and ∃, proceed as follows. Every instance of ∀ is replaced by the derivation on the right below:<fnref n="4" />

$$
\forall \frac{S\{t\}}{S\{\forall y_j.t\}} \rightsquigarrow S\{(q_{h_1,j} \lor \bar{q}_{h_1,j}) \land \dots \land (q_{h_n,j} \lor \bar{q}_{h_n,j}) \land t\} \\
\phantom{\forall \frac{S\{t\}}{S\{\forall y_j.t\}} \rightsquigarrow} \quad \{s, \equiv\} \parallel \Psi_2 \\
\phantom{\forall \frac{S\{t\}}{S\{\forall y_j.t\}} \rightsquigarrow} S\{q_{h_1,j} \lor \dots \lor q_{h_n,j} \lor (\bar{q}_{h_1,j} \land \dots \land \bar{q}_{h_n,j} \land t)\}
$$

where h₁, ..., hₙ range over the indices of the existential binders dependent on that yⱼ. It is easy to see how Ψ₁ is constructed. The construction of Ψ₂, using s and ≡, is standard, see, e.g. [40], [37], [41], [38]. Then, every occurrence of ∀yⱼ.F is replaced by qₕ₁,ⱼ ∨ ... ∨qₕₙ,ⱼ ∨ (qₕ₁,ⱼ ∧ ... ∧qₕₙ,ⱼ ∧ F) in the derivation below that ∀-instance. Now, observe that all instances of the ∃-rule introducing xᵢ dependent on yⱼ must occur below in the derivation (otherwise Φ would not be rectified). Now consider such an instance ∃ S{B[xᵢ/t]} / S{∃xᵢ.B}.

Its context S{·} must contain all the ∀yⱼ the ∃xᵢ depends on,
such that B is in their scope. Following the translation of the
∀ rules above, we can therefore translate the ∃-rule instance
by the following derivation

$$
\begin{align*}
S_0\{\bar{q}_{i,k_1} \wedge S_1\{\bar{q}_{i,k_2} \wedge \dots \wedge S_{l-1}\{\bar{q}_{i,k_l} \wedge S_l\{B'\}\} \dots \}} \\
\phantom{S_0\{\bar{q}_{i,k_1} \wedge S_1\{\bar{q}_{i,k_2} \wedge \dots \wedge S_{l-1}\{\bar{q}_{i,k_l} \wedge S_l\{B'\}\} \dots \}} \\
\{s, \equiv\} \parallel \Psi_3 \\
S_0\{S_1\{\dots \wedge S_{l-1}\{S_l\{\bar{q}_{i,k_1} \wedge \bar{q}_{i,k_2} \wedge \dots \wedge q_{i,k_l} \wedge B'\}\} \dots \}}
\end{align*}
$$

where k₁, ..., kₗ are the indices of the universal binders on
which that xᵢ depends, and B' is B in which all predicates
are replaced by a nullary one (step 3 in the frame construction).
The derivation Ψ₃ can be constructed in the same way as Ψ₂.

Doing this to all instances of the rules ∀ and ∃ in Φ
yields indeed a propositional derivation Φ\* with [[Φ\*]] = [[Φ]\*].
It has been shown by Retoré [42] and rediscovered by
Straßburger [38] that [[Φ\*]] = ⟨[C\*], ~Φ\*⟩ cannot contain an
induced bimatching. By Lemma 34, [[Φ]] does not have an
induced bimatching either. Furthermore, it follows from the
definition of δ<sub>Φ</sub> that it is a dualizer for [[Φ]].
□

**Remark 35.** There is an alternative path of proving Theorem 33 by translating Φ to an MLL1<sup>X</sup>-proof Π, observing that this process preserves the linking and the dualizer. However,

<footnote n="3">³As for formulas, the rectification of a derivation is unique up to renaming of bound variables.</footnote>

<footnote n="4">⁴For better readability we omit superfluous parentheses, knowing that we always have ≡ incorporating associativity and commutativity of ∧ and ∨.</footnote>
for this, we have to extend the construction from the previous
subsection to the cut-rule, and then show that linking and du-
alizer of a sequent proof Π are invariant under cut elimination.
This can be done similarly to unification nets in [39].

C. *From Fonets to MLL1<sup>X</sup> Proofs*

Now we are going to show how from a given fonet $\langle C, \sim_C \rangle$
we can construct a sequent proof Π in MLL1<sup>X</sup> such that $\llbracket \Pi \rrbracket =
\langle C, \sim_C \rangle$. In the proof net literature, this operation is also called
sequentialization. The basic idea behind our sequentialization
is to use the frame of C, to which we can apply the splitting
tensor theorem, and then reconstruct the sequent proof Π.

Let $\Gamma$ be a propositional sequent and $\sim_\Gamma$ be a linking for $\llbracket \Gamma \rrbracket$. A conjunction formula $A \wedge B$ is *splitting* or a *splitting tensor* if $\Gamma = \Gamma', A \wedge B, \Gamma''$ and $\sim_\Gamma = \sim_1 \cup \sim_2$, such that $\sim_1$ is a linking for $\llbracket \Gamma', A \rrbracket$ and $\sim_2$ is a linking for $\llbracket B, \Gamma'' \rrbracket$, i.e., removing the $\wedge$ from $A \wedge B$ splits the linked fograph $\langle\llbracket \Gamma \rrbracket, \sim_\Gamma \rangle$ into two fographs. We say that $\langle\llbracket \Gamma \rrbracket, \sim_\Gamma \rangle$ is *mixed* iff $\Gamma = \Gamma', \Gamma''$ and $\sim_\Gamma = \sim_1 \cup \sim_2$, such that $\sim_1$ is a linking for $\llbracket \Gamma' \rrbracket$ and $\sim_2$ is a linking for $\llbracket \Gamma'' \rrbracket$. Finally, $\langle\llbracket \Gamma \rrbracket, \sim_\Gamma \rangle$ is *splittable* if it is mixed or has a splitting tensor.

**Theorem 36.** Let $\Gamma$ be a free propositional sequent containing only atoms and $\wedge$-formulas, and $\sim_\Gamma$ be a linking for $\llbracket \Gamma \rrbracket$. If $\langle\llbracket \Gamma \rrbracket, \sim_\Gamma \rangle$ does not induce a bimatching then it is splittable.

This is the well-known splitting-tensor-theorem [19], [43],
adapted for the presence of mix. In the setting of linked
cographs, it has first been proved by Retoré [44], [45] and
then rediscovered by Hughes [9]. We use it now for our
sequentialization:

**Theorem 37.** Let $\langle C, \sim_C \rangle$ be a fonet, and let $\Gamma$ be a sequent with $\llbracket \Gamma \rrbracket = C$. Then there is an MLL1$^x$-proof $\Pi$ of $\Gamma$, such that $\llbracket \Pi \rrbracket = \langle C, \sim_C \rangle$.

Proof. Let $\delta_C$ be the dualizer of $\langle C, \sim_C \rangle$. We proceed by induction on the size of $\Gamma$ (i.e., the number of symbols in it, without counting the commas). If $\Gamma$ contains a formula with $\vee$-root, or a formula $\forall x.A$, we can immediately apply the $\vee$-rule or the $\forall$-rule of MLL1$^x$ and proceed by induction hypothesis. If $\Gamma$ contains a formula $\exists x.A$ such that the corresponding binder $\bullet x$ in $C$ has no dependency, then we can apply the $\exists$-rule, choosing the term $t$ as determined by $\delta_C$, and proceed by induction hypothesis. Hence, we can now assume that $\Gamma$ contains only atoms, $\wedge$-formulas, or formulas of shape $\exists x.A$, where the vertex $\bullet x$ has dependencies. Then the frame $\langle\llbracket \Gamma^* \rrbracket, \sim_\Gamma \rangle$ does not induce a bimatching and contains only atoms and $\wedge$-formulas, and is therefore splittable. If it is mixed, then we can apply the mix-rule to $\Gamma$ and apply the induction hypothesis to the two components. If it is not mixed then there must be a splitting tensor. If the splitting $\wedge$ is already in $\Gamma$, then we can apply the $\wedge$-rule and proceed by induction hypothesis on the two branches. However, if $\Gamma^*$ is not mixed and all splitting tensors are $\wedge$-formulas introduced in step 1 of the frame construction, then we get a contradiction as in that case there must be a $\vee$- or $\forall$-formula in $\Gamma$. □

D. *From Fonets to MLS1<sup>X</sup> Proofs*

We can now straightforwardly obtain the same result for
MLS1<sup>X</sup>:

**Theorem 38.** Let $\langle C, \sim_C \rangle$ be a fonet, and let $C$ be a formula with $\llbracket C \rrbracket = C$. Then there is a derivation $\mathbf{MLS1}^x \parallel \Phi$ such that $\llbracket \Phi \rrbracket = \langle C, \sim_C \rangle$.

*Proof.* We apply Theorem 37 to obtain a sequent proof Π of $\vdash C$ with $\llbracket \Pi \rrbracket = \langle C, \sim_C \rangle$. Then we apply Lemma 20, observing that the translation from MLL1$^x$ to MLS1$^x$ preserves linking and dualizer. □

**Remark 39.** Note that it is also possible to do a direct “sequentialization” into the deep inference system MLS1$^x$, using the techniques presented in [38] and [46].

IX. SKEW BIFIBRATIONS AND RESOURCE MANAGEMENT

In this section we establish the relation between skew
bifibrations and derivations in {$w, w_\vee, ac, c_\vee, m, m_\vee, m_\exists, \equiv$}.
However, if a derivation $\Phi$ contains instances of the rules $c_\vee$,
$m_\vee$, and $m_\exists$ we can no longer naively define the rectification
$\hat{\Phi}$ as in the previous section for MLS1$^x$, as these two rules
cannot be applied if premise and conclusion are rectified. For
this reason we define here rectified versions $\hat{c}_\vee$, $\hat{m}_\vee$ and $\hat{m}_\exists$,
shown below:

$$
\begin{align*}
& \hat{c}_{\vee} \frac{S\{\forall y.\forall x.Ax\}}{S\{\forall x.Ax\}} && \hat{m}_{\vee} \frac{S\{(\forall y.Ay) \lor (\forall z.Bz)\}}{S\{\forall x.(Ax \lor Bx)\}} \\
& \hat{m}_{\exists} \frac{S\{(\exists y.Ay) \lor (\exists z.Bz)\}}{S\{\exists x.(Ax \lor Bx)\}} && \hat{m}_{\exists} \frac{S\{(\exists y.Ay) \lor (\exists z.Bz)\}}{S\{\exists x.(Ax \lor Bx)\}}
\end{align*}
$$

Here, we use the notation $A \cdot$ for a formula $A$ with occurrences
of a placeholder $\cdot$ for a variable. Then $Ax$ stands for the results
of replacing that placeholder with $x$, and also indicating that
$x$ must not occur in $A \cdot$. Then $\forall x.Ax$ and $\forall y.Ay$ are the same
formula modulo renaming of the bound variable bound by the
outermost $\forall$-quantifier. We also demand that the variables $x$,
$y$, and $z$ do not occur in the context $S\{\cdot}$.

Note that in an instance of $\widehat{m}_{\vee}$ or $\widehat{m}_{\exists}$ (as shown above), we can have $x = y$ or $x = z$, but not both if the premise is rectified. If $x = y$ and $x = z$ we have $m_{\vee}$ and $m_{\exists}$ as special cases of $\widehat{m}_{\vee}$ and $\widehat{m}_{\exists}$, respectively. And similarly, if $x = y$ then $c_{\vee}$ is a special case of $\widehat{c}_{\vee}$.

For a derivation $\Phi$ in $\{w, w_\vee, ac, c_\vee, m, m_\vee, m_\exists, \equiv\}$, we can
now construct the **rectification** $\hat{\Phi}$ by rectifying each line of $\Phi$,
yielding a derivation in $\{w, w_\vee, ac, c_\vee, m, m_\vee, m_\exists, \equiv\}$.

For each instance $r \frac{Q}{P}$ of an inference rule in
$\{w, w_\vee, ac, c_\vee, m, m_\vee, m_\exists, \equiv\}$ we can define the **induced**
**map** $[r] : V_{\llbracket Q \rrbracket} \to V_{\llbracket P \rrbracket}$ which acts as the identity for
$r \in \{m, \equiv\}$ and as the canonical injection for $r \in \{w, w_\vee\}$.
For $r = ac$ it maps the vertices corresponding to the two
atoms in the premise to the vertex of the contracted atom
in the conclusion, and for $r \in \{c_\vee, m_\vee, m_\exists\}$ it maps the two
vertices corresponding to the quantifiers in the premise to the one in the conclusion (and acts as the identity on all other vertices). For a derivation $\Phi$ in $\{w, w_\vee, ac, \hat{c}_\vee, m, \hat{m}_\vee, \hat{m}_\vee, \equiv\}$ we can then define the **induced map** $\lfloor\Phi\rfloor$ as the composition of the induced maps of the rule instances in $\Phi$.

**Lemma 40.** Let $\{w, w_\vee, ac, c_\vee, m, m_\vee, m_\vee, \equiv\} \parallel \Phi$ be given. Then there is a rectified derivation $\{w, w_\vee, ac, \hat{c}_\vee, m, \hat{m}_\vee, \hat{m}_\vee, \equiv\} \parallel \hat{\Phi}$, such that the induced maps $\lfloor\Phi\rfloor: \lfloor A\rfloor \to \lfloor B\rfloor$ and $\lfloor\hat{\Phi}\rfloor: \lfloor \hat{A}\rfloor \to \lfloor \hat{B}\rfloor$ are equal up to a variable renaming of the vertex labels.

*Proof.* Immediate from the definition. □

### A. From Contraction and Weakening to Skew Bifibrations

**Lemma 41.** Let $\{w, w_\vee, ac, \hat{c}_\vee, m, \hat{m}_\vee, \hat{m}_\vee, \equiv\} \parallel \Phi$ be a rectified derivation. Then the induced map $\lfloor\Phi\rfloor: \lfloor A\rfloor \to \lfloor B\rfloor$ is a skew bifibration.

Before we show the proof of this lemma, we introduce another useful concept: the **propositional encoding** $A^\circ$ of a formula $A$, which is a propositional formula with the property that $\lfloor A^\circ \rfloor = \lfloor A \rfloor$. For this, we introduce new propositional variables that have the same names as the (first-order) variables $x \in \text{VAR}$. Then $A^\circ$ is defined inductively by:

$$ 
\begin{array}{l@{\qquad}l}
a^\circ = a & (\forall x A)^\circ = x \lor A^\circ \\
(A \lor B)^\circ = A^\circ \lor B^\circ & (\exists x A)^\circ = x \land A^\circ \\
(A \land B)^\circ = A^\circ \land B^\circ &
\end{array}
$$

**Lemma 42.** For every formula $A$, we have $\lfloor A^\circ \rfloor = \lfloor A \rfloor$.

*Proof.* A straightforward induction on $A$. □

We use $\equiv^\circ$ to denote the restriction of $\equiv$ to propositional formulas, i.e., the first two lines in (2).

*Proof of Lemma 41.* First, observe that for every inference rule $r \in \{w, w_\vee, ac, \hat{c}_\vee, m, \hat{m}_\vee, \hat{m}_\vee, \equiv\}$ the induced map $\lfloor r \rfloor: V_{\lfloor Q \rfloor} \to V_{\lfloor P \rfloor}$ defines an existential-preserving graph homomorphism $\lfloor Q \rfloor \to \lfloor P \rfloor$ and a fibration on the corresponding binding graphs. Therefore, their composition $\lfloor \Phi \rfloor$ has the same properties of fibration.

For showing that it is also a skew fibration, we construct for $\Phi$ its propositional encoding $\Phi^\circ$ by translating every line into its propositional encoding. The instances of the rules $\hat{m}_\vee$ and $\hat{m}_\vee$ are replaced by:

$$ \equiv \frac{S\{(y \lor (Ay)^\circ) \lor (z \lor (Bz)^\circ)\}}{\hat{a}\hat{c}} \frac{S\{(y \land (Ay)^\circ) \lor (z \land (Bz)^\circ)\}}{\hat{a}\hat{c}} \frac{S\{(y \lor z) \lor ((Ay)^\circ \lor (Bz)^\circ)\}}{\hat{a}\hat{c}} \frac{S\{(y \lor z) \land ((Ay)^\circ \lor (Bz)^\circ)\}}{\hat{a}\hat{c}} \frac{S\{x \lor ((Ax)^\circ \lor (Bx)^\circ)\}}{\hat{a}\hat{c}} $$

respectively, where $\hat{a}\hat{c}$ is a ac that renames the variables—the propositional variable, as well as the first-order variable of the same name—as everything is rectified, there is no ambiguity here. Any instance of a rule $w, ac, m$, or $\equiv$ is translated to

an instance of the same rule, $\hat{c}_\vee$ is translated to $\hat{a}\hat{c}$, and $w_\vee$ is translated to $w$.

$A^\circ$ This gives us a derivation $\{w, ac, \hat{a}\hat{c}, m, \equiv^\circ\} \parallel \Phi^\circ$ such that $\lfloor \Phi^\circ \rfloor = \lfloor \Phi \rfloor$. It has been shown in [23] that $\lfloor \Phi^\circ \rfloor$ is a skew fibration. Hence, $\lfloor \Phi \rfloor$ is a skew fibration. □

### B. From Skew Bifibrations to Contraction and Weakening

**Lemma 43.** Let $A$ and $B$ be fographs, let $\varphi: A \to B$ be a skew bifibration, and let $A$ and $B$ be formulas with $\lfloor A \rfloor = A$ and $\lfloor B \rfloor = B$. Then there are derivations

$$ \{w, w_\vee, ac, \hat{c}_\vee, m, \hat{m}_\vee, \hat{m}_\vee, \equiv\} \parallel \hat{\Phi} \quad \text{and} \quad \{w, w_\vee, ac, c_\vee, m, m_\vee, m_\vee, \equiv\} \parallel \Phi \qquad \begin{array}{l} A \\ B \end{array} $$

such that $\lfloor \hat{\Phi} \rfloor = \varphi$ and $\hat{\Phi}$ is a rectification of $\Phi$, and $\rho_\varphi$ is the substitution induced by $\varphi$.

In the proof of this lemma, we make use of the following concept: Let $s \parallel \Psi$ be a derivation where $P$ and $Q$ are propositional formulas (possibly using variable $x \in \text{VAR}$ at the places of atoms). We say that $\Psi$ can be **lifted** to $S'$ if there are (first-order) formulas $C$ and $D$ such that $P = C^\circ$ and $Q = D^\circ$ and

$C$

$D$

there is a derivation $s' \parallel \Psi'$. □

We say a fograph homomorphism $\varphi: \mathcal{G} \to \mathcal{H}$ is **full** if for all $v, w \in V_G$, we have that $\varphi(v)\varphi(w) \in E_\mathcal{H}$ implies $vw \in E_G$.

**Lemma 44.** Let $\varphi: \mathcal{G} \to \mathcal{H}$ be full and injective skew bifibration such that $\rho_\varphi$ is the identity substitution, and let $\mathcal{G}$ and $\mathcal{H}$ be formulas with $\lfloor G \rfloor = \mathcal{G}$ and $\lfloor H \rfloor = \mathcal{H}$. Then

there is a derivation $\{w, w_\vee, \equiv\} \parallel \Phi$. □

*Proof.* By [23, Proposition 7.6.1], we have a derivation $G^\circ$

$\{w, \equiv^\circ\} \parallel \Psi$. In order to lift $\Psi$, we need to reorganize the $H^\circ$

instances of $w$. If $\mathcal{H}$ contains a subformula $\forall x.A$ which is not present in $\mathcal{G}$, the w-instances in $\Psi$ could introduce the parts of the propositional encoding $x \lor A$ independently. We say that an instance $r_1$ of $w$ in $\Phi$ is in the scope of an instance $r_2$ of $w$ if $r_1$ introduced formulas that contain a free variable $x$ (i.e., $x$ occurs in a term in a predicate) and $r_2$ introduces the atom $x$ as a subformula (i.e. the propositional encoding of the binder $x$). We can now permute the w-instances in $\Psi$ such that whenever a rule instance $r_1$ is in the scope of an instance $r_2$, then $r_2$ occurs below $r_1$ in $\Psi$. Then we can lift $\Psi$ stepwise. First, observe that each line of $\Psi$ is $\equiv^\circ$-equivalent to the propositional encoding $P^\circ$ of a first-order formula $P$. We now have to show that each instance of $w$ in $\Psi$ is indeed
The obvious next step in our research is to investigate proof composition and normalisation of first-order combinatorial proofs. Even in the propositional setting, the normalisation of combinatorial proofs is underdeveloped. There exist two different procedures for cut elimination for combinatorial proofs in classical propositional logic [10], [12], but both have their insufficiencies, and have not been extended to other logics.

We hope to garner new insights on the normalisation of classical first-order proofs through our work on combinatorial proofs.

REFERENCES

[1] G. Frege, *Begriffsschrift*. Louis Nebert, Halle, 1879, English Translation in: J. van Heijenoort (ed.), From Frege to Gödel, Harvard University Press: 1977.

[2] D. Hilbert, "Die logischen Grundlagen der Mathematik," *Mathematische Annalen*, vol. 88, pp. 151–165, 1922.

[3] G. Gentzen, "Untersuchungen über das logische Schließen. I." *Mathematische Zeitschrift*, vol. 39, pp. 176–210, 1935.

[4] G. Gentzen, "Untersuchungen über das logische Schließen. II." *Mathematische Zeitschrift*, vol. 39, pp. 405–431, 1935.

[5] R. M. Smullyan, *First-Order Logic*. Berlin: Springer-Verlag, 1968.

[6] J. A. Robinson, "A Machine-Oriented Logic Based on the Resolution Principle," *Journal of the ACM*, vol. 12, pp. 23–41, 1965.

[7] R. Thiele, "Hilbert's Twenty-fourth Problem," *American Mathematical Monthly*, vol. 110, pp. 1–24, 2003.

[8] D. Hilbert, "Mathematische Probleme," *Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, mathematisch-physikalische Klasse*, vol. 3, pp. 253–297, 1900.

[9] D. Hughes, "Proofs Without Syntax," *Annals of Mathematics*, vol. 164, no. 3, pp. 1065–1076, 2006.

[10] D. Hughes, "Towards Hilbert's 24th Problem: Combinatorial Proof Invariants:(preliminary version)," *Electronic Notes in Theoretical Computer Science*, vol. 165, pp. 37–63, 2006.

[11] L. Straßburger, "The Problem of Proof Identity, and Why Computer Scientists Should Care About Hilbert's 24th Problem," *Philosophical Transactions of the Royal Society A*, vol. 377, no. 2140, p. 20180038, 2019.

[12] L. Straßburger, "Combinatorial Flows and Their Normalisation," in *2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)*. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017.

[13] L. Straßburger, "Combinatorial Flows and Proof Compression," Inria Saclay, Research Report RR-9048, 2017. [Online]. Available: https://hal.inria.fr/hal-01498468

[14] M. Acclavio and L. Straßburger, "From Syntactic Proofs to Combinatorial Proofs," in *Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings*, D. Galmiche, S. Schulz, and R. Sebastiani, Eds., vol. 10900. Springer, 2018, pp. 481–497.

[15] M. Acclavio and L. Straßburger, "On Combinatorial Proofs for Logics of Relevance and Entailment," in *26th Workshop on Logic, Language, Information and Computation (WoLLIC 2019)*, R. Iemhoff and M. Moortgat, Eds. Springer, 2019.

[16] M. Acclavio and L. Straßburger, "On Combinatorial Proofs for Modal Logic," in *International Conference on Automated Reasoning with Analytic Tableaux and Related Methods*. Springer, 2019, pp. 223–240.

[17] W. Heijltjes, D. Hughes, and L. Straßburger, "Intuitionistic Proofs Without Syntax," in *2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*. IEEE, 2019, pp. 1–13.

[18] D. Hughes, "First-order Proofs Without Syntax," *arXiv preprint arXiv:1906.11236*, 2019.

[19] J.-Y. Girard, "Linear Logic," *Theoretical Computer Science*, vol. 50, pp. 1–102, 1987.

[20] S. Abramsky and R. Jagadeesan, "Games and Full Completeness for Multiplicative Linear Logic," *Journal of Symbolic Logic*, vol. 59, no. 2, pp. 543–574, 1994.

[21] J. Herbrand, "Recherches sur la Théorie de la Démonstration," Ph.D. dissertation, University of Paris, 1930.

[22] K. Brünnler, "Cut Elimination Inside a Deep Inference System for Classical Predicate Logic," *Studia Logica*, vol. 82, no. 1, pp. 51–71, 2006.

[23] L. Straßburger, "A Characterization of Medial as Rewriting Rule," in *International Conference on Rewriting Techniques and Applications*. Springer, 2007, pp. 344–358.

[24] A. S. Troelstra and H. Schwichtenberg, *Basic Proof Theory*. Cambridge University Press, 2000, no. 43.

[25] J.-Y. Girard, "Quantifiers in Linear Logic," *Temi e prospettive della logica e della filosofia della scienza contemporanea*, vol. 1, pp. 95–130, 1988.

[26] A. Fleury and C. Retoré, "The Mix Rule," *Math. Structures in Comp. Science*, vol. 4, no. 2, pp. 273–285, 1994.

[27] G. Bellin, "Subnets of Proof-nets in Multiplicative Linear Logic with MIX," *Mathematical Structures in Computer Science*, vol. 7, no. 6, pp. 663–699, 1997.

[28] H. Lerchs, "On cliques and kernels," 1971, Tech. report, U. Toronto.

[29] D. G. Corneil, H. Lerchs, and L. K. Stewart-Burlingham, "Complement reducible graphs," *Disc. Appl. Math.*, 1981.

[30] A. Grothendieck, "Technique de descente et théorèmes d'existence en géométrie algébrique. I. Généralités. Descente par morphismes fidèlement plats," in *Séminaire Bourbaki: années 1958/59-1959/60, exposés 169-204*. Société mathématique de France, 1960.

[31] J. W. Gray, "Fibred and cofibred categories," in *Proc. Conf. on Categorical Algebra '65*. Springer, 1966, pp. 21–83.

[32] K. Brünnler, "Deep Inference and Symmetry for Classical Proofs," Ph.D. dissertation, Technische Universität Dresden, 2003.

[33] B. Ralph, "Modular Normalisation of Classical Proofs," Ph.D. dissertation, University of Bath, 2019.

[34] A. A. Tubella and A. Guglielmi, "Subatomic Proof Systems: Splittable Systems," *ACM Transactions on Computational Logic (TOCL)*, vol. 19, no. 1, pp. 1–33, 2018.

[35] K. Brünnler, "Locality for Classical Logic," *Notre Dame Journal of Formal Logic*, vol. 47, no. 4, pp. 557–580, 2006. [Online]. Available: http://www.iam.unibe.ch/~kai/Papers/LocalityClassical.pdf

[36] J.-Y. Girard, "Proof-nets: The Parallel Syntax for Proof-theory," in *Logic and Algebra*, A. Ursini and P. Agliano, Eds. Marcel Dekker, New York, 1996.

[37] A. Guglielmi and L. Straßburger, "Non-commutativity and MELL in The Calculus of Structures," in *Computer Science Logic, CSL 2001*, ser. LNCS, L. Fribourg, Ed., vol. 2142. Springer-Verlag, 2001, pp. 54–68.

[38] L. Straßburger, "Linear logic and Noncommutativity in the Calculus of Structures," Ph.D. dissertation, Technische Universität Dresden, 2003.

[39] D. Hughes, "Unification Nets: Canonical Proof Net Quantifiers," in *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science*, 2018, pp. 540–549.

[40] A. A. Tubella and L. Straßburger, "Introduction to Deep Inference," 2019, lecture notes for ESSLLI'19. [Online]. Available: https://hal.inria.fr/hal-02390267

[41] K. Brünnler and A. F. Tiu, "A Local System for Classical Logic," in *International Conference on Logic for Programming Artificial Intelligence and Reasoning*. Springer, 2001, pp. 347–361.

[42] C. Retoré, "Pomset Logic as a Calculus of Directed Cographs," INRIA, Research Report RR-3714, 1999. [Online]. Available: https://hal.inria.fr/inria-00072953

[43] V. Danos and L. Regnier, "The Structure of Multiplicatives," *Archive for Mathematical Logic*, vol. 28, no. 3, pp. 181–203, 1989.

[44] C. Retoré, "Handsome Proof-nets: Perfect Matchings and Cographs," *Theoretical Computer Science*, vol. 294, no. 3, pp. 473–488, 2003.

[45] C. Retoré, "Handsome Proof-nets: R&B-Graphs, Perfect Matchings and Series-parallel Graphs," INRIA, Research Report RR-3652, 1999. [Online]. Available: https://hal.inria.fr/inria-00073020

[46] L. Straßburger, "Deep Inference and Expansion Trees for Second-order Multiplicative Linear Logic," *Mathematical Structures in Computer Science*, vol. 29, pp. 1030–1060, 2019.

[47] B. Ralph and L. Straßburger, "Towards a Combinatorial Proof Theory," in *International Conference on Automated Reasoning with Analytic Tableaux and Related Methods*. Springer, 2019, pp. 259–276.

[48] F. Lamarche, "Exploring the Gap Between Linear and Classical Logic," *Theory and Applications of Categories*, vol. 18, no. 18, pp. 473–535, 2007.
A. *Proof of Theorem 29*

*Proof of Theorem 29.* Write $fv(A)$ for the set of variables which occur free in $A$.

Note that the instances of $w, c$ in $\Phi_2$ are deep, but inside sequent contexts.

First, if an instance of $wk \frac{\vdash \Gamma}{\vdash \Gamma, A}$ is followed by a rule in which $A$ is not in the principal formula, it can be permuted downwards. Otherwise, the proof can be transformed using the following rewriting rules.

$$
\begin{align*}
wk \frac{\vdash \Gamma}{\vdash \Gamma, A} \quad & \vdash B, \Delta \\
\wedge \frac{\vdash \Gamma}{\vdash \Gamma, A \wedge B, \Delta} & \rightsquigarrow wk \frac{\vdash \Gamma}{\vdash \Gamma, A \wedge B, \Delta} \\
wk \frac{\vdash \Gamma, A}{\vdash \Gamma, A, B} & \rightsquigarrow w \frac{\vdash \Gamma, A}{\vdash \Gamma, A \vee B} \\
\vee \frac{\vdash \Gamma, A \vee B}{\vdash \Gamma, A \vee B} & \rightsquigarrow wk \frac{\vdash \Gamma}{\vdash \Gamma, \exists x.A} \\
wk \frac{\vdash \Gamma}{\vdash \Gamma, A[x/t]} & \rightsquigarrow wk \frac{\vdash \Gamma}{\vdash \Gamma, \exists x.A} \\
\forall \frac{\vdash \Gamma}{\vdash \Gamma, \forall x.A} & \rightsquigarrow wk \frac{\vdash \Gamma}{\vdash \Gamma, \forall x.A} \\
wk \frac{\vdash \Gamma, A}{\vdash \Gamma, A, A} & \rightsquigarrow \vdash \Gamma, A \\
ctr \frac{\vdash \Gamma, A}{\vdash \Gamma, A} & \rightsquigarrow \vdash \Gamma, A
\end{align*}
$$

Note that in the case of $\vee$, we use the deep rule $w$ which can be permuted under all the rules. By using these rewriting rules, we can eventually get a derivation with all the instances of $wk$ and $w$ at the bottom. Now observe that the instances of $ctr$ in $\Phi$ can be transformed using the following rule:

$$ \mathrm{ctr} \frac{\vdash \Gamma, A, A}{\vdash \Gamma, A} \rightsquigarrow \begin{array}[t]{c} \vee \\ c \end{array} \frac{\vdash \Gamma, A, A}{\vdash \Gamma, A \vee A} \frac{\vdash \Gamma, A}{\vdash \Gamma, A} $$

Knowing that $c$ can be permuted under all the rules of $\mathrm{MLL1}^x$, we eventually obtain a derivation:

$$
\begin{array}{ccc}
\mathrm{MLL1}^x & \Phi'_1 & \\
\frac{}{\vdash \Gamma'} & & \\
\{wk, w, c, \equiv\} & \parallel \Phi'_2 & \\
\frac{}{\vdash \Gamma} & &
\end{array}
$$

Note that $\equiv$ is required here since the permutation of formulas is implicit in $\mathrm{MLL1}^x$.

By transforming each sequent of $\Phi'_2$ into its corresponding formula, and by considering the following rewriting rule:

$$ wk \frac{\vdash \Gamma}{\vdash \Gamma, A} \rightsquigarrow w \frac{\vdash \vee(\Gamma)}{\vdash \vee(\Gamma) \vee A} $$

, we obtain a derivation

$$
\begin{array}{c}
\mathrm{MLL1}^x \quad \Phi_1 \\
\frac{}{\vdash \vee(\Gamma')} \\
\{w, c, \equiv\} \parallel \Phi_2 \\
\frac{}{\vdash \vee(\Gamma)}
\end{array}
$$

where $\Phi_1$ can be obtained from $\Phi'_1$ by applying the $\vee$ rule. $\square$

B. *Rule permutation for the proof of Lemma 31*

We construct a rewriting system based on rule permutation on derivations in $\{w, w_\vee, ac, c_\vee, m, m_\vee, m_\exists, \equiv\}$ that allows us to reach a derivation of the form

$$
\begin{array}{l@{\qquad}l}
\{m, m_\vee, m_\exists, \equiv\} & A \\
\{ac, c_\vee\} & A' \\
\{w, w_\vee, \equiv\} & B' \\
& B
\end{array}
$$

from any derivation. Intuitively, we want to move all the instances of $r \in \{w, w_\vee\}$ downwards and all the instances of $r' \in \{m, m_\vee, m_\exists\}$ upwards.

We first study the interactions between two rules. Certain cases are unsolved at this stage, and they are considered later when we study the interactions between two non-$\equiv$ rule instances separated by $\equiv$. Only non-trivial cases are presented here:

* $r_1/r_2$, where $r_1 \in \{w, w_\vee\}$ and $r_2 \in \{ac, c_\vee, m, m_\vee, m_\exists\}$:

$$ w \frac{a}{ac} \frac{a \vee a}{a} \rightsquigarrow a $$

$$
\begin{array}{r@{\quad}l@{\qquad}l}
w & \displaystyle \frac{A \wedge C}{(A \wedge C) \vee (B \wedge D)} \rightsquigarrow w \frac{A \wedge C}{(A \vee B) \wedge C} \\
m & \displaystyle \frac{A \wedge C}{(A \wedge B) \wedge (C \vee D)} \rightsquigarrow w \frac{A \wedge C}{(A \vee B) \wedge (C \wedge D)} \\
& \\
w & \displaystyle \frac{\forall x.A}{(\forall x.A) \vee (\forall x.B)} \rightsquigarrow w \frac{\forall x.A}{\forall x.(A \vee B)} \\
m_\vee & \displaystyle \frac{\forall x.A}{\forall x.(A \vee B)} \rightsquigarrow \forall x.A
\end{array}
$$

$$ w_\vee \frac{\forall x.A}{\forall x.\forall x.A} \rightsquigarrow \forall x.A $$

$$ \frac{A \vee (\forall x.B)}{m_\vee (\forall x.A) \vee (\forall x.B)} \rightsquigarrow \frac{A \vee (\forall x.B)}{\forall x.(A \vee B)} $$
where in the last case, $x$ is not free in $A$.

• $r_1/r_2$, where $r_1 \in \{\text{ac}, c_\vee\}$ and $r_2 \in \{\text{m}, m_\vee, m_\wedge\}$:

$$ \frac{c_\vee \frac{S(\forall x.\forall x.A) \lor (\forall x.B)}{S(\forall x.A) \lor (\forall x.B)}}{m_\vee \frac{S(\forall x.A) \lor (\forall x.B)}{S(\forall x.(A \lor B))}} \rightsquigarrow \frac{m_\vee \frac{S(\forall x.\forall x.A) \lor (\forall x.B)}{S(\forall x.(\forall x.A \lor B))}}{m_\vee \frac{S(\forall x.A) \lor (\forall x.B)}{S(\forall x.(A \lor B))}} $$

• $c_\vee/\equiv$:

$$ \begin{align*} \frac{c_\vee \frac{\forall x.\forall x.\forall y.A}{\forall x.\forall y.A}}{\equiv \frac{\forall y.\forall x.A}{\forall y.\forall x.A}} \rightsquigarrow & \equiv \frac{\forall x.\forall x.\forall y.A}{\forall y.\forall x.A} \\ \frac{c_\vee \frac{\forall x.\forall x.(A \lor B)}{\forall x.(A \lor B)}}{\equiv \frac{(\forall x.A) \lor B}{(\forall x.A) \lor B}} \rightsquigarrow & \equiv \frac{\forall x.\forall x.(A \lor B)}{(\forall x.\forall x.A) \lor B} \\ \frac{c_\vee \frac{(\forall x.\forall x.A) \lor B}{(\forall x.A) \lor B}}{\equiv \frac{\forall x.(A \lor B)}{\forall x.(A \lor B)}} \rightsquigarrow & \equiv \frac{\forall x.\forall x.(A \lor B)}{\forall x.\forall x.(A \lor B)} \end{align*} $$

where in the last two cases, $x$ is not free in $B$.

• $w/\equiv$:

$$ \begin{align*} \frac{w \frac{A}{A \lor B}}{\equiv \frac{B \lor A}{B \lor A}} & \rightsquigarrow \frac{w \frac{A \lor C}{(A \lor B) \lor C}}{\equiv \frac{A \lor C}{A \lor (B \lor C)}} \\ \frac{w \frac{\forall x.A}{\forall x.(A \lor B)}}{\equiv \frac{(\forall x.A) \lor B}{(\forall x.A) \lor B}} & \rightsquigarrow \frac{w \frac{\forall x.A}{(\forall x.A) \lor B}}{\equiv \frac{\forall x.B}{(\forall x.A) \lor B}} \\ \frac{w \frac{\forall x.A}{(\forall x.A) \lor B}}{\equiv \frac{\forall x.(A \lor B)}{\forall x.(A \lor B)}} & \rightsquigarrow \frac{w \frac{\forall x.A}{\forall x.(A \lor B)}}{\equiv \frac{B}{\forall x.(A \lor B)}} \end{align*} $$

where in the last four cases, $x$ is not free in $B$.

• $w_\vee/\equiv$:

In the following two cases, we assume $x \neq y$ (otherwise they are trivial).

$$ \frac{w_\vee \frac{\forall y.A}{\forall x.\forall y.A} (x \notin \mathbf{fv}(\forall y.A))}{\equiv \frac{\forall y.\forall x.A}{\forall y.\forall x.A}} \rightsquigarrow w_\vee \frac{\forall y.A}{\forall y.\forall x.A} (x \notin \mathbf{fv}(A)) $$

$$ \begin{align*} \frac{w_\vee \frac{\forall y.A}{\forall y.\forall x.A}}{\equiv \frac{\forall x.\forall y.A}{\forall x.\forall y.A}} (x \notin \mathbf{fv}(A)) \rightsquigarrow & \equiv \frac{w_\vee \frac{\forall y.A}{\forall x.\forall y.A}}{(x \notin \mathbf{fv}(\forall y.A))} \\ \frac{w_\vee \frac{A \lor B}{\forall x.(A \lor B)}}{\equiv \frac{(A \lor B)}{(\forall x.A) \lor B}} \rightsquigarrow & \equiv \frac{w_\vee \frac{A \lor B}{\forall x.(A) \lor B}}{(x \notin \mathbf{fv}(\forall x.A))} \\ \frac{w_\vee \frac{A \lor B}{\forall x.(A \lor B)}}{\equiv \frac{(A \lor B)}{\forall x.(A \lor B)}} \rightsquigarrow & \equiv \frac{w_\vee \frac{A \lor B}{\forall x.(A \lor B)}}{(x \notin \mathbf{fv}(\forall x.A))} \end{align*} $$

where in the last two cases, the constraint on $x$ on the left-hand side implies that of the right-hand side.

• $\equiv/c_\vee$:

$$ \begin{align*} \equiv \frac{c_\vee \frac{\forall x.\forall y.\forall x.A}{\forall x.\forall y.A}}{\forall x.\forall y.\forall x.A} & \equiv \frac{\forall x.\forall y.\forall x.A}{\forall x.\forall y.A} \\ \equiv \frac{c_\vee \frac{\forall x.\forall y.\forall x.A}{\forall y.\forall x.\forall x.A}}{\forall y.\forall x.\forall x.A} & \equiv \frac{\forall x.((\forall x.A) \lor B)}{(\forall x.\forall x.A) \lor B} (x \notin \mathbf{fv}(B)) \\ \equiv \frac{c_\vee \frac{\forall x.((\forall x.A) \lor B)}{\forall x.\forall x.(A \lor B)}}{\forall x.\forall x.(A \lor B)} & \equiv \frac{\forall x.((\forall x.A) \lor B)}{(x \notin \mathbf{fv}(B))} \end{align*} $$

• $\equiv/m$:

$$ \begin{align*} \equiv \frac{m \frac{(C \land A) \lor (B \land D)}{(A \land C) \lor (B \land D)}}{(A \lor B) \land (C \lor D)} & \rightsquigarrow \frac{m \frac{(B \land D) \lor (A \land C)}{(A \land C) \lor (B \land D)}}{(B \lor A) \land (D \lor C)} \\ \equiv \frac{m \frac{(B \land D) \lor (A \land C)}{(A \land C) \lor (B \land D)}}{(A \lor B) \land (C \lor D)} & \rightsquigarrow \equiv \frac{m \frac{((A \land C) \land E) \lor (B \land D)}{(A \land (C \land E)) \lor (B \land D)}}{(A \lor B) \land ((C \land E) \lor D)} \\ \equiv \frac{m \frac{((\forall x.(A \land C)) \lor (B \land D)}{\forall x.((A \land C) \lor (B \land D))}}{\forall x.((A \lor B) \land (C \lor D))} & \equiv \frac{m \frac{(\forall x.(A \land C)) \lor (B \land D)}{(x \notin \mathbf{fv}(B \land D))}}{\forall x.(A \lor B)} \end{align*} $$

• $\equiv/m_\vee$:

$$ \frac{m_\vee \frac{(\forall x.B) \lor (\forall x.A)}{(\forall x.A) \lor (\forall x.B)}}{\equiv \frac{\forall x.(A \lor B)}{\forall x.(A \lor B)}} \rightsquigarrow \frac{m_\vee \frac{(\forall x.B) \lor (\forall x.A)}{\forall x.(B \lor A)}}{\equiv \frac{\forall x.(A \lor B)}{\forall x.(A \lor B)}} $$
$$
\begin{align*}
\mathbf{m}_{\lor} & \equiv \frac{\frac{(\forall y.\forall x.A) \lor (\forall x.B)}{(\forall x.\forall y.A) \lor (\forall x.B)}}{\forall x.((\forall y.A) \lor B)} \\
\mathbf{m}_{\lor} & \equiv \frac{\frac{\forall x.(A \lor (\forall x.B))}{(\forall x.A) \lor (\forall x.B)}}{\forall x.(A \lor B)}
\end{align*}
$$

• $\equiv/m_{\exists}$: similar to $\equiv/m_{\lor}$

Interactions between two non-≡ rules with the presence of
≡ in between:

• $c_{\lor} / \equiv / r$ where $r \in \{m, m_{\lor}, m_{\exists}\}$: First permute $c_{\lor}$ under
$\equiv$ and then permute $c_{\lor}$ under $r$.

• ac/ ≡ /r where r ∈ {m, m_⊕, m_∃}: First permute ac under
≡ and then permute ac under r.

• w/ ≡ /c_∀:

$$
\begin{align*}
\frac{w}{c_{\forall}} \frac{\forall x.\forall x.A}{\equiv \frac{(\forall x.((\forall x.A) \lor B))}{(\forall x.\forall x.A) \lor B}} \rightsquigarrow \frac{c_{\forall}}{w} \frac{\forall x.\forall x.A}{\frac{(\forall x.A) \lor B}{(\forall x.A) \lor B}} \\
\frac{w}{c_{\forall}} \frac{\forall x.B}{\equiv \frac{(\forall x.(B \lor (\forall x.A)))}{(\forall x.\forall x.A) \lor B}} \rightsquigarrow \frac{w}{c_{\forall}} \frac{\forall x.B}{\equiv \frac{(\forall x.(B \lor A))}{(\forall x.A) \lor B}} \\
\frac{w}{c_{\forall}} \frac{\forall x.\forall x.A}{\equiv \frac{(\forall x.((\forall x.A) \lor B))}{\forall x.\forall x.(A \lor B)}} \rightsquigarrow \frac{c_{\forall}}{w} \frac{\forall x.\forall x.A}{\frac{\forall x.A}{\forall x.(A \lor B)}} \\
\frac{w}{c_{\forall}} \frac{\forall x.B}{\equiv \frac{(\forall x.(B \lor (\forall x.A)))}{\forall x.\forall x.(A \lor B)}} \rightsquigarrow \frac{w}{c_{\forall}} \frac{\forall x.B}{\equiv \frac{(\forall x.(B \lor A))}{\forall x.(A \lor B)}}
\end{align*}
$$

where in all four cases, $x$ is not free in $B$.

• w/ ≡ /ac:

$$
\begin{align*}
\frac{w}{ac} \frac{a \lor B}{\equiv \frac{(a \lor B) \lor a}{(a \lor a) \lor B}} \rightsquigarrow a \lor B \\
\frac{w}{ac} \frac{a}{\equiv \frac{a \lor (a \lor B)}{(a \lor a) \lor B}} \rightsquigarrow w \frac{a}{a \lor B} \\
\frac{w}{ac} \frac{\forall x.a}{\equiv \frac{(\forall x.a) \lor a}{\forall x.(a \lor a)}} (x \notin \mathbf{fv}(a)) \rightsquigarrow \forall x.a
\end{align*}
$$

$$
\begin{align*}
\frac{w}{ac} \frac{a}{\forall x.a} &\equiv \frac{a \lor (\forall x.a)}{\forall x.(a \lor a)} (x \notin \mathbf{fv}(a)) \rightsquigarrow w_{\lor} \frac{a}{\forall x.a} (x \notin \mathbf{fv}(a)) \\
\frac{w}{ac} \frac{C \land A}{(A \land C) \lor (B \land D)} &\equiv \frac{C \land A}{(A \land C) \lor (B \land D)} \rightsquigarrow w \frac{\forall}{(A \lor B) \land C} \frac{C \land A}{(A \lor B) \land (C \lor D)} \\
\frac{w}{m} \frac{B \land D}{\forall x.((A \land C) \lor (B \land D))} &\equiv \frac{\forall}{\forall x.((B \land A) \land D)} \frac{B \land D}{\forall x.((B \land A) \land C \land D)} \rightsquigarrow w \frac{\forall}{\forall x.((B \land A) \land (D \lor C))} \frac{B \land D}{\forall x.((A \lor B) \land (C \lor D))}
\end{align*}
$$

• w/ ≡ /m:

$$
\begin{align*}
\frac{w}{m} \frac{C \land A}{(A \land B) \land (C \lor D)} &\rightsquigarrow \frac{C \land A}{A \land C} \frac{C \land A}{(A \lor B) \land C} \\
\frac{w}{m} \frac{B \land D}{\forall x.((A \land C) \lor (B \land D))} &\rightsquigarrow \frac{\forall}{\forall x.((B \land A) \land D)} \frac{B \land D}{\forall x.((B \land A) \land C \land D)} \\
\frac{w}{m} \frac{B \land D}{\forall x.((A \land C) \lor (B \land D))} &\rightsquigarrow \frac{\forall}{\forall x.((B \land A) \land (D \lor C))} \frac{B \land D}{\forall x.((A \lor B) \land (C \lor D))}
\end{align*}
$$

where in the second case, $x$ is free in $B \land D$.

• w/ ≡ /m_∃:

$$
\begin{align*}
\frac{w}{m_{\exists}} \frac{\forall x.B}{\equiv \frac{(\forall x.B) \lor (\forall x.A)}{(\forall x.A) \lor (\forall x.B)}} \rightsquigarrow \frac{w}{m_{\exists}} \frac{\forall x.B}{\equiv \frac{(\forall x.(B \lor A))}{\forall x.(A \lor B)}} \\
\frac{w}{m_{\exists}} \frac{\forall x.\forall x.A}{\equiv \frac{(\forall x.((\forall x.A) \lor B))}{(\forall x.A) \lor (\forall x.B)}} \rightsquigarrow \frac{c_{\forall}}{w} \frac{\forall x.\forall x.A}{\frac{\forall x.A}{\forall x.(A \lor B)}}
\end{align*}
$$

• w/ ≡ /m_∃:

$$
\frac{w}{m_∃} \frac{\exists x.B}{\equiv \frac{(\exists x.B) \lor (\exists x.A)}{(\exists x.A) \lor (\exists x.B)}} \rightsquigarrow \frac{w}{m_∃} \frac{\exists x.B}{\equiv \frac{(\exists x.(B \lor A))}{\exists x.(A \lor B)}}
$$

C. *Proof of Lemma 45*

Proof of Lemma 45. By [47, Proposition 7.5], there is a
$(G\rho_{\varphi})^{\circ}$
derivation $\{ac, m, \equiv^{\circ}\} \parallel_{\Psi}^{\circ}$, We plan to show that $\Psi$ can be lifted
$H^{\circ}$
to $\{ac, c_{\lor}, m, m_{\lor}, m_{\exists}, \equiv\}$. However, observe that not every
formula occurring in $\Psi$ is a propositional encoding. There are
two reasons for this: (i) we might have $P \equiv^{\circ} Q$ where $P$
is a propositional encoding but $Q$ is not, and (ii) the rule ac
can duplicate an atom $x \in \text{VAR}$. Let us write $ac_x$ for such
instances. The problem with (i) is that we could have the
following situation

$$
\[
\begin{array}{r@{\,}c@{\,}l@{\quad}l@{\quad}l}
 & \multicolumn{2}{@{}c@{}}{\exists x.B} &
 & \multicolumn{2}{@{}c@{}}{\exists x.B} \\
\equiv & \multicolumn{1}{@{}c@{}}{\exists x.(B \lor A)} & \multicolumn{1}{@{}c@{}}{\lor} &
 & \multicolumn{1}{@{}c@{}}{\exists x.(B \lor A)} & \multicolumn{1}{@{}c@{}}{\lor} \\
\equiv & \multicolumn{1}{@{}c@{}}{\exists x.(A \lor B)} & \multicolumn{1}{@{}c@{}}{\lor} &
 & \multicolumn{1}{@{}c@{}}{\exists x.(A \lor B)} & \multicolumn{1}{@{}c@{}}{\lor}
\end{array}
\tag{7}
\]
$$
where $x$ occurs in $C \lor D$. Then premise and conclusion are both propositional encodings, but the whole derivation cannot be lifted. However, since we demand that the mapping is a fibration (and therefore a homomorphism) on the binding graphs, there must be another instance of $m$ further below in the derivation:

$$ m \frac{S'\{(x \land E) \lor (x \land F)\}}{S'\{(x \lor x) \land (E \lor F)\}} \qquad (8) $$

We can permute both instances via the following more general scheme (see [23], [48] for a general discussion on permutations of the m-rule):

$$ \frac{m \frac{S\{(G \land E \land C) \lor (G \land F \land D)\}}{S\{(G \lor H) \land (E \lor F) \land (C \lor D)\}} \leftrightarrow m \frac{S\{(G \land E \land C) \lor (G \land F \land D)\}}{S\{(G \lor H) \land (E \lor F) \land (C \lor D)\}}}{S\{(G \land E \land C) \lor (G \land F \land D)\}} \qquad (9) $$

We omitted some instances of $\equiv^\circ$ and some parentheses. We now call instances of $m$ as in (7) illegal, and we can transform $\Psi$ through m-permutations (9) into a derivation that does not contain any illegal m-instances. To address (ii), we also apply a permutation argument, permuting all instances of $ac_x$ up until they either reach the top of the derivation or an instance of $m$ which separates the two atoms in the premise. More precisely, we consider the following inference rule

$$ ac_x \frac{S_0\{S_1\{x\} \lor S_2\{x\}\}}{S\{x\}} \qquad (10) $$

where $S_1\{\cdot\} \equiv \{\cdot\} \lor E$ and $S_2\{\cdot\} \equiv \{\cdot\} \lor F$ and $S\{\cdot\} \equiv S_0\{\cdot\} \lor E \lor F$ for some formulas $E$ and $F$, where $E$ or $F$ or both might be empty. The rule $ac_x^\equiv$ permutes over $\equiv$, ac, and other instances of $ac_x^\equiv$, and over instances of $m$ if they occur inside $S_0$ or $S_1$ or $S_2$. The only situation in which $ac_x^\equiv$ cannot be permuted up is the following:

$$ \frac{m \frac{S\{(R_1\{x\} \land C) \lor (R_2\{x\} \land D)\}}{S\{(R_1\{x\} \lor R_2\{x\}) \land (C \lor D)\}}}{ac_x \equiv \frac{S\{R\{x\} \land (C \lor D)\}}{S\{R\{x\} \land (C \lor D)\}}} \qquad (11) $$

We can therefore assume that all instances of $ac_x$, that contract an atom $x \in VAR$ are either at the top of $\Psi$ or below a m-instance as in (11). We now lift $\Psi$ to $\{ac, c_\forall, m, m_\forall, m_\exists, \equiv\}$, proceed by induction on the height of $\Psi$, beginning at the top, making a case analysis on the topmost rule that is not a $\equiv$.

* $ac_x$: We know that the premise of (10) is a propositional encoding. Hence, $S_1\{\cdot\} = \{\cdot\} \lor E^\circ$ and $S_2\{\cdot\} = \{\cdot\} \lor F^\circ$ and both $x$ are universals, and $E^\circ \lor F^\circ$ contains all occurrences of $x$ bound by that universal. We have the following subcases:

- $E$ and $F$ are both non-empty: We have

$$ ac_x \equiv \frac{S^\circ\{(x \lor E^\circ) \lor (x \lor F^\circ)\}}{S^\circ\{x \lor (E^\circ \lor F^\circ)\}} $$

which can be lifted to

$$ m_\forall \frac{S\{(\forall x.E) \lor (\forall x.F)\}}{S\{\forall x.(E \lor F)\}} $$

where $S^\circ\{\cdot\}, E^\circ, F^\circ$ are the propositional encodings of $S\{\cdot\}, E, F$, respectively.

- $E^\circ$ is empty and $F^\circ$ is non-empty: We have

$$ ac_x \equiv \frac{S^\circ\{x \lor (x \lor F^\circ)\}}{S^\circ\{x \lor F^\circ\}} $$

which can be lifted to

$$ c_\forall \frac{S\{\forall x.\forall x.F\}}{S\{\forall x.F\}} $$

- $E^\circ$ is non-empty and $F^\circ$ is empty: This is similar to the previous case.

- $E^\circ$ and $F^\circ$ are both empty: This is impossible as the premise would not be a propositional encoding.

* ac (contracting an ordinary atom): This can trivially be lifted.

* m: There are several cases to consider.

- If none of the four principal formulas in the premise is $x$ or $x \lor F$ for some formula $F$ and $x \in VAR$, then this instance of $m$ can trivially be lifted, and we can proceed by induction hypothesis.

- If exactly one of the four principal formulas in the premise is $x$ for some $x \in VAR$, then this $x$ is the encoding of an existential in the premise and of an universal in the conclusion. This is impossible, as $\varphi$ has to preserve existentials.

- If two of the four principal formulas in the premise are $x$ for some $x \in VAR$, then we are in the following special case of (11):

$$ ac_x \equiv \frac{m \frac{S\{(x \land C) \lor (x \land D)\}}{S\{(x \lor x) \land (C \lor D)\}}}{S\{x \land (C \lor D)\}} $$

which can be lifted immediately to

$$ m_\exists \frac{S\{(\exists x.C) \lor (\exists x.D)\}}{S\{\exists x.(C \lor D)\}} $$

- We have a situation (11) where $R_1\{x\} \equiv x \lor E$ for some $E$ and $R_2\{x\} \equiv x \lor F$ for some $F$ with $R\{x\} \equiv x \lor E \lor F$ (Otherwise, the application of $ac_x^\equiv$ would not be correct.) That means, we have:

$$ ac_x \equiv \frac{m \frac{S\{(x \lor E) \land C) \lor ((x \lor F) \land D)\}}{S\{(x \lor E) \lor (x \lor F) \land (C \lor D)\}}}{S\{(x \lor E \lor F) \land (C \lor D)\}} $$

which can be lifted to

$$ m_\forall \frac{m \frac{S\{(\forall x.E) \land C) \lor ((\forall x.F) \land D)\}}{S\{(\forall x.E) \lor (\forall x.F) \land (C \lor D)\}}}{S\{(\forall x.(E \lor F)) \land (C \lor D)\}} $$

- In all other cases (e.g. exactly one of the principal formulas is of shape $x \lor F$ (and none is $x$), we can trivially lift the m-instance, as the quantifier structure is not affected.

$G\rho_\varphi$

Thus $\Psi$ can be lifted to $\{ac, c_\forall, m, m_\forall, m_\exists, \equiv\} \parallel \Phi$.

$H$

□