Combinatorial Proofs and Decomposition Theorems for First-order Logic

Dominic J. D. Hughes

Logic Group

U.C. Berkeley

Lutz Straßburger
Inria, Equipe Partout

Ecole Polytechnique, LIX

Jui-Hsuan Wu
Ecole Normale Supérieure

[][Long version of the LICS 2021 paper, with full proofs in the appendix.]

We uncover a close relationship between combinatorial and
syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are
formalized in a deductive proof system based on inference rules,
a combinatorial proof is a syntax-free presentation of a proof
that is independent from any set of inference rules. We show that
the two proof representations are related via a deep inference
decomposition theorem that establishes a new kind of normal form
for syntactic proofs. This yields (a) a simple proof
of soundness and completeness for first-order combinatorial
proofs, and (b) a full completeness theorem: every combinatorial
proof is the image of a syntactic proof.

§ INTRODUCTION

First-order predicate logic is a cornerstone of modern
logic. Since its formalisation by Frege [1] it has seen a
growing usage in many fields of mathematics and computer science. Upon
the development of proof theory by Hilbert [2],
proofs became first-class citizens as mathematical objects that
could be studied on their own. Since Gentzen's sequent
calculus [3, 4], many other proof systems
have been developed that allow the implementation of efficient proof
search, for example analytic tableaux [5] or
resolution [6]. Despite the immense progress
made in proof theory in general and in the area of
automated and interactive theorem provers in
particular, we still have
no satisfactory notion of proof identity for first-order logic. In
this respect, proof theory is quite different from any other
mathematical field. For example in group theory, two groups are
the same iff they are isomorphic; in topology, two spaces are
the same iff they are homeomorphic; etc. In proof theory, we
have no such notion telling us when two proofs are the same,
even though Hilbert was considering this problem as a possible 24th
problem [7] for his famous lecture in
1900 [8], before proof theory existed as a mathematical

The main reason for this problem is that formal proofs, as they are
usually studied in logic, are inextricably tied to the syntactic
(inference rule based) proof system in which they are carried out. And
it is difficult to compare two proofs that are produced within two
different syntactic proof systems, based on different sets of inference rules.
Consider the derivations in Figure <ref>, showing two proofs of the
formula $\peirceformula$ and two proofs of the formula $\veedrinkerformula$,
in sequent calculus (top) and in a deep inference system (bottom).
It is, a priori, not clear how to compare them.

syntactic proofs in sequent calculus (above)
and the calculus of structures (below)
which translate to the same propositional combinatorial proof (centre).

syntactic proofs
in sequent calculus (above)
and the new calculus $\FOKS$ introduced in this paper (below),
which translate to the same first-order combinatorial proof (centre).

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 $\peirceimpliesformula=\peirceformula$ is shown mid-left in
Fig. <ref>,

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. <ref> 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 Heijlties, 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  $=$
is shown on the right of Fig. <ref>,
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,
$\FOKS$, for first-order logic, that (a) reflects every combinatorial
proof, i.e., there is a surjection from $\FOKS$ 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

The right of Fig. <ref>
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 <cit.>).
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

Outline: This paper has three parts. First,
in Sections <ref>–<ref> we present the
preliminaries on first-order logic, first-order graphs,
first-order combinatorial proofs, and the first-order proof system
$\FOKS$. Second, in Section <ref> we state the main
results. And third, in
Sections <ref>–<ref> we give their

§ PRELIMINARIES: FIRST-ORDER LOGIC

§.§ Terms and Formulas

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

\begin{equation*}
\begin{array}{r@{~}l}
t &\coloneqq~ x \mid f(t_1,\dots,t_n)
\\[.5ex]
a &\coloneqq~ \ttt\mid\fff\mid p(t_1,\dots,t_n) \mid \dual p(t_1,\dots,t_n)
\\[.5ex]
A &\coloneqq~ a \mid A\vlan A \mid A\vlor A \mid \exists x.A \mid \forall x.A
\end{array}
\end{equation*}

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

\begin{equation*}
\begin{array}{c@{\hspace{6ex}}c}
%    \dual{\dual a} = a
%    &
\dual\ttt =\fff &
\dual{p(t_1,\ldots,t_n)} = \dual{p}(t_1,\ldots,t_n) \\[.5ex]
%  &
\dual\fff = \ttt &
\dual{\dual p(t_1,\ldots,t_n)} = p(t_1,\ldots,t_n) \\[.5ex]
%  &
\dual{\exists x.A} = \forall x.\dual{A}
\dual{A \vlan B} = \dual{A} \ \vlor \ \dual{B} \\[.5ex]
%  &
\dual{\forall x.A} = \exists x.\dual{A}
%  \\[.5ex]
\dual{A \vlor B} = \dual{A} \ \vlan \ \dual{B}
\end{array}
\end{equation*}

Note $\dual{\dual a} = a$.
We write $A\implies B$ as an abbreviation for $\dual A\vlor 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.
$\mapsto$ .

If we consider formulas equivalent
modulo bound variable renaming ($\alpha$-conversion), the
rectified form of a formula $A$ is unique, and we denote it
by $\rectif A$.

A substitution is a function $\sigma\colon\VAR\to\TERM$ that is
the identity almost everywhere. We denote substitutions as
$\sigma=\sublist{\subst{x_1}{t_1},\ldots,\subst{x_n}{t_n}}$, where
$\sigma(x_i)=t_i$ for $i=1..n$ and $\sigma(x)=x$ for all
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\VAR$ for all variables $x$.

§.§ Sequent Calculus $\FOLK$

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

In this paper we use the sequent calculus $\FOLK$, shown in
Figure <ref>, 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 $\mixr$ rule.

$\FOLK$ is sound and complete for first-order logic.

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

The linear fragment of $\FOLK$, i.e., the fragment without the rules
$\conr$ (contraction) and $\weakr$ (weakening) defines
first-order multiplicative linear
logic [19, 25] with
mix [26, 27] (MLL1+mix). We denote that
system here with $\FOMLL$ (shown in Figure <ref> in the dashed

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

\begin{equation}
\vliinf{\cutr}{}{\sqn{\Gamma,\Delta}}{\sqn{\Gamma,A}}{\sqn{\dual A,\Delta}}
\end{equation}

If a sequent $\sqn\Gamma$ is provable in $\FOLKcut$ then it is also
provable in $\FOLK$. Furthermore, if $\sqn\Gamma$ is provable in
$\FOMLLcut$ then it is also provable in $\FOMLL$.

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

§ PRELIMINARIES: FIRST-ORDER GRAPHS

§.§ Graphs

A graph $\gG=\tuple{\vG,\eG}$ is a pair where $\vG$ is a finite
set of vertices and $\eG$ is a finite set of edges,
which are two-element subsets of $\vG$. We write $vw$ for an edge

Let $\gG=\tuple{\vG,\eG}$ and $\gH=\tuple{\vH,\eH}$ be graphs such
that $\vG\cap\vH=\emptyset$. A homomorphism
$\phi\colon\gG\to\gH$ is a function $\phi\colon\vG\to\vH$ such that if
$vw\in\eG$ then $\phi(v)\phi(w)\in\eH$. The union $\gG +\gH$ is
the graph $\tuple{\vG \cup\vH,\eG\cup \eH}$ and the join $\gG
\times \gH$ is the graph $\tuple{\vG \cup\vH,\eG \cup \eH \cup \set{vw
\mid v \in \vG, w \in \vH}}$.  A graph $\gG$ is disconnected
if $\gG=\gG_1+\gG_2$ for two non-empty graphs $\gG_1,\gG_2$, otherwise
it is connected.

A graph $\gG$ is labelled in a set $L$ if each vertex $v\in\vG$
has an associated label $\labelof v\in L$.
A graph $\gG$ is (partially) coloured if it carries a partial
equivalence relation $\linkingof\gG$ on $\vG$;

each equivalence class is a colour.[In
[9] and [18]
adjacent vertices must have distinct colours, following
the standard definition of colouring in graph
We choose to omit this condition here, as it is implied
by the preclusion of bimatchings in Def. <ref>.]

A vertex renaming of
$\gG=\tuple{\vG,\eG}$ along a bijection
$(\hat\cdot)\colon\vG\to\hat\vG$ is the graph
$\hat\gG=\tuple{\hat\vG,\set{\hat v\hat w\mid vw\in\eG}}$, with
colouring and/or labelling inherited (i.e., $\hat v\samecol\hat w$ if
$v\samecol w$, and $\ell(\hat v)=\ell(v)$). Following standard graph
theory, we identify graphs modulo vertex renaming.

A directed graph $\gG =\tuple{\vG,\eG}$ is a set $\vG$ of
vertices and a set $\eG\subseteq \vG\times\vG$ of direct edges.
A directed graph homomorphism
$\phi\colon\tuple{\vG,\eG}\to\tuple{\vH,\eH}$ is a function $\phi\colon\vG\to\vH$ such that if
$\pair{v,w}\in\eG$ then $\pair{\phi(v),\phi(w)}\in\eH$.

\begin{array}{@{}c@{}}
\dbox{%
\begin{array}{c}
\vlinf{\axr}{}{\sqn{a,\cneg a}}{}
\qquad
\vlinf{\vlor}{}{\sqn{\Gamma,A\vlor B}}{\sqn{\Gamma,A,B}}
\qquad
\vliinf{\vlan}{}{\sqn{\Gamma,A\vlan B, \Delta}}{\sqn{\Gamma,A}}{\sqn{B,\Delta}}
\\ \\[-1ex]
\vlinf{\ttt}{}{\sqn{\ttt}}{}
\qquad\;
\vlinf{\fff}{}{\sqn{\Gamma,\fff}}{\sqn{\Gamma}}
\qquad\;
\vliinf{\mixr}{}{\sqn{\Gamma,\Delta}}{\sqn\Gamma}{\sqn\Delta}
\\ \\[-1ex]
\vlinf{\exists}{}{\sqn{\Gamma,\exists x.A}}{\sqn{\Gamma,A\ssubst{x}{t}}}
\qquad
\vlinf{\forall}{\text{($x$ not free in $\Gamma$)}}{\sqn{\Gamma,\forall x.A}}{\sqn{\Gamma,A}}
\end{array}
\\\\[-1ex]
\vlinf{\conr}{}{\sqn{\Gamma,A}}{\sqn{\Gamma,A,A}}
\qquad
\vlinf{\weakr}{}{\sqn{\Gamma,A}}{\sqn{\Gamma}}
\end{array}

Sequent calculi $\FOLK$ (all rules) and $\FOMLL$ (rules in the dashed box)

§.§ Cographs

A graph $\gH=\tuple{\vH,\eH}$ is a subgraph of a graph
$\gG=\tuple{\vG,\eG}$ if $\vH\subseteq\vG$ and $\eH\subseteq\eG$. It
is induced if $v,w\in\vH$ and $vw\in\eG$ implies $vw\in\eH$. An induced
subgraph of $\gG=\tuple{\vG,\eG}$ is uniquely determined by its set of vertices
$V$ and we denote it by $\gG[V]$.
A graph is $\gH$-free if it does not contain $\gH$ as an induced
subgraph.  The graph $\Pfour$ is the (undirected) graph
$\tuple{\set{v_1, v_2, v_3, v_4},\set{v_1v_2, v_2v_3, v_3v_4}}$.  A
cograph is a $P_4$-free undirected graph. The interest in
cographs for our paper comes from the following well-known fact.

A graph is a cograph iff it can be constructed from the singletons
via the operations $+$ and $\times$.

In a graph $\gG$, the neighbourhood $N(v)$ of a vertex $v \in\vG$ is
$\set{w \mkern-2mu\mid\mkern-2mu vw \mkern-2mu\in\mkern-2mu\eG}$. A module is a set $M \mkern-2mu\subseteq\mkern-2mu \vG$
with $N(v) \mkern-1mu\setminus\mkern-1mu M = N(w) \mkern-1mu\setminus\mkern-1mu M$
for all $v, w \in M$. A module $M$ is strong if for every
module $M'$ we have $M' \mkern-2mu\subseteq\mkern-2mu M$, $M \mkern-2mu\subseteq\mkern-2mu M'$ or $M \cap M' =
\emptyset$. A module is proper if it has two or more vertices.

§.§ 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 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 $\gG$, a binder $b$ is
existential (resp. universal) if, for every other vertex
$v$ in its scope, we have $bv \in \eG$ (resp. $bv \notin \eG$). An
$x$-binder is legal if its scope contains no other $x$-binder
and at least one literal.

A first-order graph or fograph $\gG$ is a logical cograph whose binders are all legal. The
binding graph of $\gG$ is the directed graph $\bG=\tuple{\vG,
\set{(b, l) \mid b \text{ binds } l}}$.

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

\begin{equation*}
\begin{array}{r@{\;}l@{\hskip4em}r@{\;}l}
%% \multicolumn{4}{c}{
%%   \quad\graphof{\ttt}=\single\ttt
%%   \qquad
%%   \graphof{\fff}=\single\fff
%%   \qquad
%% \graphof{a} = \single a \hbox{\hskip1em(for any atom $a$)} } \\[1.1ex]
\graphof{a} &= \single a \rlap{\hskip1em(for any atom $a$)}  \\[.9ex]
\graphof{A \cor B} &= \graphof{A} + \graphof{B} &
\graphof{\exists x . A} &= \single x \times \graphof{A} \\[.9ex]
\graphof{A \cand B} &= \graphof{A} \times \graphof{B} &
\graphof{\forall x . A} &= \single x + \graphof{A}
\end{array}
\end{equation*}

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

Here is the fograph of the drinker formula $\drinkerformula=\veedrinkerformula$:

[baseline=([yshift=-1.5ex]current bounding box.north)]

If $A$ is a rectified formula then $\graphof A$ is a fograph.

That $\graphof A$ is a logical cograph follows immediately from the definition and Theorem <ref>.
The fact that every binder of $\graphof A$ is legal can be proved by
structural induction on $A$.

Note that $\graphof A$ need not be a fograph if $A$ is not
rectified. If $A = (\forall x. px) \vlor (\forall x. qx)$, then
$\graphof A = \single x \ \single px \ \single x \ \single 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 $\graphof\cdot$. For
example, in the graph of $(\exists x. px) \vlor (\exists x. qx)$,
both $x$-binders are legal, as they are not in each other's

We define a congruence relation $\fequ$ on formulas, called equivalence,
by the following equations:

\begin{equation}
\label{eq:fequ}
<EMAIL_ADDRESS>A \vlan B \fequ B \vlan A
(A \vlan B) \vlan C \fequ A \vlan (B \vlan C)
\\
A \vlor B \fequ B \vlor A
(A \vlor B) \vlor C \fequ A \vlor (B \vlor C)
\\
\forall x . \forall y . A \fequ \forall y . \forall x . A
\forall x . (A \vlor B) \fequ (\forall x . A) \vlor B
\\
\exists x . \exists y . A \fequ \exists y . \exists x . A
\exists x . (A \vlan B) \fequ (\exists x . A) \vlan B
\end{array}
\end{equation}

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

Let $A,B$ be rectified formulas. Then

A\fequ B \iff \graphof A =\graphof B

A straightforward structural induction on formulas.

$\fequ$ , and both formulas

have the same (rectified) fograph
$\drinkergraph$, below-left.

\begin{equation*}
\drinkergraphpic
\hspace{8ex}
\drinkercotreepic
\hspace{8ex}
\drinkerbindinggraphpic
\end{equation*}

Above-center we show the cotree of the underlying
cograph (illustrating the idea behind Theorem <ref>) and
above-right is its binding graph $\bD$.

§ FIRST-ORDER COMBINATORIAL PROOFS

§.§ Fonets

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

Let $\gC$ be a linked fograph. The set of links can be seen as a unification problem
by identifying dual predicate symbols. A dualizer of $\gC$ is a substitution $\delta$
unifying all the links of $\gC$. 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 $\set{\single x, \single y}$ of an
existential binder $\single x$ and a universal binder $\single 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 $\lgC$ of $\gC$ is the undirected
graph $\tuple{\vC, \lpC}$ where $\lpC$ is the set of leaps of $\gC$.
A vertex set $W \subseteq \vC$ induces a matching in
$\gC$ 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 $\gC$ if it induces a matching in $\gC$ and a matching in $\lgC$.

A first-order net or fonet is a linked fograph which
has a dualizer but no induced bimatching.

A fonet (left) with
dualizer $\protect\twolinkassignment$
and its
leap graph (right).

Figure <ref> shows a fonet with its dualizer and leap graph.

\begin{tikzpicture}\cptwoonformula
\end{tikzpicture}
\qquad
\begin{tikzpicture}\cponeonformula
\end{tikzpicture}
\qquad
\begin{tikzpicture}\cpthreeonformula
\end{tikzpicture}
\qquad
\begin{tikzpicture}\cpfouronformula
\end{tikzpicture}

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 $\phi$,
the variable substitution $\protect\rsubstof\phi$ is an identity,
thus we can omit labels from each (coloured) source fograph
(since the label of $v$ in the source is that of $\phi(v)$ in the target).

\begin{tikzpicture}
\cptwoinline
\end{tikzpicture}
\qquad\;
\begin{tikzpicture}
\cponeinline
\end{tikzpicture}
\qquad\;
\begin{tikzpicture}
\cpthreeinline
\end{tikzpicture}
\qquad\;
\begin{tikzpicture}
\cpfourinline
\end{tikzpicture}

Condensed forms of the four combinatorial proofs in Figure <ref>. We do not show the lower graph, and indicate the mapping by the position of the vertices of the upper graph.

§.§ Skew Bifibrations

A graph homomorphism $\phi\colon \tuple{\vG, \eG} \rightarrow
\tuple{\vH, \eH}$ is a fibration [30, 31] if
for all $v \in \vG$ and
$w\phi(v) \in \eH$, there exists a unique $\tilde{w} \in \vG$ such
that $\tilde{w}v \in \eG$ and $\phi(\tilde{w}) = w$ (indicated below-left),
and is a skew fibration <cit.> if
for all $v \in \vG$ and $w\phi(v) \in \eH$
there exists $\tilde{w} \in \vG$ such that $\tilde{w}v \in \eG$ and
$\phi(\tilde{w})w \notin \eH$ (indicated below-centre).
A directed graph homomorphism is a
fibration if for all $v \in \vG$ and $\pair{w,\phi(v)} \in
\eH$, there exists a unique $\tilde{w} \in \vG$ such that $\pair{\tilde{w},v}
\in \eG$ and $\phi(\tilde{w}) = w$ (indicated below-right).

A fograph homomorphism $\phi=\tuple{\phi,\rsubstof\phi}$ is a
pair where $\phi\colon\gG\to\gH$ is a graph homomorphism between the
underlying graphs, and $\rsubstof\phi$, also called the
substitution induced by $\phi$, is a variable renaming
such that
for all $v\in\vG$ we have
$\labelof{\phi(v)}=\rsubstof\phi(\labelof v)$,
and $\rsubstof\phi$ is the identity on variables not in $\gG$.

Note that $\phi$ necessarily maps binders to binders
and literals to literals.

Since $\rsubstof\phi$ is fully determined by $\phi$ alone, we often
leave $\rsubstof\phi$ implicit.
A fograph homomorphism $\phi\colon\gG \rightarrow \gH$
preserves existentials
if for all existential binders $b$ in
$\gG$, the binder $\phi(b)$ is existential in $\gH$.

Let $\gG$ and $\gH$ be fographs. A skew bifibration
$\phi\colon\gG\to\gH$ is an existential-preserving fograph
homomorphism that is a skew fibration on $\tuple{\vG, \eG} \to
\tuple{\vH, \eH}$ and a fibration on the binding graphs $\bG\to\bH$.

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.

A first-order combinatorial proof (FOCP) of a fograph $\gG$ is a skew
bifibration $\phi\colon \gC \rightarrow \gG$ where $\gC$ is a fonet. A first-order
combinatorial proof of a formula $A$ is a combinatorial proof of its graph

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

FOCPs are sound and complete for first-order logic.

Our definition of FOCP is slightly more lax than the original
definition of [18], as we allow for a variable
renaming $\rsubstof\phi$ which was restricted to be the identity
in [18].

§ FIRST-ORDER DEEP INFERENCE SYSTEM $\FOKS$

\begin{array}{@{}c@{}}
\dbox{%
\begin{array}{c}
\vlinf{\faD}{}{\Scons{\forall x.\ttt}}{\Scons\ttt}
\qquad
\vlinf{\aiD}{}{\Scons{a\vlor\cneg a}}{\Scons\ttt}
\qquad
\vlinf{\tttD}{}{\Scons{A\vlan\ttt}}{\Scons A}
\\ \\[-1ex]
\vlinf{\sw}{}{\Scons{(A\vlan B)\vlor C}}{\Scons{A\vlan (B\vlor C)}}
\qquad
\vlinf{\mix}{}{\Scons{A\vlor B}}{\Scons{A\vlan B}}
\\ \\[-1ex]
\vlinf{\exD}{}{\Scons{\exists x.A}}{\Scons{A\ssubst x t}}
\qquad
\vlinf{\fequ}{\text{(where $A\fequ B$)}}{\Scons{A}}{\Scons{B}}
\end{array}
\\ \\[-1ex]
\vlinf{\wrD}{}{\Scons{A\vlor B}}{\Scons{A}}
\quad\;
\vlinf{\me}{}{\Scons{(A\vlor B)\vlan(C\vlor D)}}{\Scons{(A\vlan C)\vlor(B\vlan D)}}
\quad\;
\vlinf{\acD}{}{\Scons{a}}{\Scons{a\vlor a}}
\\ \\[-1ex]
\vlinf{\mfaD}{}{\Scons{\forall x.(A\vlor B)}}{\Scons{(\forall x.A)\vlor(\forall x.B)}}
\qquad
\vlinf{\mexD}{}{\Scons{\exists x.(A\vlor B)}}{\Scons{(\exists x.A)\vlor(\exists x.B)}}
\\ \\[-1ex]
\vlinf{\wfaD}{\text{($x$ not free in $A$)}}{\Scons{\forall x.A}}{\Scons{A}}
\qquad
\vlinf{\cfaD}{}{\Scons{\forall x. A}}{\Scons{\forall x.\forall x.A}}
\end{array}

Deep inference systems $\FOKS$ (all rules) and $\FOMLS$ (rules in the dashed box)

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 $\Sconhole$, and which is a
formula (resp. sequent) with exactly one occurrence of the hole
$\conhole$ in the position of an atom. Then $\Scons A$ is the result
of replacing the hole $\conhole$ in $\Sconhole$ with $A$.

Figure <ref> shows the inference rules for the deep inference
system $\FOKS$ 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 $\mixr$-rule, (ii) a different
choice of how the formula equivalence $\fequ$ is defined, (iii) an
explicit rule for the equivalence, and (iv) new inference rules
$\wfaD$ and $\cfaD$. 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]).
[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.]

As with the sequent system $\FOLK$, we also need for $\FOKS$ the
linear fragment, $\FOMLS$, and that is shown
in Figure <ref> in the dashed box.

We write $\vlder{\sysS}{\Deri}{A}{B}$ to denote a derivation $\Deri$
from $B$ to $A$ using the rules from system $\sysS$. A formula $A$ is
provable in a system $\sysS$ if there is a derivation in
$\sysS$ from $\ttt$ to $A$.

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

\begin{equation}
\vlinf{\cD}{}{\Scons{A}}{\Scons{A\vlor A}}
\end{equation}

§ 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:

$\FOKS$ 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.

For every derivation $\vlder{\FOKS}{\Deri}{A}{\ttt}$ there are $\fff$-free formulas $A_1,\ldots,A_5$ and a derivation

\begin{equation*}
\scalebox{.9}{$
\vlderivation{
\vlde{\set{\wrD,\wfaD,\fequ}}{}{A}{
\vlde{\set{\acD,\cfaD}}{}{A_1}{
\vlde{\set{\me,\mfaD,\mexD,\fequ}}{}{A_2}{
\vlde{\set{\exD}}{}{A_3}{
\vlde{\set{\sw,\mix,\fequ}}{}{A_4}{
\vlde{\set{\faD,\aiD,\tttD}}{}{A_5}{
\vlhy{\ttt}}}}}}}}
\end{equation*}

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].

Theorem <ref> is also the reason why we have the rules
$\wfaD$ and $\cfaD$ in system $\FOKS$, as these rules are derivable
with the other rules. However, they are needed to obtain this

Figure <ref> shows an example of a decomposed derivation in $\FOKS$ of the
formula $(\exists x. \cneg{p}x) \vlor (\forall y.(py \vlan pfy))$.

\begin{equation*}
\scalebox{.9}{$
\vlderivation{
\vlin{\acD}{}{(\exists x. \cneg{p}x) \vlor (\forall y.(py \vlan pfy))}{
\vlin{\mexD}{}{(\exists x. (\cneg{p}x \vlor \cneg{p}x) \vlor (\forall
y.(py \vlan pfy))}{
\vlin{\fequ}{}{((\exists x. \cneg{p}x) \vlor (\exists x.\cneg{p}x))
\vlor (\forall y.(py \vlan pfy)}{
\vlin{\exists}{}{\forall y.(((\exists x. \cneg{p}x) \vlor (\exists
x.\cneg{p}x)) \vlor (py \vlan pfy))}{
\vlin{\exists}{}{\forall y.((\cneg{p}y \vlor (\exists x.\cneg{p}x))
\vlor (py \vlan pfy))}{
\vlin{\fequ}{}{\forall y.((\cneg{p}y \vlor \cneg{p}fy) \vlor
(py \vlan pfy))}{
\vlin{\sw}{}{\forall y.(\cneg{p}y \vlor ((py \vlan pfy)
\vlor \cneg{p}fy))}{
\vlin{\fequ}{}{\forall y.(\cneg{p}y \vlor (py \vlan (pfy
\vlor \cneg{p}fy)))}{
\vlin{\aiD}{}{\forall y.((\cneg{p}y \vlor py) \vlan (pfy
\vlor \cneg{p}fy))}{
\vlin{\aiD}{}{\forall y.((\cneg{p}y \vlor py) \vlan
\ttt)}{
\vlin{\ttt}{}{\forall y.(\ttt \vlan \ttt)}{
\vlin{\forall}{}{\forall y.\ttt}{
\vlhy{\ttt}}}}}}}}}}}}}}
\end{equation*}

Example derivation in decomposed form of Theorem <ref>

A weaker version of Theorem <ref> will
also be useful:

For every derivation $\rule{0ex}{4.7ex}\upsmash{\vlder{\FOKS}{\Deri}{A}{\ttt}}$
there is a formula $A'$ with no occurrence of $\fff$ and a derivation

\begin{equation*}
\vlderivation{
\vlde{\set{\wrD,\cD,\fequ}}{}{A}{
\vlde{\FOMLS}{}{A'}{
\vlhy{\ttt}}}}
% $}
\end{equation*}

Here $A'$ corresponds to $A_3$ of Theorem <ref>.

We now establish the connection between derivations in $\FOKS$ and
combinatorial proofs.

Let  $\phi\colon\gC\to\gA$ be a combinatorial proof and let $A$ be a formula with $\gA=\graphof A$. Then there is a derivation

\begin{equation}
\label{eq:decom}
\vlderivation{
\vlde{\set{\wrD,\wfaD,\acD,\cfaD,\me,\mfaD,\mexD,\fequ}}{\Deri_2}{A}{
\vlde{\FOMLS}{\Deri_1}{A'}{
\vlhy{\ttt}}}}
\end{equation}

for some $A'\fequ C\rsubstof\phi$ where $C$ is a formula with $\graphof
C=\gC$ and $\rsubstof\phi$ is the variable renaming substitution
induced by $\phi$.  Conversely,
whenever we have a derivation as in (<ref>) above, such that $\fff$ does not occur in $A'$, then
there is a combinatorial proof $\phi\colon\gC\to\graphof A$ such
that $\gC=\graphof{\rectif{A'}}$.

Furthermore, in the proof of Theorem <ref>, we will see that
(i) the links in the fonet $\gC$ correspond precisely to the pairs of
atoms that meet in the instances of the $\aiD$-rule in the derivation
$\Deri_1$, and (ii) the ”flow-graph” of $\Deri_2$ that traces the
quantifier- and atom-occurrences in the derivation corresponds exactly
to the vertex-mapping induced by $\phi$. To give an example, consider
the derivation in Figure <ref> which corresponds
to the left-most combinatorial proof in Figures <ref>
and <ref>.

Thus, combinatorial proofs are closely related to derivations of the
form (<ref>), and since by Theorem <ref>
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 <ref>, <ref>
and <ref> imply Theorem <ref>, 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).

§ TRANSLATING BETWEEN $\FOLK$ AND $\FOKS$

We prove Theorems <ref>,
<ref>, and <ref>, mainly by
translating derivations to and from the sequent calculus, and by rule
permutation arguments.

§.§ The Linear Fragments $\FOMLL$ and $\FOMLS$

We show that $\FOMLL$ and $\FOMLS$ are equivalent.

If $\sqn\Gamma$ is provable in $\FOMLL$ then $\form\Gamma$ is provable in  $\FOMLS$.

This is a straightforward induction on the proof of $\sqn\Gamma$ in
$\FOMLL$, making a case analysis on the bottommost rule instance. We
show here only the case of

$\vlinf{\forall}{}{\sqn{\Delta,\forall x.A}}{\sqn{\Delta,A}}$ (all
other cases are simpler or have been shown before,
e.g. [32]): By induction hypothesis, there is a proof
of $\form\Delta\vlor A$ in $\FOMLS$. We can prefix every line in
that proof by $\forall x$ and then compose the following derivation:

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

Let $\vlinf{\rr}{}{\Scons B}{\Scons A}$ be an inference rule in
$\FOMLS$. Then the sequent $\sqn{\cneg A,B}$ is provable in $\FOMLL$.

A routine exercise.

Let $A,B$ be formulas, and let $\Sconhole$ be a (positive)
context. If $\sqn{\cneg A,B}$ is provable in $\FOMLL$, then so is
$\sqn{\cneg{\Scons A},\Scons B}$.

A straightforward induction on $\Sconhole$. (see e.g. [37])

If a formula $C$ is provable in $\FOMLS$ then $\sqn C$ is provable in  $\FOMLL$.

We proceed by induction on the number of inference steps in the
proof of $C$ in $\FOMLS$. Consider the bottommost rule instance
$\vlinf{\rr}{}{\Scons B}{\Scons A}$. By induction hypothesis we have
a $\FOMLL$ proof $\Proof$ of $\sqn{\Scons A}$.
By Lemmas <ref> and <ref>, we have a $\FOMLL$ proof of
$\sqn{\cneg{\Scons A},\Scons B}$. We can compose them via

\begin{equation*}
\vliinf{\cutr}{}{\sqn{\Scons B}}{\sqn{\Scons A}}{\sqn{\cneg{\Scons
A},\Scons B}}
\end{equation*}

and then apply Theorem <ref>.

§.§ Contraction and Weakening

The first observation here is that Lemmas <ref>–<ref> from above also hold for $\FOLK$ and $\FOKS$. We therefore immediately have:

For every sequent $\Gamma$, we have that $\sqn\Gamma$ is provable in
$\FOLK$ if and only if $\form\Gamma$ is provable in $\FOKS$.

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

The $\cD$-rule is derivable in $\set{\acD,\me,\mfaD,\mexD,\fequ}$.

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

$\wfaD,\cfaD,\me,\mfaD,\mexD$ are derivable in $\set{\wrD,\cD,\fequ}$.

We only show the cases for $\wfaD$ and $\cfaD$ (for the others see [32]):

\begin{equation}
\label{eq:wfa-cfa}
\qquad
\vlderivation{
\vlin{\cD}{}{\forall x.A}{
\vlin{\fequ}{}{\forall x.(A \vlor A)}{
\vlin{\wrD}{}{A \vlor (\forall x.A)}{
\vlhy{A}}}}}
\qquad
\quad
\vlderivation{
\vlin{\cD}{}{\forall x.A}{
\vlin{\equiv}{}{(\forall x.A) \vlor (\forall x.A)}{
\vlin{\wrD}{}{\forall x.((\forall x.A) \vlor A)}{
\vlhy{\forall x.\forall x.A}}}}}
\end{equation}

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

Let $A$ and $B$ be formulas. Then

\begin{equation*}
\vlderivation{
\vlde{\set{\wrD,\cD,\fequ}}{}{B}{
\vlhy{A}}}
\qquad
\iff
\qquad
\vlderivation{
\vlde{\set{\wrD,\wfaD,\acD,\cfaD,\me,\mfaD,\mexD,\fequ}}{}{B}{
\vlhy{A}}}
\end{equation*}

Immediately from Lemmas <ref> and <ref>.

Observe that Lemma <ref> would also hold with the rules $\wfaD$ and $\cfaD$ removed.

§.§ Rule Permutations

Let $\Gamma$ be a sequent. If $\sqn\Gamma$ is provable in $\FOLK$ (as depicted on the left below) then there is a sequent
$\Gamma'$ not containing any $\fff$, such that there is a derivation as shown on the right below:-2ex

\begin{equation*}
\vlderivation{
\vltrl{}{\FOLK}{\Deri}{\sqns{\Gamma}}{
\vlhy{\quad}}{
\vlhy{}}{
\vlhy{}}}
\qquad
\Longrightarrow
\qquad
\vlderivation{
\vlde{\set{\wrD,\cD,\fequ}}{\Deri_2}{\sqns{\form{\Gamma}}}{
\vltrl{}{\FOMLL}{\Deri_1}{\sqns{\form{\Gamma'}}}{
\vlhy{\quad}}{
\vlhy{}}{
\vlhy{}}}}
\end{equation*}

First, we can replace every instance of the $\fff$-rule in $\Deri$ by
$\weakr$. Then the instances of $\weakr$ and $\conr$ are replaced by
$\wD$ and $\cD$, which can then be permuted down.
Details are in
Appendix <ref>.

For every derivation
\vlde{\FOMLS}{}{A}{
\vlhy{\ttt}}}$
there are formulas $A'$ and $A''$ such that

\begin{equation*}\hspace{-2ex}
\vlderivation{
\vlde{\set{\exists}}{}{A}{
\vlde{\set{\sw,\mix,\fequ}}{}{A'}{
\vlde{\set{\forall,\aiD,\tttD}}{}{A''}{
\vlhy{\ttt}}}}}
\end{equation*}

First, observe that the $\exists$ rule can be permuted under all the
other rules since $A\ssubst{x}{t}$ has the same structure as $A$ and
none of the other rules has a premise of the form $\Scons{\exists
x.A}$. It suffices now to prove that all rules in $\set{\forall,
\aiD, \tttD}$ can be permuted over the rules in $\set{\sw, \mix,
\fequ}$, which is straightforward. For $\sw$, $\mix$, and the $\fequ$-instances that
do not involve the quantifiers, the details can be found
in [38]. The $\fequ$-instances concerning the
quantifiers are admissible if the $\exists$-rule is not present.

For every derivation
\vlde{\set{\wrD,\wfaD,\acD,\cfaD,\me,\mfaD,\mexD,\fequ}}{}{B}{
\vlhy{A}}}$
there are formulas $A'$ and $B'$ such that

\begin{equation*}\hspace{-3ex}
\vlderivation{
\vlde{\set{\wrD,\wfaD,\fequ}}{}{B}{
\vlde{\set{\acD,\cfaD}}{}{B'}{
\vlde{\set{\me,\mfaD,\mexD,\fequ}}{}{A'}{
\vlhy{A}}}}}
\end{equation*}

Permute all $\wD$ and $\wfaD$ instances to the bottom of
the derivation, then permute all $\cD$ and
$\cfaD$ below $\set{\me,\mfaD,\mexD}$. 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 <ref>.
Lemma is the reason for the presence of the rules $\wfaD$ and
$\cfaD$, as without them the permutation cases in (<ref>)
could not be resolved.

We can now complete the proof of Theorems <ref> and <ref>.

Assume we have a proof of $A$ in $\FOKS$. By
Theorem <ref> we have a proof of $\sqn A$ in $\FOLK$ to
which we can apply Theorem <ref>. Finally, we
apply Lemma <ref> to get the desired shape.

Assume we have a proof of $A$ in $\FOKS$. We first apply
Theorem <ref>, and then
Lemma <ref> to the upper half and
Lemmas <ref> and <ref> to the lower half.

§ FONETS AND LINEAR PROOFS

§.§ From $\FOMLL$ Proofs to Fonets

Let $\Pi$ be a $\FOMLL$ proof of a rectified sequent $\sqn\Gamma$ not containing $\fff$. We now show
how $\Pi$ is translated into a linked fograph
$\fographof\Pi=\tuple{\graphof\Gamma,\linkingof\Pi}$. We proceed
inductively, making a case analysis on the last rule in $\Pi$. At the
same time we are constructing a dualizer $\dsubstof\Pi$, so that in the
end we can conclude that $\fographof\Pi$ is in fact a fonet.

* $\Pi$ is $\upsmash{\vlinf{\axr}{}{\sqn{a,\cneg a}}{}}$ : Then the only
link is $\set{a, \dual{a}}$, and $\dsubstof\Pi$ is empty.

* $\Pi$ is $\smash{\vlinf{\ttt}{}{\sqn{\ttt}}{}}$ : Then
$\linkingof\Pi$ and $\dsubstof\Pi$ are both empty.

* The last rule in $\Pi$ is $\vliinf{\mixr}{}{\sqn{\Gamma',\Gamma''}}{\sqn\Gamma'}{\sqn\Gamma''}$ :
By induction hypothesis, we have proofs $\Pi'$ and $\Pi''$ of $\Gamma'$ and $\Gamma''$, respectively. We have
$\graphof{\Gamma}=\graphof{\Gamma'}+\graphof{\Gamma''}$ and we can let
$\linkingof\Pi\;=\;\linkingof{\Pi'}\cup\linkingof{\Pi''}$ and

* The last rule in $\Pi$ is $\vlinf{\vlor}{}{\sqn{\Gamma_1,A\vlor
B}}{\sqn{\Gamma_1,A,B}}$ : By induction hypothesis, there is
a proof $\Pi'$ of $\Gamma'={\Gamma_1,A,B}$. We have
$\graphof{\Gamma}=\graphof{\Gamma'}$ and let
$\linkingof\Pi\;=\;\linkingof{\Pi'}$ and

* The last rule in $\Pi$ is $\vliinf{\vlan}{}{\sqn{\Gamma_1,A\vlan
B, \Gamma_2}}{\sqn{\Gamma_1,A}}{\sqn{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 $\graphof{\Gamma}=\graphof{\Gamma_1}+\mbox{$(\graphof A\times\graphof
B)$}+\graphof{\Gamma_2}$ and we let
$\linkingof\Pi\;=\;\linkingof{\Pi'}\cup\linkingof{\Pi''}$ and

* The last rule in $\Pi$ is
$\vlinf{\exists}{}{\sqn{\Gamma_1,\exists x.A}}
{\sqn{\Gamma_1,A\ssubst{x}{t}}}$ : By induction hypothesis, there is
a proof $\Pi'$ of $\Gamma'={\Gamma_1,A\ssubst{x}{t}}$.  For each atom in
$\Gamma'=\Gamma_1, A \ssubst{x}{t}$, there is a corresponding atom
in $\Gamma=\Gamma_1, \exists x.A$. We can therefore define the
linking $\linkingof{\Pi}$ from the linking $\linkingof{\Pi'}$ via
this correspondence. Then, we let $\dsubstof\Pi$ be
$\dsubstof{\Pi'}+\ssubst{x}{t}$. Since $\Gamma$ is rectified $x$
does not yet occur in $\dsubstof{\Pi'}$. Hence $\dsubstof\Pi$ is a
dualizer of $\fographof\Pi$.

* The last rule in $\Pi$ is $\vlinf{\forall}{\text{($x$ not free
in $\Gamma_1$)}}{\sqn{\Gamma_1,\forall x.A}}{\sqn{\Gamma_1,A}}$ :
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
$\linkingof\Pi\;=\;\linkingof{\Pi'}$ and

If $\Pi$ is a $\FOMLL$ proof of a rectified $\fff$-free sequent $\sqn\Gamma$,
then $\fographof\Pi$ is a fonet and $\dsubstof\Pi$ a dualizer for it.

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
$\graphof{\Gamma'}$ to the new $x$-binder $\single x$ in
$\graphof{\Gamma}$. However, observe that this $\single x$ vertex is
not connected to any vertex in $\graphof{\Gamma'}$, and hence no
such new dependency can be extended to a bimatching. That
$\dsubstof\Pi$ is a dualizer for $\fographof\Pi$ follows immediately
from the construction. Hence,  $\fographof\Pi$ is a fonet.

§.§ From $\FOMLS$ Proofs to Fonets

There is a more direct path from a $\FOMLL$ proof $\Pi$ of a rectified
sequent $\Gamma$ to the linked fograph $\fographof\Pi$: take
the fograph $\graphof\Gamma$, and let the equivalence classes of
$\linkingof\Pi$ be all the atom pairs that meet in an instance of
$\ax$, and $\dsubstof\Pi$ comprises the substitutions
at the $\exists$-rules in $\Pi$.

We chose the more cumbersome path above because it gives us a
direct proof of Theorem <ref>.

However, for translating $\FOMLS$ derivation into fonets, we employ
exactly that direct path.

In a derivation in $\FOMLS$
where the conclusion is rectified, every line is also rectified, as
the only rules involving bound variables are $\forall$ and $\exists$
which (upwards) both remove a binder.
Therefore, we can call such a derivation rectified, and
for a non-rectified  $\FOMLS$ derivation $\Deri$ we can
define its rectification $\rectif\Deri$ inductively, by rectifying each
line, proceeding step-wise
from conclusion to premise.[As for formulas,
the rectification of a derivation is unique up to renaming of bound

A rectified derivation $\vlder{\FOMLS}{\Deri}{A}{\ttt}$ determines a
substitution which maps the existential bound variables occurring in
$A$ to the terms substituted for them in the instances of the
$\exists$-rule in $\Phi$. We denote this substitution by
$\dsubstof\Phi$ and call it the dualizer of
$\Deri$. Furthermore, every atom occurring in the conclusion $A$ must
be consumed by a unique instance of the rule $\aiD$ in $\Deri$. This
allows us to define a (partial) equivalence relation $\linkingof\Deri$
on the atom occurrences in $A$ by $a\linkingof\Deri b$ if $a$ and $b$
are consumed by the same instance of $\aiD$ in $\Deri$. We call
$\linkingof\Deri$ the linking of $\Deri$, and define

Let $\vlder{\FOMLS}{\Deri}{A}{\ttt}$ be a rectified derivation where $A$ is $\fff$-free. Then
$\fographof\Deri$ is a fonet and $\dsubstof{\Deri}$ a dualizer for it.

To prove this theorem, we have to show that no inference rule in
$\FOMLS$ can introduce a bimatching. To simplify the argument, we
introduce the frame [39] of the linked fograph $\gC$,
which is a linked (propositional) cograph in which the dependencies
between the binders in $\gC$ are encoded as links.

More formally, let $C$ be a formula with $\graphof C=\gC$, to which we
exhaustively apply the following
subformula rewriting steps, to obtain a sequent $\frameof C$:

* Encode dependencies as fresh links. For each dependency
$\set{\single {x_i},\single {y_j}}$ in $\gC$, with corresponding
subformulas $\exists x_i. A$ and $\forall y_j. B$ in $C$, we pick a
fresh (nullary) predicate symbol $q_{i,j}$, and then replace $\exists
x_i. A$ by $\dual q_{i,j} \cand \exists x_i. A$, and replace $\forall y_j. B$ by
$q_{i,j} \cor \forall y_j. B$.

* Erase quantifiers. After step 1, remove all the
quantifiers, i.e., replace $\exists x_i.A$ by $A$ and replace $\forall
y_j.B$ by $B$ everywhere.

* Simplify atoms. After step 2, replace every predicate
$pt_1 \ldots t_n$ (resp. $\dual{p}t_1 \ldots t_n$) with a nullary
predicate symbol $p$ (resp. $\dual p$)

Then $\linkingof{\frameof C}$ consists of the pairs induced by
$\linkingof\gC$ and the new pairs $\set{q_{i,j},\dual q_{i,j}}$ introduced in
step 1 above.
We call $\frameof C$ the frame of $C$ and we define the frame of $\gC$, denoted
$\frameof\gC$, as
$\tuple{\graphof{\frameof C},\linkingof{\frameof C}}$.

If a linked fograph $\gC$ has an induced bimatching then so does its frame $\frameof\gC$.

Immediately from the construction of the frame.

From $\Deri$ we construct a derivation $\frameof\Deri$ of $\frameof
A$ in the propositional fragment of $\FOMLS$, such that
$\fographof{\frameof\Deri}=\frameof{\fographof\Deri}$.  The
rules $\aiD,\tttD,\mix$ and $\sw$ are translated trivially, and for
$\fequ$, it suffices to observe that the frame construction is
invariant under $\fequ$. Finally, for the rules $\forall$ and
$\exists$, proceed as follows. Every instance of $\forall$ is
replaced by the derivation on the right below:[For better
readability we omit superfluous parentheses, knowing that we always
have $\fequ$ incorporating associativity and commutativity of
$\vlan$ and $\vlor$.] -4ex

\begin{equation*}
\scalebox{.95}{$
\vlinf{\forall}{}{\Scons{\forall y_j.\ttt}}{\Scons{\ttt}}
\;\leadsto
\vlderivation{
\vlde{\set{\sw,\fequ}}{\DDeri_2}{\Scons{q_{h_1,j}\vlor\cdots\vlor
q_{h_n,j}\vlor(\dual q_{h_1,j}\vlan\cdots\vlan\dual
\vlde{\set{\aiD,\tttD}}{\DDeri_1}{
\Scons{(q_{h_1,j}\vlor \dual q_{h_1,j})\vlan\cdots\vlan(q_{h_n,j}\vlor \dual q_{h_n,j})\vlan\ttt}}{
\vlhy{\ttt}}}}
\end{equation*}

where $h_1,\ldots,h_n$ range over the indices of the existential
binders dependent on that $y_j$. It is easy to see how $\DDeri_1$ is
constructed. The construction of $\DDeri_2$, using $\sw$ and $\fequ$, is standard, see,
e.g. [40, 37, 41, 38]. Then, every
occurrence of $\forall y_j.F$ is replaced by
$q_{h_1,j}\vlor\cdots\vlor q_{h_n,j}\vlor (\dual
q_{h_1,j}\vlan\cdots\vlan\dual q_{h_n,j}\vlan F)$ in the derivation
below that $\forall$-instance. Now, observe that all instances of
the $\exists$-rule introducing $x_i$ dependent on $y_j$ must occur
below in the derivation (otherwise $\Deri$ would not be rectified).
Now consider such an instance $\vlinf{\exists}{}{\Scons{\exists
x_i.B}}{\Scons{B\ssubst {x_i} t}}$.  Its context $\Sconhole$
must contain all the $\forall y_j$ the $\exists x_i$ depends on,
such that $B$ is in their scope. Following the translation of the
$\forall$ rules above, we can therefore translate the $\exists$-rule
instance by the following derivation

\begin{equation*}
\vlder{\set{\sw,\fequ}}{\DDeri_3}{ S_0\cons{S_1\cons{\cdots
S_{l-1}\cons{S_{l}\cons{\dual q_{i,k_1}\vlan\dual
q_{i,k_2}\vlan\cdots q_{i,k_l}\vlan B'}}\cdots}}}{
S_0\cons{\dual q_{i,k_1}\vlan S_1\cons{\dual
q_{i,k_2}\vlan\cdots S_{l-1}\cons{\dual q_{i,k_l}\vlan
\end{equation*}

where $k_1,\ldots,k_l$ are the indices of the universal binders
on which that $x_i$ depends, and $B'$ is $B$ in which all predicates
are replaced by a nullary one (step 3 in the frame construction). The
derivation $\DDeri_3$ can be constructed in the same way as

Doing this to all instances of the rules $\forall$ and $\exists$ in
$\Deri$ yields indeed a propositional derivation $\frameof\Deri$
$\fographof{\frameof\Deri}=\frameof{\fographof\Deri}$. It has
been shown by Retoré [42] and
rediscovered by Straßburger [38] that
C},\linkingof{\frameof\Deri}}$ cannot contain an induced
bimatching. By Lemma <ref>, $\fographof{\Deri}$ does not
have an induced bimatching either. Furthermore, it follows from the
definition of $\dsubstof\Deri$ that it is a dualizer for

There is an alternative path of proving Theorem <ref>
by translating $\Deri$ to an $\FOMLL$-proof $\Pi$, observing that
this process preserves the linking and the dualizer. However, for
this, we have to extend the construction from the previous subsection to the $\cut$-rule,
and then show that linking and dualizer of a sequent proof $\Pi$ are
invariant under cut elimination. This can be done similarly to
unification nets in [39].

§.§ From Fonets to $\FOMLL$ Proofs

Now we are going to show how from a given fonet
$\tuple{\gC,\linkingof\gC}$ we can construct a sequent proof $\Pi$ in
$\FOMLL$ such that $\fographof\Pi=\tuple{\gC,\linkingof\gC}$. In the
proof net literature, this operation is also called
sequentialization. The basic idea behind our sequentialization
is to use the frame of $\gC$, to which  we can apply the splitting tensor
theorem, and then reconstruct the sequent proof $\Pi$.

Let $\Gamma$ be a propositional sequent and $\linkingof\Gamma$ be a
linking for $\graphof\Gamma$. A conjunction formula $A\vlan B$ is
splitting or a splitting tensor if
$\Gamma=\Gamma',A\vlan B,\Gamma''$ and
$\mathord{\linkingof\Gamma}=\mathord{\linking_1}\cup\linking_2$, such
that $\linking_1$ is a linking for $\graphof{\Gamma',A}$ and
$\linking_2$ is a linking for $\graphof{B,\Gamma''}$, i.e., removing
the $\vlan$ from $A\vlan B$ splits the linked fograph $\tuple{
\graphof\Gamma,\linkingof\Gamma}$ into two fographs.
We say that $\tuple{
\graphof\Gamma,\linkingof\Gamma}$ is mixed iff
$\Gamma=\Gamma',\Gamma''$ and
$\mathord{\linkingof\Gamma}=\mathord{\linking_1}\cup\linking_2$, such
that $\linking_1$ is a linking for $\graphof{\Gamma'}$ and
$\linking_2$ is a linking for $\graphof{\Gamma''}$.
Finally, $\tuple{
\graphof\Gamma,\linkingof\Gamma}$ is splittable if it is mixed or has a splitting tensor.

Let $\Gamma$ be a $\fff$-free propositional sequent containing only atoms
and $\vlan$-formulas, and $\linkingof\Gamma$ be a
linking for $\graphof\Gamma$. If $\tuple{
\graphof\Gamma,\linkingof\Gamma}$ 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:

Let $\tuple{\gC,\linkingof\gC}$ be a fonet, and let $\Gamma$ be a sequent with $\graphof\Gamma=\gC$. Then there is an
$\FOMLL$-proof $\Pi$ of $\Gamma$, such that

Let $\dsubstof\gC$ be the dualizer of $\tuple{\gC,\linkingof\gC}$.  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 $\vlor$-root, or a formula $\forall x.A$, we can
immediately apply the $\vlor$-rule or the $\forall$-rule of $\FOMLL$
and proceed by induction hypothesis. If $\Gamma$ contains a formula
$\exists x.A$ such that the corresponding binder $\single x$ in $\gC$
has no dependency, then we can apply the $\exists$-rule, choosing the
term $t$ as determined by $\dsubstof\gC$, and proceed by induction
hypothesis.  Hence, we can now assume that $\Gamma$ contains only
atoms, $\vlan$-formulas, or formulas of shape $\exists x.A$, where
the vertex $\single x$ has dependencies. Then the frame
$\tuple{\graphof{\frameof\Gamma},\linkingof{\frameof\Gamma}}$ does
not induce a bimatching and contains only atoms and
$\vlan$-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 $\vlan$ is already in
$\Gamma$, then we can apply the $\vlan$-rule and proceed by
induction hypothesis on the two branches. However, if
$\frameof\Gamma$ is not mixed and all splitting tensors are
$\vlan$-formulas introduced in step 1 of the frame construction,
then we get a contradiction as in that case there must be a $\vlor$- or $\forall$-formula in $\Gamma$.

§.§ From Fonets to $\FOMLS$ Proofs

We can now straightforwardly obtain the same result for $\FOMLS$:

Let $\tuple{\gC,\linkingof\gC}$ be a fonet, and let $C$ be a formula with $\graphof C=\gC$. Then there is
a derivation $\vlder{\FOMLS}{\Deri}{C}{\ttt}$ such that $\fographof\Deri=\tuple{\gC,\linkingof\gC}$.

We apply Theorem <ref> to obtain a sequent
proof $\Pi$ of $\sqn C$ with
$\fographof\Pi=\tuple{\gC,\linkingof\gC}$. Then we apply
Lemma <ref>, observing that the translation from
$\FOMLL$ to $\FOMLS$ preserves linking and dualizer.

Note that it is also possible to do a direct “sequentialization”
into the deep inference system $\FOMLS$, using the techniques
presented in [38] and [46].

§ SKEW BIFIBRATIONS AND RESOURCE MANAGEMENT

In this section we establish the relation between skew bifibrations and derivations in
$\set{\wrD,\wfaD,\acD,\cfaD,\me,\mfaD,\mexD,\fequ}$. However,
if a derivation $\Deri$ contains instances of the rules $\cfaD$, $\mfaD$, and
$\mexD$ we can no longer naively define the rectification
$\rectif\Deri$ as in the previous section for $\FOMLS$, as these two
rules cannot be applied if premise and conclusion are rectified. For
this reason we define here rectified versions $\rectif\cfaD$,  $\rectif\mfaD$ and
$\rectif\mexD$, shown below:-1ex

\begin{equation*}
\scalebox{1}{$
\vlinf{\rectif\cfaD}{}{\Scons{\forall x.Ax}}{\Scons{\forall y.\forall x.Ax}}
\hskip3em
\begin{array}{c}
\vlinf{\rectif\mfaD}{}{\Scons{\forall x.(Ax\vlor Bx)}}{\Scons{(\forall y.Ay)\vlor(\forall z.Bz)}}
\\ \\[-1ex]
\vlinf{\rectif\mexD}{}{\Scons{\exists x.(Ax\vlor Bx)}}{\Scons{(\exists y.Ay)\vlor(\exists z.Bz)}}
\end{array}
\end{equation*}

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 $\Sconhole$.

Note that in an instance of $\rectif\mfaD$ or $\rectif\mexD$ (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 $\mfaD$ and
$\mexD$ as special cases of $\rectif\mfaD$ and $\rectif\mexD$, respectively. And similarly,  if $x=y$ then $\cfaD$
is a special case of $\rectif\cfaD$.

For a derivation $\Deri$ in
$\set{\wrD,\wfaD,\acD,\cfaD,\me,\mfaD,\mexD,\fequ}$, we can now construct the
rectification $\rectif\Deri$ by rectifying each line of $\Deri$, yielding
a derivation in

For each instance $\vlinf{\rr}{}{P}{Q}$ of an inference rule in
$\set{\wrD,\wfaD,\acD,\rectif\cfaD,\me,\rectif\mfaD,\rectif\mexD,\fequ}$ we can
define the induced map $\mapof{\rr}\colon\vgraphof
Q\to\vgraphof P$ which acts as the identity for
$\rr\in\set{\me,\fequ}$ and as the canonical injection for
$\rr\in\set{\wrD,\wfaD}$. For $\rr=\acD$ it maps the vertices
corresponding to the two atoms in the premise to the vertex of the
contracted atom in the conclusion, and for
$\rr\in\set{\rectif\cfaD,\rectif\mfaD,\rectif\mexD}$ 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 $\Deri$ in
$\set{\wrD,\wfaD,\acD,\rectif\cfaD,\me,\rectif\mfaD,\rectif\mexD,\fequ}$ we can then define
the induced map $\mapof\Deri$ as the composition of the induced
maps of the rule instances in $\Deri$.

Let $\downsmash{\vlderivation{
\vlde{\set{\wrD,\wfaD,\acD,\cfaD,\me,\mfaD,\mexD,\fequ}}{\Deri}{B}{
\vlhy{A}}}}$ be given.

Then there is a rectified derivation
\vlde{\set{\wrD,\wfaD,\acD,\rectif\cfaD,\me,\rectif\mfaD,\rectif\mexD,\fequ}}{\rectif\Deri}{\rectif
B}{ \vlhy{\rectif A}}}$, such that the induced maps
$\mapof\Deri\colon\graphof{A}\to\graphof{B}$ and
$\mapof{\rectif\Deri}\colon\graphof{\rectif A}\to\graphof{\rectif
B}$ are equal up to a variable renaming of the vertex labels.

Immediate from the definition.

§.§ From Contraction and Weakening to Skew Bifibrations

Let $\vlderivation{
\vlde{\set{\wrD,\wfaD,\acD,\rectif\cfaD,\me,\rectif\mfaD,\rectif\mexD,\fequ}}{\Deri}{B}{
\vlhy{A}}}$ be a rectified derivation. Then the induced map
$\mapof\Deri\colon\graphof{A}\to\graphof{B}$ is a skew bifibration.

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

\begin{equation*}
\begin{array}{r@{\;=\;}l}
\PE{a} & a\\
\PE{(A \cor B)} &  \PE{A} \cor \PE{B} \\
\PE{(A \cand B)} & \PE{A} \cand \PE{B}
\end{array}
\qquad
\begin{array}{r@{\;=\;}l}
\PE{(\forall x A)} & x \cor \PE{A}\\
\PE{(\exists x A)} & x \cand \PE{A}
\end{array}
\end{equation*}

For every formula $A$, we have $\graphof{\PE A}=\graphof{A}$.

A straightforward induction on $A$.

We use $\PE\fequ$ to denote the restriction of $\fequ$ to
propositional formulas, i.e., the first two lines in (<ref>).

First, observe that for every inference rule
the induced map $\mapof{\rr}\colon\vgraphof Q\to\vgraphof P$ defines
an existential-preserving graph homomorphism $\graphof Q\to\graphof
P$ and a fibration on the corresponding binding graphs.  Therefore,
their composition $\mapof\Deri$ has the same properties of fibration.

For showing that it is also a skew fibration, we construct for
$\Deri$ its propositional encoding $\PE\Deri$ by
translating every line into its propositional encoding.
The instances
of the rules $\rectif\mfaD$ and $\rectif\mexD$ are replaced by:

\begin{equation*}
\scalebox{.85}{$
\vlderivation{
\vlin{\rectif\acD}{}{\Scons{x\vlor(\PE{(Ax)}\vlor\PE{(Bx)})}}{
\vlin{\fequ}{}{\Scons{(y\vlor z)\vlor(\PE{(Ay)}\vlor\PE{(Bz)})}}{
\vlhy{\Scons{(y\vlor\PE{(Ay)})\vlor (z\vlor\PE{(Bz)})}}}}}
\qquad\!
\vlderivation{
\vlin{\rectif\acD}{}{\Scons{x\vlan(\PE{(Ax)}\vlor\PE{(Bx)})}}{
\vlin{\me}{}{\Scons{(y\vlor z)\vlan(\PE{(Ay)}\vlor\PE{(Bz)})}}{
\vlhy{\Scons{(y\vlan\PE{(Ay)})\vlor (z\vlan\PE{(Bz)})}}}}}
\end{equation*}

respectively, where $\rectif\acD$ is a $\acD$ 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 $\wD$, $\acD$, $\me$, or
$\fequ$ is translated to an instance of the same rule,
$\rectif\cfaD$ is translated to $\rectif\acD$, and $\wfaD$ is
translated to $\wD$.

This gives us a derivation $\vlderivation{
\vlde{\set{\wrD,\acD,\rectif\acD,\me,\PE\fequ}}{\PE\Deri}{\PE B}{
\vlhy{\PE A}}}$ such that $\mapof{\PE\Deri}=\mapof\Deri$. It has
been shown in [23] that $\mapof{\PE\Deri}$ is a skew
$\mapof\Deri$ is a skew fibration.

§.§ From Skew Bifibrations to Contraction and Weakening

Let $\gA$ and $\gB$ be fographs, let $\phi\colon\gA\to\gB$ be a skew
bifibration, and let $A$ and $B$ be formulas with $\graphof A=\gA$
and $\graphof B=\gB$. Then there are derivations

\begin{equation*}
\vlderivation{
\vlde{\set{\wrD,\wfaD,\acD,\rectif\cfaD,\me,\rectif\mfaD,\rectif\mexD,\fequ}}{\rectif\Deri}{B}{
\vlhy{A}}}
\quand
\vlderivation{
\vlde{\set{\wrD,\wfaD,\acD,\cfaD,\me,\mfaD,\mexD,\fequ}}{\Deri}{B}{
\vlhy{A\rsubstof\phi}}}
\end{equation*}

such that $\mapof{\rectif\Deri}=\phi$ and $\rectif{\Deri}$ is a
rectification of $\Deri$, and $\rsubstof\phi$ is the substitution
induced by $\phi$.

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

We say a fograph homomorphism $\phi\colon\gG\to\gH$ is full if
for all $v,w\in\vG$, we have that $\phi(v)\phi(w)\in\eH$ implies

Let $\phi\colon\gG\to\gH$ be full and injective skew bifibration
such that $\rsubstof\phi$ is the identity substitution, and let $G$
and $H$ be formulas with $\graphof G=\gG$ and $\graphof H=\gH$. Then
there is a derivation $\vlder{\set{\wrD,\wfaD,\fequ}}{\Deri}{H}{G}$.

By <cit.>, we have a derivation
$\vlder{\set{\wrD,\PE\fequ}}{\DDeri}{\PE H}{\PE G}$. In order to
lift $\DDeri$, we need to reorganize the instances of
$\wD$. If $H$ contains a subformula $\forall x.A$ which is not
present in $G$, the $\wD$-instances in $\DDeri$ could introduce the
parts of the propositional encoding $x\vlor A$ independently.  We
say that an instance $\rr_1$ of $\wD$ in $\Deri$ is in the
scope of an instance $\rr_2$ of $\wD$ if $\rr_1$ introduced
formulas that contain a free variable $x$ (i.e., $x$ occurs in a
term in a predicate) and $\rr_2$ introduces the atom $x$ as a
subformula (i.e. the propositional encoding of the binder $x$).  We
can now permute the $\wD$-instances in $\DDeri$ such that whenever
a rule instance $\rr_1$ is in the scope of an instance $\rr_2$, then
$\rr_2$ occurs below $\rr_1$ in $\DDeri$.
Then we can lift $\DDeri$ stepwise. First, observe that each line of
$\DDeri$ is $\PE\fequ$-equivalent to the propositional encoding $\PE P$ of a
first-order formula $P$.  We now have to show
that each instance of $\wrD$ in $\DDeri$ is indeed the image of a correct
application of $\wD$ or $\wfaD$ in first-order logic.
If we have a $\wD$ of the form

\begin{equation*}
\scalebox{1}{$
\vlinf{\wD}{}{\PE S\cons{x\vlor \PE A}}{\PE S\cons{\PE A}}
\qquor
\vlinf{\wD}{}{\PE S\cons{(x\vlor \PE B)\vlor \PE A}}{\PE S\cons{\PE A}}
\end{equation*}

then $x$ cannot occur freely in $A$, as otherwise the fibration
property would be violated. We can therefore lift these instances to

\begin{equation*}
\scalebox{1}{$
\vlinf{\wfaD}{}{S\cons{\forall x. A}}{S\cons{A}}
\qquor
\vlinf{\wD}{}{S\cons{(\forall x. B)\vlor A}}{S\cons{A}}
\end{equation*}

If a  weakening happens inside a subformula $x\vlor \PE C$ or $x\vlan
\PE C$ in $\DDeri$, then there are the following cases:

\begin{equation*}%\small
\scalebox{.9}{$
\vlinf{\wD}{}{\PE S\cons{x\vlor\PE  D\vlor \PE C}}{\PE S\cons{x\vlor\PE  C}}
\quad
\vlinf{\wD}{}{\PE S\cons{x\vlan (\PE D\vlor \PE C)}}{\PE S\cons{x\vlan\PE  C}}
\quad
\vlinf{\wD}{}{\PE S\cons{(x\vlor\PE  D)\vlan \PE C}}{\PE S\cons{x\vlan \PE C}}
\end{equation*}

The first two cases can be lifted to

\begin{equation*}
\vlinf{\wD}{}{S\cons{\forall x.( D\vlor C)}}{S\cons{\forall x.  C}}
\quand
\vlinf{\wD}{}{S\cons{\exists x.( D\vlor C)}}{S\cons{\exists x.  C}}
\end{equation*}

respectively. But in the third case,  an $\exists$-quantifier would be
transformed into an $\forall$-quantifier. But as $\phi$ has to
preserve existentials, this third case cannot occur. All other situations can be lifted trivially, giving us
$\vlder{\set{\wrD,\wfaD,\fequ}}{\Deri}{H}{G}$ as desired.

Let $\phi\colon\gG\to\gH$ be a surjective skew
bifibration, and let $G$ and $H$ be formulas with $\graphof G=\gG$
and $\graphof H=\gH$. Then there is a derivation

\begin{equation*}
\vlderivation{
\vlde{\set{\acD,\cfaD,\me,\mfaD,\mexD,\fequ}}{\Deri}{H}{
\vlhy{G\rsubstof\phi}}}
\end{equation*}

where  $\rsubstof\phi$ is the substitution
induced by $\phi$.

By <cit.>, there is a derivation
H}{\PE{(G\substof\phi)}}$.  We can lift $\DDeri$ to a first-order
derivation in $\set{\acD,\cfaD,\me,\mfaD,\mexD,\fequ}$, in a similar
way as in the previous lemma.
The technical details are in
Appendix <ref>.

Let $\vB'\subseteq\vB$ be the image of $\phi$, and let $\gB_1$ be
the subgraph of $\gB$ induced by $\vB'$. Hence, we have two maps
$\phi''\colon\gA\to\gB_1$ being a surjection and $\phi'\colon
\gB_1\to\gB$ being a full injection.  Both, $\phi'$ and $\phi''$
remain skew bifibrations.  Furthermore, $\gB_1$ is also a fograph.
Let $B_1$ be a formula with $\graphof{B_1}=\gB_1$.
We can apply Lemmas <ref>
and <ref> to obtain derivations

\begin{equation*}
\vlder{\set{\wrD,\wfaD,\fequ}}{\Deri'}{B}{B_1}
\qquand
\vlder{\set{\acD,\cfaD,\me,\mfaD,\mexD,\fequ}}{\Deri''}{B_1}{
\end{equation*}

As $\rsubstof{\phi'}$ is the identity, we have
$\rsubstof{\phi''}=\rsubstof{\phi}$. Hence, the composition of
$\Deri''$ and $\Deri'$ is the desired derivation $\Deri$.  Then
$\rectif\Deri$ can be constructed by rectifying $\Deri$, where the
variables to be used in $A$ are already given. That
$\phi=\mapof{\rectif\Deri}$ follows immediately from the

§ SUMMARY AND PROOF OF MAIN RESULT

The only theorem of Section <ref> that has not yet been
proved is Theorem <ref> establishing the full correspondence
between decomposed proofs in $\FOKS$ and combinatorial proofs. We show
the proof here, by summarizing the results of the previous two
Sections <ref> and <ref>.

First, assume we have a combinatorial proof $\phi\colon\gC\to\gA$
and a formula $A$ with $\gA=\graphof A$.
Let $C$ be a formula with $\graphof C=\gC$, and let $\rsubstof\phi$
be the substitution induced by $\phi$.
By Lemma <ref> there is a derivation

\begin{equation*}
\vlder{\set{\wrD,\wfaD,\acD,\cfaD,\me,\mfaD,\mexD,\fequ}}{\Deri_2}{A}{C\rsubstof\phi}
\end{equation*}

Since $\gC$ is a fonet, we have by Theorem <ref> a derivation

\begin{equation*}
\vlder{\FOMLS}{\Deri'_1}{C}{\ttt}
\end{equation*}

This derivation remains valid if we apply the substitution
$\rsubstof\phi$ to every line in $\Deri'_1$, yielding the derivation
$\Deri_1$ of $C\rsubstof\phi$ as desired.

Conversely, assume we have a decomposed derivation

\begin{equation}
\label{eq:decomx}
\vlderivation{
\vlde{\set{\wrD,\wfaD,\acD,\cfaD,\me,\mfaD,\mexD,\fequ}}{\Deri_2}{A}{
\vlde{\FOMLS}{\Deri_1}{A'}{
\vlhy{\ttt}}}}
\end{equation}

Then we can transform $\Deri_1$ into a rectified form
$\rectif\Deri_1$, proving $\rectif A'$. By
Theorem <ref>, the linked fograph
A'},\linkingof{\rectif\Deri_1}}$ is a fonet.  Then, by
Lemma <ref>, there is a rectified derivation
\vlde{\set{\wrD,\wfaD,\acD,\rectif\cfaD,\me,\rectif\mfaD,\rectif\mexD,\fequ}}{\rectif{\Deri_2}}{\rectif
A}{ \vlhy{\rectif{A'}}}}$ whose induced map
A}$ is the same as the induced map
$\mapof{\Deri_2}\colon\graphof{A'}\to\graphof{A}$ of $\Deri_2$. By
Lemma <ref>, this map is a skew bifibration. Hence, we
have a combinatorial proof $\phi\colon\gC\to\graphof{A}$ with

Note that Theorem <ref> shows at the same time soundness, completeness, and full completeness, as

* every proof in $\FOKS$ can be translated into a combinatorial proof, and

* every combinatorial proof is the image of a $\FOKS$-proof under that translation.

§ CONCLUSION

We uncovered a close correspondence between
first-order combinatorial proofs and decomposed deep inference
derivations of system $\FOKS$, and showed that every proof in
$\FOKS$ has such a decomposed form.

The most surprising discovery for us was that all technical
difficulties in our work could be reduced (in a non-trivial way) to
the propositional setting.

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

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

[1]
G. Frege, Begriffsschrift.1em plus 0.5em minus 0.4emLouis
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.1em plus 0.5em minus
0.4emBerlin: 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).1em plus 0.5em minus 0.4emSchloss
Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017.

[13]
L. Straßburger, “Combinatorial Flows and Proof Compression,”
Inria Saclay, Research Report RR-9048, 2017. [Online]. Available:

[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.1em plus
0.5em minus 0.4emSpringer, 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.1em plus 0.5em minus 0.4emSpringer, 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.1em plus 0.5em minus
0.4emSpringer, 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).1em plus 0.5em minus 0.4emIEEE,
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.1em plus 0.5em minus 0.4emSpringer, 2007, pp.

[24]
A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory.1em
plus 0.5em minus 0.4emCambridge University Press, 2000, no. 43.

[25]
J.-Y. Girard, “Quantifiers in Linear Logic,” Temi e prospettive
della logica e della filosofia della scienza comtemporanee, 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.1em plus 0.5em minus 0.4emSociété mathématique de France, 1960.

[31]
J. W. Gray, “Fibred and cofibred categories,” in Proc. Conf. on
Categorical Algebra '65.1em plus 0.5em minus 0.4emSpringer,
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.1em plus 0.5em
minus 0.4emMarcel 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.1em plus 0.5em minus
0.4emSpringer-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:

[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.1em plus 0.5em minus 0.4emSpringer,
2001, pp. 347–361.

[42]
C. Retoré, “Pomset Logic as a Calculus of Directed Cographs,”
INRIA, Research Report RR-3714, 1999. [Online]. Available:

[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.1em plus 0.5em minus
0.4emSpringer, 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.

§.§ Proof of Theorem <ref>

Write $\fv(A)$ for the set of variables which occur free in $A$.

Note that the instances of $\wrD,\cD$ in $\Deri_2$ are deep, but inside sequent contexts.

First, if an instance of $\vlinf{\weakr}{}{\sqn{\Gamma,A}}{\sqn{\Gamma}}$
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{equation*}
\vlderivation{
\vliin{\vlan}{}{\sqns{\Gamma, A \vlan B, \Delta}}{
\vlin{\weakr}{}{\sqns{\Gamma, A}}{
\vlhy{\sqns{\Gamma}}}}{
\vlhy{\sqns{B, \Delta}}}}
\leadsto
\vlderivation{
\vlin{\weakr}{}{\sqns{\Gamma, A \vlan B, \Delta}}{
\vlin{\weakr}{}{\vlvdots}{
\vlhy{\sqns{\Gamma}}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\vlor}{}{\sqns{\Gamma, A \vlor B}}{
\vlin{\weakr}{}{\sqns{\Gamma, A, B}}{
\vlhy{\sqns{\Gamma, A}}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{\sqns{\Gamma, A \vlor B}}{
\vlhy{\sqns{\Gamma, A}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\exists}{}{\sqns{\Gamma, \exists x.A}}{
\vlin{\weakr}{}{\sqns{\Gamma, A\ssubst{x}{t}}}{
\vlhy{\sqns{\Gamma}}}}}
\leadsto
\vlderivation{
\vlin{\weakr}{}{\sqns{\Gamma, \exists x.A}}{
\vlhy{\sqns{\Gamma}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\forall}{}{\sqns{\Gamma, \forall x.A}}{
\vlin{\weakr}{}{\sqns{\Gamma, A}}{
\vlhy{\sqns{\Gamma}}}}}
\leadsto
\vlderivation{
\vlin{\weakr}{}{\sqns{\Gamma, \forall x.A}}{
\vlhy{\sqns{\Gamma}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\conr}{}{\sqns{\Gamma, A}}{
\vlin{\weakr}{}{\sqns{\Gamma, A, A}}{
\vlhy{\sqns{\Gamma, A}}}}}
\leadsto
\vlderivation{
\vlhy{\sqns{\Gamma, A}}}
\end{equation*}

Note that in the case of $\vlor$, we use the deep rule $\wrD$ which can be
permuted under all the rules. By using these rewriting rules, we can eventually get
a derivation with all the instances of $\weakr$ and $\wrD$ at the bottom. Now observe
that the instances of $\conr$ in $\Deri$ can be transformed using the following

\begin{equation*}
\vlderivation{
\vlin{\conr}{}{\sqns{\Gamma, A}}{
\vlhy{\sqns{\Gamma, A, A}}}}
\leadsto
\vlderivation{
\vlin{\cD}{}{\sqns{\Gamma, A}}{
\vlin{\vlor}{}{\sqns{\Gamma, A \vlor A}}{
\vlhy{\sqns{\Gamma, A, A}}}}}
\end{equation*}

Knowing that $\cD$ can be permuted under all the rules of $\FOMLL$, we
eventually obtain a derivation:

\begin{equation*}
\vlderivation{
\vlde{\set{\weakr, \wrD,\cD,\fequ}}{\Deri'_2}{\sqns{\Gamma}}{
\vltrl{}{\FOMLL}{\Deri'_1}{\sqns{\Gamma'}}{
\vlhy{\quad}}{
\vlhy{}}{
\vlhy{}}}}
\end{equation*}

Note that $\fequ$ is required here since the permutation of formulas is implicit
in $\FOMLL$.

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

\begin{equation*}
\vlderivation{
\vlin{\weakr}{}{\sqns{\Gamma, A}}{
\vlhy{\sqns{\Gamma}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{\sqns{\form{\Gamma} \vlor A}}{
\vlhy{\sqns{\form{\Gamma}}}}}
\end{equation*}
we obtain a derivation

\begin{equation*}
\vlderivation{
\vlde{\set{\wrD,\cD,\fequ}}{\Deri_2}{\sqns{\form{\Gamma}}}{
\vltrl{}{\FOMLL}{\Deri_1}{\sqns{\form{\Gamma'}}}{
\vlhy{\quad}}{
\vlhy{}}{
\vlhy{}}}}
\end{equation*}

where $\Deri_1$ can be obtained from $\Deri'_1$
by applying the $\vlor$ rule.

§.§ Rule permutation for the proof of Lemma <ref>

We construct a rewriting system based on rule permutation on derivations in $\set{\wrD, \wfaD, \acD,
\cfaD, \me, \mfaD, \mexD, \fequ}$ that allows us to reach a derivation of the

\begin{equation*}
\vlderivation{
\vlde{\set{\wrD,\wfaD,\fequ}}{}{B}{
\vlde{\set{\acD,\cfaD}}{}{B'}{
\vlde{\set{\me,\mfaD,\mexD,\fequ}}{}{A'}{
\vlhy{A}}}}}
\end{equation*}

from any derivation. Intuitively, we want to move all the instances of $\rr \in
\set{\wrD, \wfaD}$ downwards and all the instances of $\rr' \in \set{\me,
\mfaD, \mexD}$ 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-$\fequ$ rule instances separated by $\fequ$. Only non-trivial cases are
presented here:

* $\rr_1/\rr_2$, where $\rr_1 \in \set{\wrD, \wfaD}$ and $\rr_2 \in
\set{\acD, \cfaD, \me, \mfaD, \mexD}$:

\begin{equation*}
\vlderivation{
\vlin{\acD}{}{a}{
\vlin{\wrD}{}{a \vlor a}{
\vlhy{a}}}}
\leadsto
\vlderivation{
\vlhy{a}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\me}{}{(A \vlor B) \vlan (C \vlor D)}{
\vlin{\wrD}{}{(A \vlan C) \vlor (B \vlan D)}{
\vlhy{A \vlan C}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{(A \vlor B) \vlan (C \vlor D)}{
\vlin{\wrD}{}{(A \vlor B) \vlan C}{
\vlhy{A \vlan C}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\mfaD}{}{\forall x.(A \vlor B)}{
\vlin{\wrD}{}{(\forall x.A) \vlor (\forall x.B)}{
\vlhy{\forall x.A}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{\forall x.(A \vlor B)}{
\vlhy{\forall x.A}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\cfaD}{}{\forall x.A}{
\vlin{\wfaD}{}{\forall x.\forall x.A}{
\vlhy{\forall x.A}}}}
\leadsto
\vlderivation{
\vlhy{\forall x.A}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\mfaD}{}{\forall x.(A \vlor B)}{
\vlin{\wfaD}{}{(\forall x.A) \vlor (\forall x.B)}{
\vlhy{A \vlor (\forall x.B)}}}}
\leadsto
\vlderivation{
\vlin{\fequ}{}{\forall x.(A \vlor B)}{
\vlhy{A \vlor (\forall x.B)}}}
\end{equation*}

where in the last case, $x$ is not free in $A$.

* $\rr_1/\rr_2$, where $\rr_1 \in \set{\acD, \cfaD}$ and $\rr_2 \in
\set{\me, \mfaD, \mexD}$:

\begin{equation*}
\scalebox{.9}{$
\vlderivation{
\vlin{\mfaD}{}{\Scons{\forall x.(A \vlor B)}}{
\vlin{\cfaD}{}{\Scons{(\forall x.A) \vlor (\forall x.B)}}{
\vlhy{\Scons{(\forall x.\forall x.A) \vlor (\forall x.B)}}}}}
\leadsto
\vlderivation{
\vlin{\mfaD}{}{\Scons{\forall x.(A \vlor B)}}{
\vlin{\fequ}{}{\Scons{(\forall x.A) \vlor (\forall x.B)}}{
\vlin{\mfaD}{}{\Scons{\forall x.(\forall x.A \vlor B)}}{
\vlhy{\Scons{(\forall x.\forall x.A) \vlor (\forall x.B)}}}}}}$}
\end{equation*}

* $\cfaD/\fequ$:

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{\forall y.\forall x.A}{
\vlin{\cfaD}{}{\forall x.\forall y.A}{
\vlhy{\forall x.\forall x.\forall y.A}}}}
\leadsto
\vlderivation{
\vlin{\cfaD}{}{\forall y.\forall x.A}{
\vlin{\fequ}{}{\forall y.\forall x.\forall x.A}{
\vlhy{\forall x.\forall x.\forall y.A}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{(\forall x.A) \vlor B}{
\vlin{\cfaD}{}{\forall x.(A \vlor B)}{
\vlhy{\forall x.\forall x.(A \vlor B)}}}}
\leadsto
\vlderivation{
\vlin{\cfaD}{}{(\forall x.A) \vlor B}{
\vlin{\fequ}{}{(\forall x.\forall x. A) \vlor B}{
\vlhy{\forall x.\forall x.(A \vlor B)}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{\forall x.(A \vlor B)}{
\vlin{\cfaD}{}{(\forall x.A) \vlor B}{
\vlhy{(\forall x.\forall x.A) \vlor B}}}}
\leadsto
\vlderivation{
\vlin{\cfaD}{}{\forall x.(A \vlor B)}{
\vlin{\fequ}{}{\forall x.\forall x.(A \vlor B)}{
\vlhy{(\forall x.\forall x.A) \vlor B}}}}
\end{equation*}

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

* $\wrD/\fequ$:

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{B \vlor A}{
\vlin{\wrD}{}{A \vlor B}{
\vlhy{A}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{A \vlor (B \vlor C)}{
\vlin{\wrD}{}{(A \vlor B) \vlor C)}{
\vlhy{A \vlor C}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{(\forall x.A) \vlor B}{
\vlin{\wrD}{}{\forall x.(A \vlor B)}{
\vlhy{\forall x.A}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{(\forall x. A) \vlor B}{
\vlhy{\forall x.A}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{(\forall x.A) \vlor B}{
\vlin{\wrD}{}{\forall x.(B \vlor A)}{
\vlhy{\forall x.B}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{\forall x.(A \vlor B)}{
\vlin{\wrD}{}{(\forall x.A) \vlor B}{
\vlhy{\forall x.A}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{\forall x.(A \vlor B)}{
\vlhy{\forall x.A}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{\forall x.(A \vlor B)}{
\vlin{\wrD}{}{B \vlor (\forall x.A)}{
\vlhy{B}}}}
\end{equation*}

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

* $\wfaD/\fequ$:

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

\begin{equation*}
\scalebox{.9}{$
\vlderivation{
\vlin{\fequ}{}{\forall y.\forall x.A}{
\vlin{\wfaD}{(x \notin \fv(\forall y.A))}{\forall x.\forall y.A}{
\vlhy{\forall y.A}}}}
\leadsto
\vlderivation{
\vlin{\wfaD}{(x \notin \fv(A))}{\forall y.\forall x.A}{
\vlhy{\forall y.A}}}$}
\end{equation*}

\begin{equation*}
\scalebox{.9}{$
\vlderivation{
\vlin{\fequ}{}{\forall x.\forall y.A}{
\vlin{\wfaD}{(x \notin \fv(A))}{\forall y.\forall x.A}{
\vlhy{\forall y.A}}}}
\leadsto
\vlderivation{
\vlin{\wfaD}{(x \notin \fv(\forall y.A))}{\forall x.\forall y.A}{
\vlhy{\forall y.A}}}$}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{(\forall x.A) \vlor B}{
\vlin{\wfaD}{}{\forall x.(A \vlor B)}{
\vlhy{A \vlor B}}}}
\leadsto
\vlderivation{
\vlin{\wfaD}{}{(\forall x.A) \vlor B}{
\vlhy{A \vlor B}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\fequ}{}{\forall x.(A \vlor B)}{
\vlin{\wfaD}{}{(\forall x.A) \vlor B}{
\vlhy{A \vlor B}}}}
\leadsto
\vlderivation{
\vlin{\wfaD}{}{\forall x.(A \vlor B)}{
\vlhy{A \vlor B}}}
\end{equation*}

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

* $\fequ/\cfaD$:

\begin{equation*}
\vlderivation{
\vlin{\cfaD}{}{\forall x.\forall y.A}{
\vlin{\fequ}{}{\forall x.\forall x.\forall y. A}{
\vlhy{\forall x.\forall y.\forall x.A}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\cfaD}{}{\forall y.\forall x.A}{
\vlin{\fequ}{}{\forall y.\forall x.\forall x.A}{
\vlhy{\forall x.\forall y.\forall x.A}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\cfaD}{}{(\forall x.A) \vlor B}{
\vlin{\fequ}{(x \notin \fv(B))}{(\forall x.\forall x.A) \vlor B}{
\vlhy{\forall x.((\forall x.A) \vlor B)}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\cfaD}{}{\forall x.(A \vlor B)}{
\vlin{\fequ}{(x \notin \fv(B))}{\forall x.\forall x.(A \vlor B)}{
\vlhy{\forall x.((\forall x.A) \vlor B)}}}}
\end{equation*}

* $\fequ/\me$:

\begin{equation*}
\vlderivation{
\vlin{\me}{}{(A \vlor B) \vlan (C \vlor D)}{
\vlin{\fequ}{}{(A \vlan C) \vlor (B \vlan D)}{
\vlhy{(C \vlan A) \vlor (B \vlan D)}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\me}{}{(A \vlor B) \vlan (C \vlor D)}{
\vlin{\fequ}{}{(A \vlan C) \vlor (B \vlan D)}{
\vlhy{(B \vlan D) \vlor (A \vlan C)}}}}
\leadsto
\vlderivation{
\vlin{\fequ}{}{(A \vlor B) \vlan (C \vlor D)}{
\vlin{\me}{}{(B \vlor A) \vlan (D \vlor C)}{
\vlhy{(B \vlan D) \vlor (A \vlan C)}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\me}{}{(A \vlor B) \vlan ((C \vlan E) \vlor D)}{
\vlin{\fequ}{}{(A \vlan (C \vlan E)) \vlor (B \vlan D)}{
\vlhy{((A \vlan C) \vlan E) \vlor (B \vlan D)}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\me}{}{\forall x.((A \vlor B) \vlan (C \vlor D))}{
\vlin{\fequ}{(x \notin \fv(B \vlan D))}{\forall x.((A \vlan C) \vlor (B \vlan D))}{
\vlhy{(\forall x.(A \vlan C)) \vlor (B \vlan D)}}}}
\end{equation*}

* $\fequ/\mfaD$:

\begin{equation*}
\vlderivation{
\vlin{\mfaD}{}{\forall x.(A \vlor B)}{
\vlin{\fequ}{}{(\forall x.A) \vlor (\forall x.B)}{
\vlhy{(\forall x.B) \vlor (\forall x.A)}}}}
\leadsto
\vlderivation{
\vlin{\fequ}{}{\forall x.(A \vlor B)}{
\vlin{\mfaD}{}{\forall x.(B \vlor A)}{
\vlhy{(\forall x.B) \vlor (\forall x.A)}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\mfaD}{}{\forall x.((\forall y.A) \vlor B)}{
\vlin{\fequ}{}{(\forall x.\forall y.A) \vlor (\forall x.B)}{
\vlhy{(\forall y.\forall x.A) \vlor (\forall x.B)}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\mfaD}{}{\forall x.(A \vlor B)}{
\vlin{\fequ}{}{(\forall x.A) \vlor (\forall x.B)}{
\vlhy{\forall x.(A \vlor (\forall x.B))}}}}
\end{equation*}

* $\fequ/\mexD$: similar to $\fequ/\mfaD$

Interactions between two non-$\fequ$ rules with the presence of $\fequ$ in

* $\cfaD/\fequ/\rr$ where $\rr \in \set{\me, \mfaD, \mexD}$: First permute
$\cfaD$ under $\fequ$ and then permute $\cfaD$ under $\rr$.

* $\acD/\fequ/\rr$ where $\rr \in \set{\me, \mfaD, \mexD}$: First permute
$\acD$ under $\fequ$ and then permute $\acD$ under $\rr$.

* $\wrD/\fequ/\cfaD$:

\begin{equation*}
\vlderivation{
\vlin{\cfaD}{}{(\forall x.A) \vlor B}{
\vlin{\fequ}{}{(\forall x.\forall x.A) \vlor B}{
\vlin{\wrD}{}{\forall x.((\forall x.A) \vlor B)}{
\vlhy{\forall x.\forall x.A}}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{(\forall x.A) \vlor B}{
\vlin{\cfaD}{}{(\forall x.A) \vlor B}{
\vlhy{\forall x.\forall x.A}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\cfaD}{}{(\forall x.A) \vlor B}{
\vlin{\fequ}{}{(\forall x.\forall x.A) \vlor B}{
\vlin{\wrD}{}{\forall x.(B \vlor (\forall x.A))}{
\vlhy{\forall x.B}}}}}
\leadsto
\vlderivation{
\vlin{\fequ}{}{(\forall x.A) \vlor B}{
\vlin{\wrD}{}{\forall x.(B \vlor A)}{
\vlhy{\forall x.B}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\cfaD}{}{\forall x.(A \vlor B)}{
\vlin{\fequ}{}{\forall x.\forall x.(A \vlor B)}{
\vlin{\wrD}{}{\forall x.((\forall x.A) \vlor B)}{
\vlhy{\forall x.\forall x.A}}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{\forall x.(A \vlor B)}{
\vlin{\cfaD}{}{\forall x.A}{
\vlhy{\forall x.\forall x.A}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\cfaD}{}{\forall x.(A \vlor B)}{
\vlin{\fequ}{}{\forall x.\forall x.(A \vlor B)}{
\vlin{\wrD}{}{\forall x.(B \vlor (\forall x.A))}{
\vlhy{\forall x.B}}}}}
\leadsto
\vlderivation{
\vlin{\fequ}{}{\forall x.(A \vlor B)}{
\vlin{\wrD}{}{\forall x.(B \vlor A)}{
\vlhy{\forall x.B}}}}
\end{equation*}

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

* $\wrD/\fequ/\acD$:

\begin{equation*}
\vlderivation{
\vlin{\acD}{}{a \vlor B}{
\vlin{\fequ}{}{(a \vlor a) \vlor B}{
\vlin{\wrD}{}{(a \vlor B) \vlor a}{
\vlhy{a \vlor B}}}}}
\leadsto
\vlderivation{
\vlhy{a \vlor B}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\acD}{}{a \vlor B}{
\vlin{\fequ}{}{(a \vlor a) \vlor B}{
\vlin{\wrD}{}{a \vlor (a \vlor B)}{
\vlhy{a}}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{a \vlor B}{
\vlhy{a}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\acD}{}{\forall x.a}{
\vlin{\fequ}{(x \notin \fv(a))}{\forall x.(a \vlor a)}{
\vlin{\wrD}{}{(\forall x.a) \vlor a}{
\vlhy{\forall x.a}}}}}
\leadsto
\vlderivation{
\vlhy{\forall x.a}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\acD}{}{\forall x.a}{
\vlin{\fequ}{(x \notin \fv(a))}{\forall x.(a \vlor a)}{
\vlin{\wrD}{}{a \vlor (\forall x.a)}{
\vlhy{a}}}}}
\leadsto
\vlderivation{
\vlin{\wfaD}{(x \notin \fv(a))}{\forall x.a}{
\vlhy{a}}}
\end{equation*}

* $\wrD/\fequ/\me$:

\begin{equation*}
\vlderivation{
\vlin{\me}{}{(A \vlor B) \vlan (C \vlor D)}{
\vlin{\fequ}{}{(A \vlan C) \vlor (B \vlan D)}{
\vlin{\wrD}{}{(C \vlan A) \vlor (B \vlan D)}{
\vlhy{C \vlan A}}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{(A \vlor B) \vlan (C \vlor D)}{
\vlin{\wrD}{}{(A \vlor B) \vlan C}{
\vlin{\fequ}{}{A \vlan C}{
\vlhy{C \vlan A}}}}}
\end{equation*}

\begin{equation*}
\scalebox{.9}{$
\vlderivation{
\vlin{\me}{}{\forall x.((A \vlor B) \vlan (C \vlor D))}{
\vlin{\fequ}{}{\forall x.((A \vlan C) \vlor (B \vlan
\vlin{\wrD}{}{(B \vlan D) \vlor (\forall x.(A \vlan C))}{
\vlhy{B \vlan D}}}}}
\leadsto
\vlderivation{
\vlin{\fequ}{}{\forall x.((A \vlor B) \vlan (C \vlor D))}{
\vlin{\wrD}{}{\forall x.((B \vlor A) \vlan (D \vlor C))}{
\vlin{\wrD}{}{\forall x.((B \vlor A) \vlan D)}{
\vlin{\faD}{}{\forall x.(B \vlan D)}{
\vlhy{B \vlan D}}}}}}$}
\end{equation*}

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

* $\wrD/\fequ/\mfaD$:

\begin{equation*}
\vlderivation{
\vlin{\mfaD}{}{\forall x.(A \vlor B)}{
\vlin{\fequ}{}{(\forall x.A) \vlor (\forall x.B)}{
\vlin{\wrD}{}{(\forall x.B) \vlor (\forall x.A)}{
\vlhy{\forall x.B}}}}}
\leadsto
\vlderivation{
\vlin{\fequ}{}{\forall x.(A \vlor B)}{
\vlin{\wrD}{}{\forall x.(B \vlor A)}{
\vlhy{\forall x.B}}}}
\end{equation*}

\begin{equation*}
\vlderivation{
\vlin{\mfaD}{}{\forall x.(A \vlor B)}{
\vlin{\fequ}{}{(\forall x.A) \vlor (\forall x.B)}{
\vlin{\wrD}{}{\forall x.((\forall x.A) \vlor B)}{
\vlhy{\forall x.\forall x.A}}}}}
\leadsto
\vlderivation{
\vlin{\wrD}{}{\forall x.(A \vlor B)}{
\vlin{\cfaD}{}{\forall x.A}{
\vlhy{\forall x.\forall x.A}}}}
\end{equation*}

* $\wrD/\fequ/\mexD$:

\begin{equation*}
\vlderivation{
\vlin{\mexD}{}{\exists x.(A \vlor B)}{
\vlin{\fequ}{}{(\exists x.A) \vlor (\exists x.B)}{
\vlin{\wrD}{}{(\exists x.B) \vlor (\exists x.A)}{
\vlhy{\exists x.B}}}}}
\leadsto
\vlderivation{
\vlin{\fequ}{}{\exists x.(A \vlor B)}{
\vlin{\wrD}{}{\exists x.(B \vlor A)}{
\vlhy{\exists x.B}}}}
\end{equation*}

§.§ Proof of Lemma <ref>

<cit.>, there is a derivation
$\vlder{\set{\acD,\me,\PE\fequ}}{\DDeri}{\PE H}{\PE{(G\rsubstof\phi)}}$,
We plan to show that $\DDeri$ can be lifted to
$\set{\acD,\cfaD,\me,\mfaD,\mexD,\fequ}$. However, observe that not
every formula occurring in $\DDeri$ is a propositional
encoding. There are two reasons for this: (i) we might have
$P\PE\fequ Q$ where $P$ is a propositional encoding but $Q$ is not,
and (ii) the rule $\acD$ can duplicate an atom
$x\in\VAR$. Let us write $\acDx$ for such instances.
The problem with (i) is that we could have the following situation

\begin{equation}
\label{eq:m-illegal}
\vlderivation{
\vlin{\me}{}{\Scons{((x\vlan E)\vlor(x\vlan F))\vlan(C\vlor D)}}{
\vlin{\PE\fequ}{}{\Scons{((x\vlan E)\vlan C)\vlor((x\vlan F)\vlan D)}}{
\vlhy{\Scons{(x\vlan (E\vlan C))\vlor(x\vlan (F\vlan D))}}}}}
\end{equation}

where $x$ occurs in $C\vlor 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 $\me$ further below in the derivation:

\begin{equation}
\vlderivation{
\vlin{\me}{}{S'\cons{(x\vlor x)\vlan(E\vlor F)}}{
\vlhy{S'\cons{(x\vlan E)\vlor(x\vlan F)}}}}
\end{equation}

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

\begin{equation}
\label{eq:m-permutation}
\scalebox{.66}{$
\vlderivation{
\vlin{\me}{}{\Scons{(G\vlor H)\vlan(E\vlor F)\vlan(C\vlor D)}}{
\vlin{\me}{}{\Scons{((G\vlan E)\vlor(H\vlan F))\vlan(C\vlor D)}}{
\vlhy{\Scons{(G\vlan E\vlan C)\vlor(G\vlan F\vlan D)}}}}}
\;
\leftrightarrow
\;
\vlderivation{
\vlin{\me}{}{\Scons{(G\vlor H)\vlan(E\vlor F)\vlan(C\vlor D)}}{
\vlin{\me}{}{\Scons{(G\vlor H)\vlan((E\vlan C)\vlor(F\vlan D))}}{
\vlhy{\Scons{(G\vlan E\vlan C)\vlor(G\vlan F\vlan D)}}}}}
\end{equation}

We omitted some instances of $\PE\fequ$ and some parentheses.  We
now call instances of $\me$ as in (<ref>)
illegal, and we can transform $\DDeri$ through
$\me$-permutations (<ref>) into a derivation that
does not contain any illegal $\me$-instances.
address (ii),
we also apply a permutation argument, permuting all
instances of $\acDx$ up until they either reach the top of the
derivation or an instance of $\me$ which separates the two atoms in
the premise. More precisely, we consider the following inference rule

\begin{equation}
\label{eq:acDeq}
\vlinf{\acDeq}{}{\Scons{x}}{S_0\cons{S_1\cons{x}\vlor S_2\cons{x}}}
\end{equation}

where $S_1\conhole\fequ\conhole\vlor E$ and
$S_2\conhole\fequ\conhole\vlor F$ and $S\conhole\fequ
S_0\cons{\conhole\vlor E\vlor F}$ for some formulas $E$ and $F$, where $E$ or $F$ or both might be empty. The
rule $\acDeq$ permutes over $\fequ$, $\acD$, and other instances of $\acDeq$,
and over instances of $\me$ if they occur inside $S_0$ or $S_1$ or
$S_2$. The only situation in which $\acDeq$ cannot be permuted up is
the following:

\begin{equation}
\label{eq:mac}
\vlderivation{
\vlin{\acDeq}{}{\Scons{R\cons{x}\vlan(C\vlor D)}}{
\vlin{\me}{}{\Scons{(R_1\cons{x}\vlor R_2\cons{x})\vlan(C\vlor D)}}{
\vlhy{\Scons{(R_1\cons{x}\vlan C)\vlor (R_2\cons{x}\vlan D)}}}}}
\end{equation}

We can therefore assume that all instances of $\acDx$, that contract
an atom $x\in\VAR$ are either at the top of $\DDeri$ or below a
$\me$-instance as in (<ref>). We now lift $\DDeri$ to
$\set{\acD,\cfaD,\me,\mfaD,\mexD,\fequ}$, proceed by induction on
the height of $\DDeri$, beginning at the top, making a case
analysis on the topmost rule that is not a $\fequ$.

* $\acDx$: We know that the premise of (<ref>) is a
propositional encoding. Hence, $S_1\conhole=\conhole\vlor \PE E$ and
$S_2\conhole=\conhole\vlor \PE F$ and both $x$ are universals, and
$\PE E\vlor \PE F$ contains all occurrences of $x$ bound by that
universal. We have the following subcases:

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

\begin{equation*}
\vlinf{\acDeq}{}{\PE S\cons{x\vlor (\PE E\vlor \PE F)}}{\PE S\cons{(x\vlor \PE E)\vlor (x\vlor\PE F)}}
\end{equation*}

which can be lifted to

\begin{equation*}
\vlinf{\mfaD}{}{\Scons{\forall x.(E\vlor F)}}{S\cons{(\forall x.E)\vlor (\forall x.F)}}
\end{equation*}

where $\PE S\conhole, \PE E, \PE F$ are the propositional encodings of $\Sconhole,E,F$, respectively.

* $\PE E$ is empty and $\PE F$ is non-empty: We have

\begin{equation*}
\vlinf{\acDeq}{}{\PE S\cons{x\vlor \PE F)}}{\PE S\cons{x\vlor (x\vlor \PE F)}}
\end{equation*}

which can be lifted to

\begin{equation*}
\vlinf{\cfaD}{}{\Scons{\forall x.F}}{S\cons{\forall x.\forall x.F}}
\end{equation*}

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

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

* $\acD$ (contracting an ordinary atom): This can trivially be lifted.

* $\me$: There are several cases to consider.

* If none of the four principal formulas in the premise is $x$
or $x\vlor F$ for some formula $F$ and $x\in\VAR$, then this
instance of $\me$ 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 $\phi$ 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 (<ref>):

\begin{equation*}
\vlderivation{
\vlin{\acDeq}{}{\Scons{x\vlan(C\vlor D)}}{
\vlin{\me}{}{\Scons{(x\vlor x)\vlan(C\vlor D)}}{
\vlhy{\Scons{(x\vlan C)\vlor (x\vlan D)}}}}}
\end{equation*}

which can be lifted immediately to

\begin{equation*}
\vlinf{\mexD}{}{\Scons{\exists x.(C\vlor D)}}{\Scons{(\exists x.C)\vlor(\exists x.D)}}
\end{equation*}

* We have a situation (<ref>) where
$R_1\cons{x}\fequ x\vlor E$ for some $E$ and $R_2\cons{x}\fequ
x\vlor F$ for some $F$ with $R\cons{x}\fequ x\vlor E\vlor
F$ (Otherwise, the application of $\acDeq$ would not be correct.)
That means, we have:

\begin{equation*}
\vlderivation{
\vlin{\acDeq}{}{\Scons{(x\vlor E\vlor F)\vlan(C\vlor D)}}{
\vlin{\me}{}{\Scons{((x\vlor E)\vlor (x\vlor F))\vlan(C\vlor D)}}{
\vlhy{\Scons{((x\vlor E)\vlan C)\vlor ((x\vlor F)\vlan D)}}}}}
\end{equation*}

which can be lifted to

\begin{equation*}
\vlderivation{
\vlin{\mfaD}{}{\Scons{(\forall x.(E\vlor F))\vlan(C\vlor D)}}{
\vlin{\me}{}{\Scons{((\forall x. E)\vlor (\forall x. F))\vlan(C\vlor D)}}{
\vlhy{\Scons{((\forall x. E)\vlan C)\vlor ((\forall x. F)\vlan D)}}}}}
\end{equation*}

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

Thus $\DDeri$ can be lifted to