On the semantics of proofs in classical sequent calculus.
On the semantics of proofs in classical sequent calculus

Fabio Massaioli
F. Massaioli

Scuola Normale Superiore, Pisa, Italy

We discuss the problem of finding non-trivial invariants of non-deterministic, symmetric
cut-reduction procedures in the classical sequent calculus. We come to the conclusion
that (an enriched version of) the propositional fragment of GS4 – i.e. the one-sided
variant of Kleene's context-sharing style sequent system G4, where independent rule
applications permute freely – is an ideal framework in which to attack the problem.
We show that the graph induced by axiom rules linking dual atom occurrences is preserved
under arbitrary rule permutations in the cut-free fragment of GS4. We then refine the
notion of axiom-induced graph so as to extend the result to derivations with cuts, and
we exploit the invertibility of logical rules to define a global normalisation procedure
that preserves the refined axiom-induced graphs, thus yielding a non-trivial invariant
of cut-elimination in GS4. Finally, we build upon the result to devise a new proof system
for classical propositional logic, where the rule permutations of GS4 reduce to identities.

§ INTRODUCTION

Cut-elimination procedures in classical sequent calculus are notoriously non-deterministic
and non-confluent, both in the original formulation by Gentzen and in later reformulations
<cit.>. It is natural to ask whether those instances of
non-confluence are superficial in nature, i.e. whether distinct normal forms of the same
derivation are in fact correlated in a non-trivial way. A famous counter-example by Lafont
<cit.> purports to show that the answer is negative, that is, any notion of proof
equivalence compatible with classical cut-elimination must be a trivial one that identifies
all proofs of the same sequent. Specifically, the counter-example involves a derivation of
the form

\[
\prftree[r]{\rl{ctr}}
{\prfsummary[\(P\)]{\th A}}
{\th A, B}}
{\prfsummary[\(Q\)]{\th A}}
{\th A, \dl{B}}}
{\th A, A}}
{\th A}
\]

where \(P,Q\) are a pair of arbitrary derivations of the same formula \(A\)[We
use the one-sided formulation of sequent calculus in the style of Tait <cit.> to
reduce the number of rules to be treated. Negation is defined as an involution on formulas
through De Morgan dualities. Sequents are considered as multisets, i.e. quotiented up to
arbitrary permutations of their elements, hence the exchange rule is implicit]. Because
both cut-formulas are introduced by weakening, there are two ways to eliminate the cut,
leading to two potentially very different derivations:

\[
\prftree[r]{\rl{ctr}}
{\prfsummary[\(P\)]{\th A}}
{\th A, A}}
{\th A}
\qquad\qquad
\prftree[r]{\rl{ctr}}
{\prfsummary[\(Q\)]{\th A}}
{\th A, A}}
{\th A}
\]

Any notion of proof identity that is compatible with the cut-elimination process should then
identify all three derivations shown above, leading to the identification of \(P\) with \(Q\)
under the reasonable assumption that the weakening-contraction sequence on \(A\) be an
irrelevant detour. \(P\) and \(Q\), however, were arbitrary derivations of \(A\),
i.e. potentially not correlated in any way: this has catastrophic consequences, making
our hypothetical notion of proof identity trivial and patently unreasonable. For example,
the following three proofs would be identified:

\[
\prftree[r]{\rl{\lor}}
{\prfsummary{\th A}}
{\th A \lor B}
\qquad\qquad
\prftree[r]{\rl{\lor}}
{\prfsummary{\th B}}
{\th A \lor B}
\qquad\qquad
\prftree[r]{\rl{\lor}}
{\prfsummary{\th A, B}}
{\th A \lor B}
\]

meaning that it does not matter at all whether a disjunction holds in virtue of the left
or of the right disjunct, or by contradiction. In a sense we are identifying not just
all proofs of the same thesis, but indeed all proofs altogether.

Under such a notion of proof identity, it becomes utterly useless to look for alternative
proofs of the same theorem, as they are virtually the same as any other one and there is
nothing to be learned from them: a conclusion that plainly contradicts millennia of mathematical

Many solutions have been proposed. We mention among them Krivine's classical realizability
program <cit.>, which has yielded a fruitful analysis of classical reasoning
principles in computational terms; the approaches based on polarised deductive systems,
like Girard's calculus LC <cit.>, Parigot's \(\lambda\mu\)-calculus <cit.>,
Danos Joinet and Schellinx' calculi LKT and LKQ <cit.>, and finally the approaches
based on fine grained focalization and embeddings of the classical sequent calculus into
linear logic <cit.>.

From the point of view of sequent calculus, the common thread to all mentioned solutions
is to restrict cut-elimination (and sometimes the logical rules too) in a principled way,
breaking its simmetry and therefore solving the non-deterministic cases. Typically the
approaches based on \(\lambda\)-calculus correspond to various double-negation translations
from classical to intuitionistic logic that preserve provability. While this approach
bears many interesting results, it is not entirely satisfactory.

On the one hand, every restriction is somewhat arbitrary. Looking back at Lafont's
example above, it is hard to see any actual reason to privilege one reduct over
the other, and doing so arguably fails to capture the content of the original derivation,
which effectively offers two possible ways to prove the same conclusion. On the other hand,
the problem is by no means exclusive to sequent calculus. Analogous examples can be constructed
in a great variety of classical proof systems, with the notable exception of those who have
been accurately tuned to avoid them, and there is even a categorical counterpart due to Joyal.
The solutions recalled above sacrifice the inherent symmetries of classical proof systems
to the possibility of extracting at least some computational content from them. It is
important to underline here that while those symmetries are not strictly needed to characterize
classical provability, the fact that classical logic allows them to arise seems to be somehow
essential to it.

A long standing open question has been then whether it could possible to work around
the non-deterministic reduction steps by natural and non-trivial adjustments of the calculus
and/or of cut-reduction steps, without resorting to symmetry-breaking techniques like
polarization or embeddings into intuitionistic or linear logic. It is clear that Lafont's
example requires a change in the calculus. Two simple solutions have been discussed many
times in the literature: the mix rule and non-deterministic sums.

\[
\makebox[\textwidth]{\small\(
\vcenter{\prftree[r]{\rl{mix}}
{\prfsummary[\(P\)]{\th \Gamma}}
{\prfsummary[\(Q\)]{\th \Delta}}
{\th \Gamma, \Delta}}
\quad\stackrel{?}{\longleftarrow}\quad
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma}}
{\th \Gamma, A}}
{\prfsummary[\(Q\)]{\th \Delta}}
{\th \Delta, \dl{A}}}
{\th \Gamma, \Delta}}
\quad\stackrel{?}{\longrightarrow}\quad
\vcenter{\prftree[r]{\rl{\oplus}}
{\prfsummary[\(P\)]{\th \Gamma}}
{\th \Gamma, \Delta}}
{\prfsummary[\(Q\)]{\th \Delta}}
{\th \Gamma, \Delta}}
{\th \Gamma, \Delta}}
\)}
\]

While those two rules do not contribute to classical provability, they increase the amount
of available proofs <cit.>, accommodating for cut-free proofs that intuitively “provide
multiple alternatives.”

The non-deterministic sum (on the right) expresses the intuitive idea that the resulting
proof might be seen either as \(P\) or \(Q\), without the reader being free to choose between
the two alternatives. Its use can be extended coherently to all problematic situations,
viewing proofs with cuts as the sum of their possible normal forms. While this approach
is known to be non-trivial and non-reducible to intuitionistic or linear embeddings (see
e.g. <cit.>), it is also not very deep, as it does not get to the point of what
the content of a classical proof actually is; notably, it is not known to yield a canonical
representation of classical proofs up to the related notion of proof identity. Moreover,
it has no faithful representation on paper, where the choice between \(P\) and \(Q\)
is clearly available to the reader.

On the other hand, the mix rule (on the left) expresses the idea that two proofs are
effectively provided in parallel, both equally available to the reader. Informally, this
might be viewed as writing down two different proofs of the same theorem one after the
other: something that makes sense and might actually happen in mathematics textbooks.
Extending the calculus with the mix rule effectively solves the weakening-weakening
problem[Note however that there is a subtle technical issue to be handled:
because logical rules might hide applications of weakenings on their subformulas, weakening
cuts cannot be eliminated directly; instead, all weakenings must first be reduced to atomic
form, something which is well-known to be possible in classical logic.]. The question
becomes then how to handle the other two non-deterministic reduction steps (<ref>).

\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \vphantom{\dl{A}}}}
{\prfsummary[\(Q\)]{\th \Delta, \dl{A}}}
{\th \Gamma, \Delta, B \vphantom{\dl{A}}}}
{\prfsummary[\(R\)]{\th \Sigma, \dl{B}}}
{\th \Gamma, \Delta, \Sigma}}
\quad\longleftarrow\quad
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \vphantom{\dl{AB}}}}
{\th \Gamma, A \lor B \vphantom{\dl{AB}}}}
{\prfsummary[\(Q\)]{\th \Delta, \dl{A}}}
{\prfsummary[\(R\)]{\th \Sigma, \dl{B}}}
{\th \Delta, \Sigma, \dl{A} \land \dl{B}}}
{\th \Gamma, \Delta, \Sigma}}
\quad\longrightarrow\quad
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \vphantom{\dl{B}}}}
{\prfsummary[\(R\)]{\th \Sigma, \dl{B}}}
{\th \Gamma, A, \Sigma \vphantom{\dl{A}}}}
{\prfsummary[\(Q\)]{\th \Delta, \dl{A}}}
{\th \Gamma, \Delta, \Sigma}}
\)

\vcenter{\prftree[r,d]{\rl{wk}}
{\prfsummary[\(P\)]{\th \Gamma}}
{\th \Gamma, \Delta}}
\quad\longleftarrow\quad
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma}}
{\th \Gamma, A \vphantom{\dl{A}}}}
{\prfsummary[\(Q\)]{\th \Delta}}
{\th \Delta, \dl{A}}}
{\th \Gamma, \Delta}}
\quad\longrightarrow\quad
\vcenter{\prftree[r,d]{\rl{wk}}
{\prfsummary[\(Q\)]{\th \Delta}}
{\th \Gamma, \Delta}}
\)

\vcenter{\prftree[r,d]{\rl{ctr}}
{\prfsummary[\(P\)]{\th \Gamma, A, A \vphantom{\dl{A}}}}
{\th \Gamma, A \vphantom{\dl{A}}}}
{\prfsummary[\(P\)]{\th \Gamma, A, A}}
{\th \Gamma, A}}
{\prfsummary[\(Q\)]{\th \Delta, \dl{A}, \dl{A}}}
{\th \Gamma, \Delta, \dl{A}}}
{\th \Gamma, \Delta, \Delta}}
{\th \Gamma, \Delta}}
\quad\longleftarrow\quad
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, A \vphantom{\dl{A}}}}
{\th \Gamma, A \vphantom{\dl{A}}}}
{\prfsummary[\(Q\)]{\th \Delta, \dl{A}, \dl{A}}}
{\th \Delta, \dl{A}}}
{\th \Gamma, \Delta}}
\quad\longrightarrow\quad
\vcenter{\prftree[r,d]{\rl{ctr}}
{\prfsummary[\(P\)]{\th \Gamma, A, A}}
{\prfsummary[\(Q\)]{\th \Delta, \dl{A}, \dl{A}}}
{\th \Delta, \dl{A}}}
{\th \Gamma, \Delta, A \vphantom{\dl{A}}}}
{\prfsummary[\(Q\)]{\th \Delta, \dl{A}, \dl{A}}}
{\th \Delta, \dl{A}}}
{\th \Gamma, \Delta, \Delta}}
{\th \Gamma, \Delta}}
\)
Non-deterministic cut-reduction steps in the classical sequent calculus; also
called logical and structural dilemmas in <cit.>.

We start from an idea which is well-established in proof-theory, i.e. that the way axioms
link together the subformulas of the conclusion is somehow essential to the content of a proof.
Such an idea underlines, e.g., the theory of proof-nets <cit.> and the research program
known as Geometry of Interaction <cit.>, but has also been widely explored –
for various purposes and in many different ways – in the classical setting, among others by
Andrews <cit.>, Statman <cit.>, Buss and Carbone <cit.>,
Lamarche and Straßburger <cit.>, Hughes <cit.>, Guglielmi and
Gundersen <cit.>.

The approach of Andrews, Lamarche and Straßburger in particular is of interest here: it consists
in extracting graphs from each derivation, whose vertices are the atomic formula occurrences
in the conclusion and whose edges join those dual occurrences that are related by some axiom.
Andrews first considered graphs of this kind (which he called matings) in <cit.>,
and showed in <cit.> how to reconstruct natural deduction proofs from them. Lamarche
and Straßburger used them in <cit.> to develop a system of proof-nets for classical
logic (which they called \(\mathbb{B}\)-nets), and provided a correctness criterion
and a sequentialization theorem, as well as a confluent and terminating cut-elimination
procedure on nets which corresponds essentially to a composition of graphs by contraction
of alternating paths, in the style of the Geometry of Interaction.

Having such a procedure is of the essence when extracting graphs from derivations with cuts.
One has to trace the history of all atomic occurrences through the derivation, then combine
the traces with axioms and cuts in an appropriate way to obtain the resulting graph. As an
example consider the following derivation:

\[
\prftree[r]{\rl{cut}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{x-l-1}{\alpha}}, \tikzmarknode{y-l-1}{\alpha}}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\alpha}, \alpha}}
{\th \dl{\tikzmarknode{x-l-2}{\alpha}} \land \dl{\alpha}, \tikzmarknode{y-l-2}{\alpha}, \alpha}}
{\th \dl{\tikzmarknode{x-l-3}{\alpha}} \land \dl{\alpha}, \tikzmarknode{y-l-3}{\alpha}}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\alpha}, \alpha}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{y-r-1}{\alpha}}, \tikzmarknode{z-r-1}{\alpha}}}
{\th \dl{\alpha}, \dl{\tikzmarknode{y-r-2}{\alpha}}, \alpha \land \tikzmarknode{z-r-2}{\alpha}}}
{\th \dl{\tikzmarknode{y-r-3}{\alpha}}, \alpha \land \tikzmarknode{z-r-3}{\alpha}}}
{\th \dl{\tikzmarknode{x-4}{\alpha}} \land \dl{\alpha}, \alpha \land \tikzmarknode{z-4}{\alpha}}
\]

[remember picture, overlay, thick, blue]

([yshift=2pt]x-l-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]y-l-1.north);
([yshift=2pt]y-r-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]z-r-1.north);

([yshift=2pt]x-4.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]x-l-3.south);
([yshift=2pt]x-l-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. ([yshift=-1pt]x-l-2.south);
([yshift=2pt]x-l-2.north) .. controls ++(0,5pt) and ++(0,-5pt) .. ([yshift=-1pt]x-l-1.south);

([yshift=1pt]y-l-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. ([yshift=-1pt]y-l-2.south);
([yshift=1pt]y-l-2.north) .. controls ++(0,5pt) and ++(0,-5pt) .. ([yshift=-1pt]y-l-1.south);

([yshift=2pt]y-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. ([yshift=-1pt]y-r-2.south);
([yshift=2pt]y-r-2.north) .. controls ++(0,5pt) and ++(0,-5pt) .. ([yshift=-1pt]y-r-1.south);

([yshift=1pt]z-4.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]z-r-3.south);
([yshift=1pt]z-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. ([yshift=-1pt]z-r-2.south);
([yshift=1pt]z-r-2.north) .. controls ++(0,5pt) and ++(0,-5pt) .. ([yshift=-1pt]z-r-1.south);

[draw, densely dashed, semithick, rounded corners=2pt]
([xshift=1pt]y-l-3.east) – ([xshift=5pt]y-l-3.south east) – ([xshift=-5pt]y-r-3.south west) – ([xshift=-1pt]y-r-3.west);

We select an atomic formula occurrence in the conclusion and start tracing its history up
through the derivation; when we reach an axiom we move to the linked dual occurrence and
start traveling down; when we reach a cut we move to the corresponding dual occurrence
in the other premiss and start moving up again; we continue doing so until we get back
to the conclusion: the graph shall then contain an edge linking the initial and final
points of the resulting path.

The key idea is however not just to track the axioms, but also to avoid counting them.
To understand why this approach might hold promise for a better treatment of the contraction
case, consider the following example:

\[
\prftree[r]{\rl{cut}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{x-1}{\alpha}}, \tikzmarknode{y-1}{\alpha}}}
{\prfsummary{\th B, C, C}}
{\th B, C \vphantom{\dl{\alpha}}}}
{\th \dl{\tikzmarknode{x-2}{\alpha}}, \tikzmarknode{y-2}{\alpha} \land B, C}}
{\prfsummary{\th \dl{C}, \dl{C}}}
{\th \dl{C}}}
{\th \dl{\tikzmarknode{x-3}{\alpha}}, \tikzmarknode{y-3}{\alpha} \land B}
\]

[remember picture, overlay, thick, blue]

([yshift=2pt]x-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]y-1.north);

([yshift=2pt]x-3.north) .. controls ++(0,5pt) and ++(0,-10pt) .. ([yshift=-1pt]x-2.south);
([yshift=2pt]x-2.north) .. controls ++(0,3pt) and ++(0,-7pt) .. ([yshift=-1pt]x-1.south);

([yshift=1pt]y-3.north) .. controls ++(0,10pt) and ++(0,-5pt) .. ([yshift=-1pt]y-2.south);
([yshift=1pt]y-2.north) .. controls ++(0,7pt) and ++(0,-3pt) .. ([yshift=-1pt]y-1.south);

Notice that there is exactly one axiom rule linking the two dual occurences of \(\alpha\)
in the conclusion. There are two possible ways to reduce the cut:

\[
\scalebox{0.8}{\makebox[\textwidth]{\(
\vcenter{\prftree[r]{\rl{\land}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{x-1}{\alpha}}, \tikzmarknode{y-1}{\alpha}}}
{\prfsummary{\th B, C, C}}
{\th B, C \vphantom{\dl{C}}}}
{\prfsummary{\th \dl{C}, \dl{C}}}
{\th \dl{C}}}
{\th B \vphantom{\dl{\alpha}}}}
{\th \dl{\tikzmarknode{x-2}{\alpha}}, \tikzmarknode{y-2}{\alpha} \land B}}
\qquad\qquad
\vcenter{\prftree[r,d]{\rl{ctr}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{z-1}{\alpha}}, \tikzmarknode{u-1}{\alpha}}}
{\prfsummary{\th B, C, C}}
{\th B, C \vphantom{\dl{\alpha}}}}
{\th \dl{\tikzmarknode{z-2}{\alpha}}, \tikzmarknode{u-2}{\alpha} \land B, C}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{v-1}{\alpha}}, \tikzmarknode{w-1}{\alpha}}}
{\prfsummary{\th B, C, C}}
{\th B, C \vphantom{\dl{\alpha}}}}
{\th \dl{\tikzmarknode{v-2}{\alpha}}, \tikzmarknode{w-2}{\alpha} \land B, C}}
{\prfsummary{\th \dl{C}, \dl{C}}}
{\th \dl{\tikzmarknode{v-3}{\alpha}}, \tikzmarknode{w-3}{\alpha} \land B, \dl{C}}}
{\th \dl{\tikzmarknode{z-3}{\alpha}}, \tikzmarknode{u-3}{\alpha} \land B, \dl{\tikzmarknode{v-4}{\alpha}}, \tikzmarknode{w-4}{\alpha} \land B}}
{\th \dl{\tikzmarknode{zv}{\alpha}}, \tikzmarknode{uw}{\alpha} \land B}}
\)}%
\begin{tikzpicture}[remember picture, overlay, thick, blue]
% Axioms
\draw ([yshift=2pt]x-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]y-1.north);
\draw ([yshift=2pt]z-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]u-1.north);
\draw ([yshift=2pt]v-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]w-1.north);
% History of x
\draw ([yshift=2pt]x-2.north) .. controls ++(0,5pt) and ++(0,-10pt) .. ([yshift=-1pt]x-1.south);
% History of y
\draw ([yshift=1pt]y-2.north) .. controls ++(0,10pt) and ++(0,-5pt) .. ([yshift=-1pt]y-1.south);
% History of z
\draw ([yshift=2pt]zv.north) .. controls ++(0,3pt) and ++(0,-7pt) .. ([yshift=-1pt]z-3.south);
\draw ([yshift=2pt]z-3.north) .. controls ++(0,10pt) and ++(0,-15pt) .. ([yshift=-1pt]z-2.south);
\draw ([yshift=2pt]z-2.north) .. controls ++(0,3pt) and ++(0,-7pt) .. ([yshift=-1pt]z-1.south);
% History of u
\draw ([yshift=1pt]uw.north) .. controls ++(0,7pt) and ++(0,-3pt) .. ([yshift=-1pt]u-3.south);
\draw ([yshift=1pt]u-3.north) .. controls ++(0,18pt) and ++(0,-10pt) .. ([yshift=-1pt]u-2.south);
\draw ([yshift=1pt]u-2.north) .. controls ++(0,7pt) and ++(0,-3pt) .. ([yshift=-1pt]u-1.south);
% History of v
\draw ([yshift=2pt]zv.north) .. controls ++(0,7pt) and ++(0,-3pt) .. ([yshift=-1pt]v-4.south);
\draw ([yshift=2pt]v-4.north) .. controls ++(0,15pt) and ++(0,-10pt) .. ([yshift=-1pt]v-3.south);
\draw ([yshift=2pt]v-3.north) .. controls ++(0,5pt) and ++(0,-10pt) .. ([yshift=-1pt]v-2.south);
\draw ([yshift=2pt]v-2.north) .. controls ++(0,3pt) and ++(0,-7pt) .. ([yshift=-1pt]v-1.south);
% History of w
\draw ([yshift=1pt]uw.north) .. controls ++(0,3pt) and ++(0,-7pt) .. ([yshift=-1pt]w-4.south);
\draw ([yshift=1pt]w-4.north) .. controls ++(0,10pt) and ++(0,-15pt) .. ([yshift=-1pt]w-3.south);
\draw ([yshift=1pt]w-3.north) .. controls ++(0,10pt) and ++(0,-5pt) .. ([yshift=-1pt]w-2.south);
\draw ([yshift=1pt]w-2.north) .. controls ++(0,7pt) and ++(0,-3pt) .. ([yshift=-1pt]w-1.south);
\end{tikzpicture}}
\]

On the left, the cut has been commuted with the conjunction rule. Axioms in the new derivation
have not changed at all. On the right, the cut has been reduced into two cuts of lower complexity,
and the left subderivation has been duplicated. There are now clearly more axioms than before,
but they link the exact same subformulas. For example, two axioms now link the dual
occurrences of \(\alpha\) in the conclusion, but no new link has been created.

The question is then whether axiom-induced graphs, being insensitive to changes in the number
of axioms in a derivation, are indeed preserved by all non-deterministic cut-reduction steps.
Lamarche and Straßburger were motivated by results obtained in the family of formalisms known
as Deep Inference, and while they provided an interpretation of the sequent calculus
into \(\mathbb{B}-nets\), as far as we know they didn't investigate in detail the behaviour
of the interpretation under cut-elimination. Führmann and Pym have proven in <cit.>
– as a general theorem for a whole class of interpretations of the classical sequent
calculus – that the axiom-induced graphs cannot gain edges under cut-reduction, i.e. that
our intuition that no axioms are created is indeed correct. They also show that the graphs
are preserved by the two logical cut-reduction steps, and it is possible to prove that they
are also invariant under atomic weakening reductions when the non-deterministic case is solved
by the mix rule.

Unfortunately, it turns out they are not preserved by all cut-reduction steps involving
contraction, as there are cases where some paths disappear. The prototypical counter-example,
also due to Führmann and Pym <cit.>, looks like this:

\[
\prftree[r]{\rl{cut}}
{\prfsummary{\th A}}
{\prfsummary[\(P\)]{\th \tikzmarknode{bc-l-1}{B}, \tikzmarknode{ac-l-1}{A}}}
{\th A \land \tikzmarknode{bc-l-2}{B}, \tikzmarknode{ac-l-2}{A}}}
{\prfsummary{\th B}}
{\th A \land \tikzmarknode{bc-l-3}{B}, \tikzmarknode{ac-l-3}{A} \land B}}
{\th \tikzmarknode{ac-l-4}{A} \land \tikzmarknode{bc-l-4}{B}}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{ac-r-1}{A}}, \tikzmarknode{a-r-1}{A}}}
{\th \dl{\tikzmarknode{ac-r-2}{A}}, \dl{B}, \tikzmarknode{a-r-2}{A}}}
{\th \dl{\tikzmarknode{ac-r-3}{A}} \lor \dl{B}, \tikzmarknode{a-r-3}{A}}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{bc-r-1}{B}}, \tikzmarknode{b-r-1}{B}}}
{\th \dl{A}, \dl{\tikzmarknode{bc-r-2}{B}}, \tikzmarknode{b-r-2}{B}}}
{\th \dl{A} \lor \dl{\tikzmarknode{bc-r-3}{B}}, \tikzmarknode{b-r-3}{B}}}
{\th \dl{\tikzmarknode{ac-r-4}{A}} \lor \dl{B}, \dl{A} \lor \dl{\tikzmarknode{bc-r-4}{B}}, \tikzmarknode{a-r-4}{A} \land \tikzmarknode{b-r-4}{B}}}
{\th \dl{\tikzmarknode{ac-r-5}{A}} \lor \dl{\tikzmarknode{bc-r-5}{B}}, \tikzmarknode{a-r-5}{A} \land \tikzmarknode{b-r-5}{B}}}
{\th \tikzmarknode{a-6}{A} \land \tikzmarknode{b-6}{B}}
\]

[remember picture, overlay, thick, blue]

[draw, densely dotted, rounded corners=.5em]
([yshift=2pt]bc-l-1.north west) – ([shift=(-5pt,5pt)]bc-l-1.north west) – ([shift=(-5pt,3em)]bc-l-1.north west)
– ([shift=(5pt,3em)]ac-l-1.north east) – ([shift=(5pt,5pt)]ac-l-1.north east) – ([yshift=2pt]ac-l-1.north east);
([yshift=2pt]ac-r-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]a-r-1.north);
([yshift=2pt]bc-r-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]b-r-1.north);

(bc-l-4.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (bc-l-3.south);
(bc-l-3.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (bc-l-2.south);
(bc-l-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (bc-l-1.south);

(ac-l-4.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (ac-l-3.south);
(ac-l-3.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (ac-l-2.south);
(ac-l-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (ac-l-1.south);

([yshift=2pt]ac-r-5.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (ac-r-4.south);
([yshift=2pt]ac-r-4.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (ac-r-3.south);
([yshift=2pt]ac-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (ac-r-2.south);
([shift=(2pt,2pt)]ac-r-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (ac-r-1.south);

(a-6.north) .. controls ++(0,15pt) and ++(0,-10pt) .. (a-r-5.south);
(a-r-5.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (a-r-4.south);
(a-r-4.north) .. controls ++(0,15pt) and ++(0,-10pt) .. (a-r-3.south);
(a-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (a-r-2.south);
(a-r-2.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (a-r-1.south);

([yshift=2pt]bc-r-5.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (bc-r-4.south);
([yshift=2pt]bc-r-4.north) .. controls ++(0,7pt) and ++(0,-7pt) .. (bc-r-3.south);
([yshift=2pt]bc-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (bc-r-2.south);
([yshift=2pt]bc-r-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (bc-r-1.south);

(b-6.north) .. controls ++(0,10pt) and ++(0,-20pt) .. (b-r-5.south);
(b-r-5.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (b-r-4.south);
(b-r-4.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (b-r-3.south);
(b-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (b-r-2.south);
(b-r-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (b-r-1.south);

[draw, densely dashed, semithick, rounded corners=1em]
(ac-l-4.south) – ([yshift=-2em]ac-l-4.south) – ([yshift=-2em]ac-r-5.south) – (ac-r-5.south);
[draw, densely dashed, semithick, rounded corners=1em]
(bc-l-4.south) – ([yshift=-3em]bc-l-4.south) – ([yshift=-3em]bc-r-5.south) – (bc-r-5.south);

Observe that, under the assumption that the subderivation \(P\) have a path connecting \(B\)
with \(A\) (represented here as a dotted line), there is in the axiom graph of the complete
derivation a path connecting (some subformula of) \(A\) with (some subformula of) \(B\) in the
conclusion. When the cut is reduced by duplicating the right subderivation and commuting it
up the two conjunctions, nothing bad happens. However, if the cut is reduced by duplicating
the left subderivation, the path traced above is lost:

\[
\makebox[\textwidth]{\small\(
\prftree[r]{\rl{cut}}
{\prfsummary{\th A}}
{\prfsummary[\(P\)]{\th \tikzmarknode{bc-l1-1}{B}, \tikzmarknode{ac-l1-1}{A}}}
{\th A \land \tikzmarknode{bc-l1-2}{B}, \tikzmarknode{ac-l1-2}{A}}}
{\prfsummary{\th B}}
{\th A \land \tikzmarknode{bc-l1-3}{B}, \tikzmarknode{ac-l1-3}{A} \land B}}
{\th \tikzmarknode{ac-l1-4}{A} \land \tikzmarknode{bc-l1-4}{B}}}
{\prfsummary{\th A}}
{\prfsummary[\(P\)]{\th \tikzmarknode{bc-l2-1}{B}, \tikzmarknode{ac-l2-1}{A}}}
{\th A \land \tikzmarknode{bc-l2-2}{B}, \tikzmarknode{ac-l2-2}{A}}}
{\prfsummary{\th B}}
{\th A \land \tikzmarknode{bc-l2-3}{B}, \tikzmarknode{ac-l2-3}{A} \land B}}
{\th \tikzmarknode{ac-l2-4}{A} \land \tikzmarknode{bc-l2-4}{B}}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{ac-r-1}{A}}, \tikzmarknode{a-r-1}{A}}}
{\th \dl{\tikzmarknode{ac-r-2}{A}}, \dl{B}, \tikzmarknode{a-r-2}{A}}}
{\th \dl{\tikzmarknode{ac-r-3}{A}} \lor \dl{B}, \tikzmarknode{a-r-3}{A}}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{bc-r-1}{B}}, \tikzmarknode{b-r-1}{B}}}
{\th \dl{\tikzmarknode{aw-r-1}{A}}, \dl{\tikzmarknode{bc-r-2}{B}}, \tikzmarknode{b-r-2}{B}}}
{\th \dl{\tikzmarknode{aw-r-2}{A}} \lor \dl{\tikzmarknode{bc-r-3}{B}}, \tikzmarknode{b-r-3}{B}}}
{\th \dl{\tikzmarknode{ac-r-4}{A}} \lor \dl{B}, \dl{\tikzmarknode{aw-r-3}{A}} \lor \dl{\tikzmarknode{bc-r-4}{B}}, \tikzmarknode{a-r-4}{A} \land \tikzmarknode{b-r-4}{B}}}
{\th \dl{\tikzmarknode{ac-r-5}{A}} \lor \dl{\tikzmarknode{bc-r-5}{B}}, \tikzmarknode{a-r-5}{A} \land \tikzmarknode{b-r-5}{B}}}
{\th \tikzmarknode{a-6}{A} \land \tikzmarknode{b-6}{B}}
\)}
\]

[remember picture, overlay, thick, blue]

[draw, densely dotted, rounded corners=.5em]
([yshift=2pt]bc-l2-1.north west) – ([shift=(-5pt,5pt)]bc-l2-1.north west) – ([shift=(-5pt,3em)]bc-l2-1.north west)
– ([shift=(5pt,3em)]ac-l2-1.north east) – ([shift=(5pt,5pt)]ac-l2-1.north east) – ([yshift=2pt]ac-l2-1.north east);

([yshift=2pt]bc-r-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]b-r-1.north);

(bc-l2-4.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (bc-l2-3.south);
(bc-l2-3.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (bc-l2-2.south);
(bc-l2-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (bc-l2-1.south);

(ac-l2-4.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (ac-l2-3.south);
(ac-l2-3.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (ac-l2-2.south);
(ac-l2-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (ac-l2-1.south);

([yshift=2pt]aw-r-3.north) .. controls ++(0,7pt) and ++(0,-3pt) .. (aw-r-2.south west);
([yshift=2pt]aw-r-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (aw-r-1.south);

([yshift=2pt]bc-r-4.north) .. controls ++(0,7pt) and ++(0,-7pt) .. (bc-r-3.south);
([yshift=2pt]bc-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (bc-r-2.south);
([yshift=2pt]bc-r-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (bc-r-1.south);

(b-6.north) .. controls ++(0,15pt) and ++(0,-10pt) .. (b-r-5.south);
(b-r-5.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (b-r-4.south);
(b-r-4.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (b-r-3.south);
(b-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (b-r-2.south);
(b-r-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (b-r-1.south);

[draw, densely dashed, semithick, rounded corners=1em]
(ac-l2-4.south) – ([yshift=-1em]ac-l2-4.south) – ([shift=(3em,-1em)]ac-l2-4.south)
– ([shift=(3em,-3em)]ac-l2-4.south) – ([yshift=-3em]aw-r-3.south) – (aw-r-3.south);
[draw, densely dashed, semithick, rounded corners=1em]
(bc-l2-4.south) – ([yshift=-4em]bc-l2-4.south) – ([yshift=-4em]bc-r-4.south) – (bc-r-4.south);

We show for clarity only the surviving part of the path that is connected to \(B\). Note how
the new path must end at the weakening rule. The old path depended critically on the ability
to pass through both premises of the contraction rule; now that the contraction rule has
vanished and we have two independent cuts it becomes impossible to construct the same path.

There is however a better way to look at the same problem. Notice how the following two
derivations are associated to the same axiom graph:

\[
\vcenter{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{ac-l-1}{A}} \lor \dl{\tikzmarknode{bc-l-1}{B}}, \tikzmarknode{a-l-1}{A} \land \tikzmarknode{b-l-1}{B}}}
\qquad\qquad
\vcenter{\prftree[r]{\rl{ctr}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{ac-r-1}{A}}, \tikzmarknode{a-r-1}{A}}}
{\th \dl{\tikzmarknode{ac-r-2}{A}}, \dl{B}, \tikzmarknode{a-r-2}{A}}}
{\th \dl{\tikzmarknode{ac-r-3}{A}} \lor \dl{B}, \tikzmarknode{a-r-3}{A}}}
{\prfbyaxiom{\rl{ax}}{\th \dl{\tikzmarknode{bc-r-1}{B}}, \tikzmarknode{b-r-1}{B}}}
{\th \dl{A}, \dl{\tikzmarknode{bc-r-2}{B}}, \tikzmarknode{b-r-2}{B}}}
{\th \dl{A} \lor \dl{\tikzmarknode{bc-r-3}{B}}, \tikzmarknode{b-r-3}{B}}}
{\th \dl{\tikzmarknode{ac-r-4}{A}} \lor \dl{B}, \dl{A} \lor \dl{\tikzmarknode{bc-r-4}{B}}, \tikzmarknode{a-r-4}{A} \land \tikzmarknode{b-r-4}{B}}}
{\th \dl{\tikzmarknode{ac-r-5}{A}} \lor \dl{\tikzmarknode{bc-r-5}{B}}, \tikzmarknode{a-r-5}{A} \land \tikzmarknode{b-r-5}{B}}}
\]

[remember picture, overlay, thick, blue]

([yshift=2pt]ac-l-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]a-l-1.north);
([yshift=2pt]bc-l-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]b-l-1.north);
([yshift=2pt]ac-r-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]a-r-1.north);
([yshift=2pt]bc-r-1.north) .. controls ++(0,1em) and ++(0,1em) .. ([yshift=2pt]b-r-1.north);

([yshift=2pt]ac-r-5.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (ac-r-4.south);
([yshift=2pt]ac-r-4.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (ac-r-3.south);
([yshift=2pt]ac-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (ac-r-2.south);
([shift=(2pt,2pt)]ac-r-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (ac-r-1.south);

(a-r-5.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (a-r-4.south);
(a-r-4.north) .. controls ++(0,15pt) and ++(0,-10pt) .. (a-r-3.south);
(a-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (a-r-2.south);
(a-r-2.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (a-r-1.south);

([yshift=2pt]bc-r-5.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (bc-r-4.south);
([yshift=2pt]bc-r-4.north) .. controls ++(0,7pt) and ++(0,-7pt) .. (bc-r-3.south);
([yshift=2pt]bc-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (bc-r-2.south);
([yshift=2pt]bc-r-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (bc-r-1.south);

(b-r-5.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (b-r-4.south);
(b-r-4.north) .. controls ++(0,5pt) and ++(0,-5pt) .. (b-r-3.south);
(b-r-3.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (b-r-2.south);
(b-r-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. (b-r-1.south);

The peculiarity of this graph is that it is behaves as an identity w.r.t. composition,
i.e. whatever derivation \(P\) we may cut against one of the two derivations above,
the resulting graph will be precisely that of \(P\). This is not in the least surprising
in the case of the derivation of the left, which is just an axiom hence an identity
w.r.t. cut-elimination. The situation is different for the derivation on the right,
which is not in general an identity w.r.t. cut-elimination.

The principle expressed by the derivation on the right is the syntactic invertibility
of conjunctions, i.e. the fact that any derivation \(P\) of the sequent \(\th \Gamma, A \land B\)
can be turned into a derivation \(P'\) of the same sequent whose last rule (up to some auxiliary
contraction on the context) introduces the conjunction \(A \land B\). One way to obtain
that result is precisely to cut \(P\) with the derivation on the right, then eliminate
the cut by duplicating \(P\) and commuting its copies up.

The difficulty with this formulation of the classical sequent calculus is that it contains
derivations of conjunctions whose axiom graph cannot be expressed by a derivation ending
with the conjunction rule. This is precisely the case for the left subderivation of the
counter-example described above. The result of our analysis suggests the conjecture
that drives our methodological approach: either axiom graphs are the natural semantics
of a proof system where the invertibility of logical rules is a fundamental property,
and essentially an identity, or at least we may hope to solve the problem by moving
to such a system and refining the notion of axiom graph until it becomes invariant under
inversion of logical rules.

The sequent calculus \(\data{GS4}\) (displayed in <ref>), both in full and in
its cut-free fragment, is precisely such a system. It is the one-sided presentation
of Kleene's context-sharing style calculus \(\data{G4}\) <cit.>,
where independent rule applications permute freely. It is known that, when the axioms
of \(\data{GS4}\) are restricted to atomic conclusions, the set of axioms of any derivation
is invariant under arbitrary permutations of logical rules <cit.>. The calculus
admits an elegant proof of completeness and enjoys a cut-elimination procedure <cit.>.

\begin{gather*}
\vcenter{\prfbyaxiom{\rl{ax}\ (\(\Gamma\) atomic)}{\th \Gamma, \alpha, \dl{\alpha}}}
\qquad\qquad
\vcenter{\prftree[r]{\rl{cut}}
{\prfassumption{\th \Gamma, A}}
{\prfassumption{\th \Gamma, \dl{A}}}
{\th \Gamma}}
\\[1em]
\prftree[r]{\rl{\lor}}
{\prfassumption{\th \Gamma, A, B}}
{\th \Gamma, A \lor B}
\qquad\qquad
\prftree[r]{\rl{\land}}
{\prfassumption{\th \Gamma, A}}
{\prfassumption{\th \Gamma, B}}
{\th \Gamma, A \land B}
\end{gather*}

The sequent calculus \(\data{GS4}\).

One difficulty in adopting \(\data{GS4}\) for our investigation is that every provable
sequent has a unique derivation up to permutations of logical rules. This is due to
the fact that weakenings are absorbed into the axioms and sequents are identified up
to arbitrary permutations of their elements, hence we lose in general the ability to
tell which pairs of atomic formulas are linked by the axiom:

\[
\prfbyaxiom{\rl{ax}}{\th \beta, \dl{\beta}, \alpha, \dl{\alpha}}
\quad=\quad
\prfbyaxiom{\rl{ax}}{\th \alpha, \dl{\alpha}, \beta, \dl{\beta}}
\]

In order to restore that ability we perform two steps (<ref>):

* we replace usual formulas with named formulas (<ref>),
i.e. formulas where each atomic formula occurrence is assigned a distinct name:

\[
\nm{x}{\alpha} \lor (\nm{y}{\beta} \land \nm{z}{\alpha}).
\]

It is a tedious but unfortunately necessary technical detail, as it is the only way
keep track of the history of each occurrence through the derivation;[The
alternative is the sequents-as-lists approach, which requires no modification whatsoever
to the calculus, but makes reasoning on proof transformations exceedingly complicated
because of the need to insert exchange rules everywhere.]

* we enrich the calculus with a deterministic axiom and a superposition

\[
\vcenter{\prfbyaxiom{\rl[\{\nm{x}{\alpha},\nm{y}{\dl{\alpha}}\}]{ax}}
{\th \Gamma, \nm{x}{\alpha},\nm{y}{\dl{\alpha}}}}
\qquad\qquad
\vcenter{\prftree[r]{\rl{\sqcup}}
{\prfassumption{\th \Gamma}}
{\prfassumption{\th \Gamma}}
{\th \Gamma}}
\]

We additionally allow the use of non-atomic axioms, which are interesting in that they
greatly reduce the size of derivations; this makes reasoning about the calculus a bit
more complicated, but it provides us with a nice proof of derivability of the contraction
rule (<ref>).

Deterministic axioms allow us to recover the standard form that axioms have in calculi
with explicit structural rules without losing the benefits of axioms with embedded
weakenings. They essentially provide a way to tell which formulas in the context come
from a weakening, and which ones do not. Observe that this is not a trivial addition
to \(\data{GS4}\): the complexity of checking the correctness of standard axiom rule
applications ranges from linear to quadratic in the size of the context, while for
deterministic axioms it ranges from sub-linear to linear.

The superposition rule is an adaptation of the mix-rule to the context-sharing framework.
The shape of the rule is reminiscent of the non-deterministic sums discussed earlier,
but its behaviour under cut-elimination is, as we shall see, closer to that of the
mix-rule. We choose to adopt a non-standard name for the rule to remark this fact
and avoid confusion.

In <ref> we recall the main results about the invertibility of
logical rules in \(\data{GS4}\), and introduce some related notation. We slightly depart
from standard terminology in that we speak of inversion when recovering derivations
of the premises of a logical rule, while we speak of isolation when permuting
rule applications to the bottom of the derivation. The two properties are provably equivalent,
hence they often receive the same name. In our case, however, we needed a way to distinguish
the two operations.

We are then able to formalize the axiom graph construction on the enriched calculus
(<ref>, <ref>) and show the remarkable fact that
axiom graphs are preserved under inversion of logical rules in the cut-free fragment
(<ref>). The full calculus on the other hand
fails to satisfy the same property; two counter-examples are provided in <ref> and discussed in <ref>.

This motivates us to seek a refinement of the axiom graph construction. The main problem
identified in <ref> is that the composition operator for axiom
graphs might join edges which occur in incompatible branches of the derivation, i.e. branches
that prove distinct conjuncts of some conjunction occurring in the conclusion. Thus a
path is obtained which provably cannot exist in a cut-free derivation.

Our solution is to enrich axiom graphs with labels tracking for each edge the branch it
came from: we are then able to define a branch-sensitive composition operator (<ref>).
We develop the refinement in <ref>, then show in <ref>
that the new construction is invariant under inversion of logical rules in the full fragment
of the calculus (<ref>).

Unfortunately, the refined axiom graphs are no longer preserved by the standard logical
cut-reduction steps (as defined e.g. in <cit.>). The reasons are subtle, we discuss
them briefly along with possible solutions in <ref>.

We then put our hand to developing a new normalization procedure that preserves the refined
axiom graphs. Naturally, invertibility is at the core of the procedure (described in the
proof of <ref>), which exploits it to permute all cuts up the derivation
until they are reduced to atomic contexts, i.e. they are of the form

\[
\prftree[r]{\rl{cut}}
{\prfassumption{\th \Gamma, A}}
{\prfassumption{\th \Gamma, \dl{A}}}
{\th \Gamma}
\]

where \(\Gamma\) contains only atomic formulas, while \(A\) may be arbitrarily complex.
The lack of a proper cut-reduction procedure (<ref>) forces
us to proceed from this point with a normalisation-by-evaluation argument, i.e. we show
that whenever the graph of a derivation is not empty, there is a cut-free derivation of
the same conclusion and associated to the same graph.

Such a result was essentially already available in <cit.>. We manage to restrict
the need for this kind of argument to the significantly simpler case of cuts with atomic
context between cut-free derivations. Nonetheless the main lemma (<ref>,
a kind of graph-based cut-admissibility result) still requires a very complex proof (provided
in <ref>) which a proper cut-reduction procedure,
if available, would simplify greatly.

Finally, we provide in <ref> a direct characterisation of the class of
axiom graphs that come from \(\data{GS4}\) derivations. The resulting condition, which
we call totality, is analogous to the correctness criterion of <cit.> and
provides a kind of sequentialization theorem <ref>. We exploit
this fact to devise a classical proof system (which we call \(\data{BLG}\)) optimized
for invertibility, in the sense that the inversion procedures become immediate and the
isolation procedures are just identities. Proofs in \(\data{BLG}\) have the following

\[
\makebox{\prftree
{\blgbranch{\nm{x}{\alpha}, \nm{z}{\beta}, \nm{v}{\dl{\alpha}}, \nm{w}{\gamma}}{x/v}}
{\blgbranch{\nm{x}{\alpha}, \nm{u}{\dl{\gamma}}, \nm{v}{\dl{\alpha}}, \nm{w}{\gamma}}{x/v, u/w}}
{\blgbranch{\nm{y}{\dl{\beta}}, \nm{z}{\beta}, \nm{v}{\dl{\alpha}}, \nm{w}{\gamma}}{y/z}}
{\blgbranch{\nm{y}{\dl{\beta}}, \nm{u}{\dl{\gamma}}, \nm{v}{\dl{\alpha}}, \nm{w}{\gamma}}{u/w}}
{\th \nm{x}{\alpha} \land \nm{y}{\dl{\beta}}, \nm{z}{\beta} \land \nm{u}{\dl{\gamma}}, \nm{v}{\dl{\alpha}} \lor \nm{w}{\gamma}}}
\]

i.e. a set of atomic decompositions of the conclusion together with a graph providing
the axiom links. All \(\data{GS4}\) rules, including the cut-rule, are admissible in \(\data{BLG}\).

It is important to stress how \(\data{BLG}\) is different from the \(\mathbb{B}\)-nets
of <cit.>, apart from disallowing some proofs. The question of whether a certain
formalism provides a proof system for propositional classical logic is delicate. Because
propositional tautologies are decidable in exponential time in the size of the formula,
it has been argued (e.g. in <cit.>) that correctness criteria for proofs should
have significantly lower complexity. In particular, Cook and Reckhow argue in <cit.>
that, as a minimal requirement, proofs should be checkable in polynomial time for some
adequate notion of proof size.

\(\mathbb{B}\)-nets notoriously failed to be a proof system in this sense: the only known
correctness criterion is exponential in the size of the proof object, which is itself polynomially
bounded by the size of the conclusion; moreover, Das showed that the existence of a polynomial
time correctness criterion for Andrews' matings <cit.> or for \(\mathbb{B}\)-nets
would imply \(\mathbf{NP} = \mathbf{coNP}\).

The situation is different for \(\data{BLG}\), where we are able to argue (quite informally)
that correctness is checkable in polynomial time in the size of proof objects (<ref>).
The idea is that a correctness check amounts to constructing a \(\data{GS4}\) derivation of the
same conclusion, then check that the decomposition provided by the \(\data{BLG}\) proof
object matches the one obtained through \(\data{GS4}\). Crucially, it is possible to construct
the derivation one branch at a time and thus check the correctness of the decomposition
incrementally: we are then able to show that the number of required steps is polynomially
bounded by the size of the \(\data{BLG}\) proof object.

§ TRACKING ATOM OCCURRENCES

Let us fix a countably infinite set \(\mathcal{N}\) of names and an
arbitrary set \(\mathcal{A}\) of propositional atoms, together with a fixpoint-free

\[
\sdl{(\cdot)}: \mathcal{A} \to \mathcal{A}
\]

i.e. a map such that \(\alpha \neq \dl\alpha\) and \(\dl{\dl\alpha} = \alpha\) for all
atoms \(\alpha \in \mathcal{A}\): this means that atoms come in pairs symmetrically related
by the involution. We use letters \(x, y, z, \ldots\) to range over \(\mathcal{N}\) and greek
letters \(\alpha, \beta, \gamma, \ldots\) to range over \(\mathcal{A}\).

The set \(\mathcal{F}\) of classical propositional formulas is defined by the grammar

\[
F, G \cceq \alpha \mid F \lor G \mid F \land G
\]

where \(\alpha \in \mathcal{A}\). Named formulas are formulas where every
occurrence of a propositional atom is assigned a name from the set \(\mathcal{N}\).
Formally, we define the set \(\mathcal{F^N}\) of formulas with names
in \(\mathcal{N}\) by the grammar

\[
A, B \cceq \nm{x}{\alpha} \mid A \lor B \mid A \land B
\]

where \(\alpha \in \mathcal{A}\) and \(x \in \mathcal{N}\). Call (possibly named)
formulas of the form \(\alpha\) (resp. \(\nm{x}{\alpha}\)) atomic. Each named
formula \(A \in \mathcal{F^N}\) is naturally associated to the anonymous formula \(|A|
\in \mathcal{F}\) obtained by forgetting all names. Write \(A \equiv B\) iff \(|A| = |B|\),
i.e. if \(A\) and \(B\) are identical up to a change of names.

We define as usual an involution \(\sdl{(\cdot)}: \mathcal{F} \to \mathcal{F}\) (resp.
\(\sdl{(\cdot)}: \mathcal{F^N} \to \mathcal{F^N}\)) over propositional formulas and named
formulas, expressing negation through De Morgan's duality:

\[\arraycolsep=1em
\begin{array}{ccc}
\sdl{(\alpha)} = \dl\alpha & \dl{F \lor G} = \dl{F} \land \dl{G} & \dl{F \land G} = \dl{F} \lor \dl{G}; \\[.5em]
\sdl{(\nm{x}{\alpha})} = \nm{x}{\dl\alpha} & \dl{A \lor B} = \dl{A} \land \dl{B} & \dl{A \land B} = \dl{A} \lor \dl{B}.
\end{array}
\]

Named classical propositional sequents are expressions of the form \(\th \Gamma,
\th \Delta, \ldots\) where \(\Gamma, \Delta, \ldots\) are finite sets of named
formulas. Write \(\Gamma \equiv \Delta\) (resp. \((\th \Gamma) \equiv (\th \Delta)\))
if sets \(\Gamma, \Delta\) (resp. sequents \(\th \Gamma, \th \Delta\)) are identical up
to a change of names, formally if there is a bijection \(\phi: \Gamma \to \Delta\)
such that \(A \equiv \phi A\) for all \(A \in \Gamma\).

For every named formula \(A \in \mathcal{F^N}\), let \(\data{names}(A)\) denote the set of
all names occurring in \(A\), with the obvious inductive definition. The definition extends
easily to sets and named sequents by taking unions over all their members, i.e.

\[
\data{names}(\Gamma) = \data{names}(\th \Gamma) = \bigcup_{A \in \Gamma} \data{names}(A),
\]

where \(\Gamma\) is any finite set of named formulas.

Say that named formulas \(A, B\) (resp. sets \(\Gamma, \Delta\) of formulas,
sequents \(\th \Gamma, \th \Delta\)) share names if their name sets overlap
(i.e. have non-empty intersection), otherwise say that they share no names;
in the case of formulas we may also say that they are disjoint, while we shall
not use this terminology with sets and sequents to avoid confusion with the set-theoretical
meaning of the term.

Call a named formula \(A\) sharing-free if each name appears at most once in \(A\);
formally, by structural induction, if either \(A\) is atomic or it is of the form \(B \lor C\),
\(B \land C\) where \(B, C\) are disjoint and themselves sharing-free. Call a set \(\Gamma\)
of named formulas sharing-free if all formulas in \(\Gamma\) are sharing-free and
pairwise disjoint. Call a sequent \(\th \Gamma\) sharing-free iff so is the
set \(\Gamma\).

Let \(A\) (resp. \(\Gamma\)) be a sharing-free named formula (resp. set of named
formulas). By <ref> there is for each name \(x \in \data{names}(A)\)
(resp. \(\data{names}(\Gamma)\)) a unique atom \(\alpha \in \mathcal{A}\) such that
\(\nm{x}{\alpha}\) is a subformula of \(A\) (resp. of \(\Gamma\)). We write \(A[x]\)
(resp. \(\Gamma[x]\)) to denote that unique \(\alpha\).

Note that negation preserves names when applied to named formulas, hence for all \(A \in
\mathcal{F^N}\) we have \(\data{names}(A) = \data{names}(\dl{A})\), and \(\dl{A}[x] =
\dl{A[x]}\) for all \(x \in \data{names}(A)\).

From now on we are going to assume that all named formulas and sequents be sharing-free.
As a consequence, when writing down sequents through the customary comma notation:

\[
\th \Gamma, A, B, \Delta, \ldots
\]

we shall assume implicitly that every pair of comma-separated components share no names. Observe
that disjoint formulas are necessarily distinct, and therefore any pair of sets of named formulas
sharing no names must also be disjoint in the set-theoretical sense. In particular, in the example
above, \(\Gamma, \Delta\) are disjoint, \(A \notin \Gamma\), and so on…

While named sequents are defined as sets, because of the presence of names this is
by no means equivalent to the standard sequents-as-sets approach: for example,
the sequent

\[
\th \nm{x}{\alpha}\! \land \nm{y}{\beta}, \nm{z}{\alpha}\! \land \nm{w}{\beta}
\]

contains two occurrences of the same anonymous formula, distinguished by their names.
In other words, stripping named sequents of all names results in multisets of formulas.

We now redefine the usual \(\data{GS4}\) sequent system using named sequents in place of
traditional ones. As announced before, we also enrich the system with deterministic
axioms and a superposition rule.

Named \(\data{GS4}\) derivations are finite trees whose nodes (also called rule
applications) are labeled by an inference rule and by a sharing-free named sequent (called
conclusion of the rule), inductively constructed in accordance with the following rules:

* identity rules:

\[
\prfbyaxiom{\rl[\{A,\dl{B}\}]{ax}}{\th \Gamma, A, \dl{B}}
\qquad
\prftree[r]{\rl{cut}}
{\prfassumption{\th \Gamma, A}}
{\prfassumption{\th \Gamma, \dl{A}}}
{\th \Gamma}
\]

where \(A \equiv B\);

* superposition rule:

\[
\prftree[r]{\rl{\sqcup}}
{\prfassumption{\th \Gamma}}
{\prfassumption{\th \Gamma}}
{\th \Gamma}
\]

* logical rules:

\[
\prftree[r]{\rl{\lor}}
{\prfassumption{\th \Gamma, A, B}}
{\th \Gamma, A \lor B}
\qquad
\prftree[r]{\rl{\land}}
{\prfassumption{\th \Gamma, A}}
{\prfassumption{\th \Gamma, B}}
{\th \Gamma, A \land B}
\]

Let \(\data{GS4}^\mathcal{N}\) denote the set of all named derivations; we use letters
\(P, Q, R, \ldots\) to range over \(\data{GS4}^\mathcal{N}\). We let \(\data{names}(P)\)
denote the set of all names occurring in some formula in \(P\).

The peculiar form of axiom rules is due to the fact that the pairs of formulas they relate
must share no names: because named formulas \(A\) and \(\dl{A}\) share the same
names, the conclusion of an hypothetical derivation tree of the form

\[
\prfbyaxiom{\rl[\{A, \dl{A}\}]{ax}}{\th \Gamma, A, \dl{A}}
\]

would not be sharing-free, as required by <ref>.

Correctness, completeness and cut admissibility results apply as usual: by forgetting
names one obtains a sound proof in the negative presentation of sequent calculus as
a tree of multisets of formulas, while completeness and cut admissibility can be obtained
either by adding names to anonymous proofs, or more easily by a straightforward adaptation
of Schutte's completeness proof (see <cit.>).

§ INVERSION AND ISOLATION OF LOGICAL RULES

The foremost property of \(\data{GS4}^\mathcal{N}\) derivations is the invertibility of
all logical inference rules. As is well-known, the reason why they are called invertible
is not just that their conclusions logically entail their premises; in fact, a stronger
property holds: each derivation \(P\) of \(\th \Gamma, A\) with \(A\) non-atomic may be
rewritten in such a way as to recover derivations in the context \(\Gamma\) of each premiss
of the logical rule introducing \(A\). We call this rewriting step inversion.
One may then apply the logical rule again to obtain a derivation \(P'\) of \(\th \Gamma, A\)
where the last rule application introduces \(A\): we say that \(P'\) has been obtained
by isolating \(A\) in \(P\). We state below the relevant facts and introduce some
notation; the rewriting procedures are described in detail in <ref>.

For each derivation \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma, A \lor B\),
there is a derivation \(\data{inv}(P, A \lor B) \in \data{GS4}^\mathcal{N}\) with
conclusion \(\th \Gamma, A, B\), cut-free if so is \(P\).

For each derivation \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma, A \lor B\),
there is a derivation \(\data{isl}(P, A \lor B) \in \data{GS4}^\mathcal{N}\) with the same
conclusion, cut-free if so is \(P\), and whose last rule application introduces \(A \lor B\).

Let \(\data{isl}(P, A \lor B)\) be the derivation

\[
\prftree[r]{\rl{\lor}}
{\prfsummary[\(\data{inv}(P, A \lor B)\)]{\th \Gamma, A, B}}
{\th \Gamma, A \lor B}
\qedhere
\]

For each derivation \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma,
A \land B\), there is a derivation \(\data{inv_l}(P, A \land B) \in \data{GS4}^\mathcal{N}\)
with conclusion \(\th \Gamma, A\), cut-free if so is \(P\).

For each derivation \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma,
A \land B\), there is a derivation \(\data{inv_r}(P, A \land B) \in \data{GS4}^\mathcal{N}\)
with conclusion \(\th \Gamma, B\), cut-free if so is \(P\).

For each derivation \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma,
A \land B\), there is a derivation \(\data{isl}(P, A \land B) \in \data{GS4}^\mathcal{N}\)
with the same conclusion, cut-free if so is \(P\), and whose last rule application
introduces \(A \land B\).

Let \(\data{isl}(P, A \land B)\) be the derivation

\[
\prftree[r]{\rl{\land}}
{\prfsummary[\(\data{inv_l}(P, A \land B)\)]{\th \Gamma, A}}
{\prfsummary[\(\data{inv_r}(P, A \land B)\)]{\th \Gamma, B}}
{\th \Gamma, A \land B}
\qedhere
\]

§.§ Admissibility of contraction and weakening

For each derivation \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma\)
and sharing-free set \(\Delta\) of named formulas such that \(\Gamma, \Delta\)
share no names, there is a derivation \(\data{wk}(P, \Delta) \in \data{GS4}^\mathcal{N}\)
with conclusion \(\th \Gamma, \Delta\), cut-free if so is \(P\).

The contraction rule is derivable through the use of cuts, and therefore admissible:

\[
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, B}}
{\prfbyaxiom{\rl[\{A,\dl{B}\}]{ax}}{\th \Gamma, A, \dl{B}}}
{\th \Gamma, A}}
\qquad
(A \equiv B)
\]

On the other hand, the weakening rule is not derivable because of the way the cut rule is
formulated in \(\data{GS4}\) (i.e. with context sharing).

§ AXIOM GRAPHS

We are now ready to formalize the idea of axiom-induced graphs. We shall rely on a standard
notion of simple graph: the related notation and properties are summarized in <ref>.
We start from the notion of name graph, i.e. a simple graph whose vertex set is a subset
of the set \(\mathcal{N}\) of names. We associate a name graph to each derivation; following
the intuitions given in the introduction, only axioms and cuts will receive a special treatment,
while all other rules shall be interpreted trivially by graph unions.

For any sharing-free set \(\Gamma\) of named formulas, let \(\data{Wk}_\Gamma\)
denote the graph

\[
\data{Wk}_\Gamma = \langle \data{names}(\Gamma), \emptyset \rangle
\]

whose vertices are the names occurring in \(\Gamma\) and whose edge set is empty.
We call \(\data{Wk}_\Gamma\) the edgeless or weakening graph on \(\Gamma\).

For any pair \(A, \dl{B}\) of disjoint and sharing-free named formulas such that
\(A \equiv B\), we define by induction on the height[Which is necessarily
identical to the height of \(B\), see <ref> from <ref>.]
of \(A\) the graph \(\data{Id}_{\{A, \dl{B}\}}\):

\begin{gather*}
\data{Id}_{\{\nm{x}{\alpha}, \nm{y}{\dl\alpha}\}} = \langle \{x,y\}, \{xy\} \rangle;\\[.5em]
\data{Id}_{\{A_1 \lor A_2, \dl{B}_1 \land \dl{B}_2\}} =
\data{Id}_{\{A_1 \land A_2, \dl{B}_1 \lor \dl{B}_2\}} =
\data{Id}_{\{A_1, \dl{B}_1\}} \sqcup \data{Id}_{\{A_2, \dl{B}_2\}}.
\end{gather*}

We call \(\data{Id}_{\{A, \dl{B}\}}\) the identity graph on \(A, \dl{B}\).
It is easy to check by induction on \(A\) that \(V_{\data{Id}_{\{A, \dl{B}\}}} =
\data{names}(\{A, \dl{B}\})\).

In order to interpret cuts, we need to implement the informal idea of paths alternating between
the two cut subderivations through the cut-formula. The implementation is independent of the
logical framework and can be specified directly in terms of name graphs:

Let \(G, H\) be arbitrary name graphs, \(I \subseteq \mathcal{N}\) a set of names
called interface. Furthermore, let \(x_1, \ldots, x_n \in V_G \cup V_H\) be
a sequence of pairwise distinct vertices from \(G, H\) (for some \(n > 0\)),
and let \(e_i\) denote the unordered pair \(x_i x_{i+1}\) for all \(1 \leq i < n\).

\(x_1, \ldots, x_n\) is an alternating path between \(G\) and \(H\) through
the interface \(I\) if and only if

* \(x_i \in I\) for all \(1 < i < n\) (those we call internal vertices of
the path);

* either \(e_i \in E_G\) for all odd \(1 \leq i < n\) and \(e_i \in E_H\) for
all even \(1 \leq i < n\), or \(e_i \in E_H\) for all odd \(1 \leq i < n\) and \(e_i
\in E_G\) for all even \(1 \leq i < n\).

In other words, alternating paths are built by choosing ‘adjacent’ edges alternately in \(G\)
and \(H\) or vice versa, under the restriction that all vertices except the first and
the last be in the interface. Observe that cycles are ignored – since vertices in the
path are required to be pairwise distinct – hence when \(G\) and \(H\) are finite, there
are for any given interface only finitely many alternating paths between them.

Given name graphs \(G, H\) and a set of names \(I \subseteq \mathcal{N}\), we define
the composite of \(G\) and \(H\) on interface \(I\) as the graph

\[
G \odot_I H = \langle V, E \rangle
\]

\[
V = (V_G \cup V_H) \setminus I
\]

and for all \(x \neq y \in V\), \(xy \in E\) if and only if there is an alternating path
\(z_1, \ldots, z_n\) between \(G\) and \(H\) through the interface \(I\) such that
\(z_1 = x\) and \(z_n = y\).

From now on, given any name graphs \(G, H\) and a named formula \(A\), we may write
\(G \odot_A H\) as a shorthand for \(G \odot_{\data{names}(A)} H\).

To each derivation tree \(P \in \data{GS4}^\mathcal{N}\) we associate a named graph \(\axg{P}\),
called axiom graph of \(P\), defined by structural induction on \(P\):

* if \(P\) has the form

\[
\prfbyaxiom{\rl[\{A, \dl{B}\}]{ax}}
{\th \Gamma, A, \dl{B}}
\]

where \(A \equiv B\), then let \(\axg{P} = \data{Wk}_\Gamma \sqcup \data{Id}_{\{A,\dl{B}\}}\);

* if \(P\) has the form

\[
\prftree[r]{\rl{cut}}
{\prfsummary[\(Q\)]{\th \Gamma, A \vphantom{\dl{A}}}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{A}}}
{\th \Gamma}
\]

then let \(\axg{P} = \axg{Q} \odot_A \axg{R}\);

* if \(P\) has the form

\[
\prftree[r]{\(r\)}
{\prfsummary[\(Q_1\)]{\th \Gamma_1}}
{\prfsummary[\(Q_n\)]{\th \Gamma_n}}
{\th \Gamma}
\]

where \(r \in \{\rl{\sqcup}, \rl{\lor}, \rl{\land}\}\), then let
\(\axg{P} = \axg{Q_1} \sqcup \ldots \sqcup \axg{Q_n}\).

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma\),

\[
V_{\axg{P}} = \data{names}(\Gamma).
\]

§.§ Axiom graphs do not increase under inversion and isolation

Let \(P \in \data{GS4}^\mathcal{N}\) be any named derivation tree with conclusion \(\th \Gamma, A\),
where \(A\) is any non-atomic named formula: then

\[
\axg{\data{isl}(P, A)} \sqsubseteq \axg{P}.
\]

From now on, and especially in the statements and proofs of the following lemmas, we shall
write expressions of the form \(\axg{P} \rst_{\Gamma, A}\) as a shorthand for \(\axg{P}
\rst_{\data{names}(\Gamma, A)}\) (see <ref> for the subgraph relation and
the graph restriction notation). All omitted proofs can be found in <ref>.

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma, A \lor B\),

\[
\axg{\data{inv}(P, A \lor B)} = \axg{P}.
\]

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma, A \land B\),

\[
\axg{\data{inv_l}(P, A \land B)} \sqsubseteq \axg{P} \rst_{\Gamma, A} \text{ and }
\axg{\data{inv_r}(P, A \land B)} \sqsubseteq \axg{P} \rst_{\Gamma, B};
\]

Immediate consequence of <ref> together with the definition of
the \(\data{isl}\)-transformation (<ref>). The result may also be seen as a very specific
instance of a more general one by Führmann and Pym <cit.>.

§.§ Axiom graphs are not invariants of isolation and normalisation

The inequality from <ref> can be upgraded to an equality in the
case of cut-free proofs:

For all cut-free derivations \(P \in \data{GS4}^\mathcal{N}\) of the sequent \(\th \Gamma, A\)
with \(A\) non-atomic,

\[
\axg{\data{isl}(P, A)} = \axg{P}.
\]

On the other hand, the invariance result does not hold in the case of proofs with cuts,
as there are derivations whose axiom graph decreases strictly under isolation of some conjunction
in their conclusions. <Ref> shows one such counterexample,
where there is an alternating path (marked in blue in <ref>)
that is lost as soon as the conjunction in the conclusion is isolated, as shown in

The unstable path in <ref> is precisely the one that
connects names occurring on the two distinct sides of a conjunction: in fact, it is possible
to prove that no such edge may exist in a cut-free derivation, hence the axiom graph construction
cannot be invariant under cut-elimination.

One might be tempted to modify the construction so that conjunction-crossing paths be erased
as soon as possible; this, however, is not enough to guarantee invariance under isolation.
<Ref> shows a more complex example where an alternating
path is lost, whose endpoints are not separated by a conjunction. The problem in this case
is that the disappearing path contains edges coming from subderivations of both conjuncts
of a conjunction that appears in the conclusion. As soon as the conjunction is isolated
(<ref>), it becomes impossible to construct such
a path.

§ BRANCH-LABELED AXIOM GRAPHS

Our solution is to refine the axiom graph construction by attaching labels to each edge,
whose purpose is to track the branches each edge came from in the interpreted derivation.
We do this by replacing the edge set with a relation associating sets of names (representing
branches of derivations) to unordered pairs of vertices (representing unoriented edges).
Every edge must come from some branch: if some pair of vertices has no associated name set,
then we consider there to be no edge between the two vertices. We then use the additional
information to discard alternating paths composed by edges belonging to incompatible branches.

§.§ Naming branches

It is a well-known fact <cit.> that when the axiom rule is restricted to atomic
conclusions, the set of axiom rule conclusions (also called top-sequents) of any given
\(\data{GS4}\) derivation is uniquely determined by the conclusion of the derivation.
For obvious reasons, every branch is terminated by a unique axiom-rule application and can
then be named by its conclusion – in fact it is sufficient to consider the set of names that
occur in the leaf's conclusion. In the presence of superposition rules the naming will not be
unique, but this is not a problem as identically named branches can be collapsed into one
by reducing superpositions to atomic form.

In order to ensure that branch names be stable under isolation, we need to take into account
the possible expansions of non-atomic axioms: branches terminated by such rule applications
correspond in fact to multiple “virtual” atomic branches, still uniquely determined by the
leaf's conclusion. We need then to define the unique set \(\data{Br}(\Gamma)\) of atomic
branch names determined by a given sequent \(\th \Gamma\). One possible approach – followed
e.g. in <cit.> – is to rely upon \(\data{GS4}\) inference rules to obtain the unique
atomic decomposition of the sequent; we prefer however to provide a direct characterisation
of the set \(\data{Br}(\Gamma)\), then show that it is compatible with the inference rules.

We associate inductively a set of branch names to each sharing-free named formula \(A\)
as follows:

* \(\data{Br}(\nm{x}{\alpha}) = \{\{x\}\}\);

* \(\data{Br}(B \lor C) = \{ X \cup Y \mid X \in \data{Br}(B), Y \in \data{Br}(C) \}\);

* \(\data{Br}(B \land C) = \data{Br}(B) \cup \data{Br}(C)\);

then let, for all sharing-free sets \(\Gamma\) of named formulas,

\[
\data{Br}(\Gamma) = \{ X \subseteq \data{names}(\Gamma) \mid \forall A \in \Gamma.\,(X \cap \data{names}(A)) \in \data{Br}(A) \}.
\]

The construction for sets is meant to treat them as generalized disjunctions over their elements.
While syntactic binary disjunction distinguishes between a left and a right subformula, elements
of a set have no preferred ordering, hence the need for a slightly less straightforward definition.
We provide for clarity an alternative characterisation of \(\data{Br}(\Gamma)\) (as usual
we provide detailed proofs in <ref>):

Let \(\Gamma\) be any sharing-free set of named formulas. For any branch name \(X
\subseteq \mathcal{N}\), \(X \in \data{Br}(\Gamma)\) if and only if there is a family
\((X_A)_{A \in \Gamma}\) of branch names such that \(X = \bigcup_{A \in \Gamma} X_A\),
with \(X_A \in \data{Br}(A)\) for all \(A \in \Gamma\).

Let \(\Gamma, \Delta\) be sharing free sets of named formulas that share no names:

\[
\data{Br}(\Gamma \cup \Delta) = \{ X \cup Y \mid X \in \data{Br}(\Gamma), Y \in \data{Br}(\Delta) \}.
\]

\(\data{Br}(\Gamma) = \{ X \setminus \data{names}(\Delta) \mid X \in \data{Br}(\Gamma \cup \Delta) \}\).

It is an easy consequence of <ref> that \(\data{Br}(\{A\}) =
\data{Br}(A)\). Therefore, from this point on we are going to abuse systematically the usual
sequent notation and write, e.g., \(\data{Br}(\Gamma, A, \Delta)\) for \(\data{Br}(\Gamma \cup
\{A\} \cup \Delta)\).

Let \(\Gamma\) be any sharing-free set of named formulas, \(A, B\) disjoint and sharing-free
named formulas that share no name with \(\Gamma\):

* if all formulas in \(\Gamma\) are atomic, then \(\data{Br}(\Gamma) = \{\data{names}(\Gamma)\}\);

* \(\data{Br}(\Gamma, A \lor B) = \data{Br}(\Gamma, A, B)\);

* \(\data{Br}(\Gamma, A \land B) = \data{Br}(\Gamma, A) \cup \data{Br}(\Gamma, B)\);

* \(\data{Br}(\Gamma, A)\) and \(\data{Br}(\Gamma, B)\) are disjoint.

§.§ Branch-labeled name graphs

A branch-labeled name graph is a pair \(G = \langle V_G, {\adin_G} \rangle\) where
\(V_G \subseteq \mathcal{N}\) is a set of names and

\[
{\adin_G} \subseteq \binom{V_G}{2} \times \pwr(V_G)
\]

is a binary relation between unordered pairs of vertices and arbitrary sets of vertices
of \(G\), such that

\begin{equation}
e \adin_G X \implies e \subseteq X. \tag{\(\star\)}\label{eqn:edge-branch-inclusion}
\end{equation}

For \(G\) any branch-labeled name graph (hereinafter bl-graph for brevity), we can
define a set

\[
E_G = \pi_{\data{l}}({\adin_G}) = \{ e \mid \exists X.\ e \adin_G X \}
\]

of unordered pairs of vertices which we shall call the edges of \(G\). We define
similarly the set of branches of \(G\):

\[
\data{Br}(G) = \pi_{\data{r}}({\adin_G}) = \{ X \mid \exists e.\ e \adin_G X \}.
\]

We read the predicate \(xy \adin_G X\) as \(x, y\) are adjacent in branch \(X\),
or branch \(X\) has the edge \(xy\). Condition (<ref>)
ensures that edges only connect vertices belonging to the branch they originated in.

We extend the subgraph relation and the union operator to bl-graphs simply by replacing the
edge set with the edge-branch relation in the definition, i.e. let

\[
G \sqsubseteq H \iff V_G \subseteq V_H \text{ and } {\adin_G} \subseteq {\adin_H}
\]

for all pairs \(G, H\) of bl-graphs, and

\[
\bigsqcup_{i \in I} G_i = \langle \bigcup_{i \in I} V_{G_i}, \bigcup_{i \in I} {\adin_{G_i}} \rangle
\]

where \(I\) is any index set and \((G_i)_{i \in I}\) an indexed family of bl-graphs. The
restriction operator must be modified slightly so as to select branches instead of edges:
for \(G\) any bl-graph and \(X \subseteq \mathcal{N}\), let

\[
G \rst_X = \langle V_G \cap X, \{ (e, Y) \in {\adin_G} \mid Y \subseteq X \} \rangle.
\]

Note that while union acts upon edges in the usual way (we have \(E_{G \sqcup H} = E_G
\cup E_H\)), restriction might remove more edges than in the case of simple graphs:
for all \(e \in E_G\), \(e \in E_{G \rst_X}\) implies \(e \subseteq X\), but the converse
does not hold in general.

§.§ Branch-sensitive composition

We come thus to the crux of the refined approach – the composition of bl-graphs over
some interface. Remember that composition is meant to interpret cuts between derivations
\(P, Q\) of conclusion \(\th \Gamma, A\) and \(\th \Gamma, \dl{A}\) respectively, with the
cut rule having conclusion \(\th \Gamma\). We start then with atomic branch sets \(\data{Br}(
\Gamma, A)\), \(\data{Br}(\Gamma, \dl{A})\), while the branch set of the final cut-free
derivation will be \(\data{Br}(\Gamma)\). When constructing alternating paths, we are going
to use edges which come in general from different branches in \(P, Q\), but we need to ensure
that they all belong to the same branch of the cut-free derivation, otherwise they might
disappear under isolation.

To this end, observe that by <ref> all branches \(X \in \data{Br}(
\Gamma, A)\) (resp. \(\data{Br}(\Gamma, \dl{A})\)) are of the form \(Y \cup Z\) where \(Y \in
\data{Br}(\Gamma)\) and \(Z \in \data{Br}(A)\) (resp. \(\data{Br}(\dl{A})\)). Therefore,
we have \(X \setminus \data{names}(A) = X \setminus \data{names}(\dl{A}) \in \data{Br}(\Gamma)\)
(<ref>). The idea is then to check that all edges forming an
alternating path share the same branch label up to names in the composition interface.

For any bl-graph \(G\) and set \(I \subseteq \mathcal{N}\) of names, we define an
interface-relativized edge-branch relation

\[
{\adin^I_G} = \{ (e, X \setminus I) \mid e \adin_G X \},
\]

or equivalently

\[
e \adin^I_G X \iff \exists Y.\,e \adin_G Y \text{ and } X = Y \setminus I.
\]

Let \(G, H\) be arbitrary bl-graphs, \(I, X \subseteq \mathcal{N}\) sets of names,
\(x_1, \ldots, x_n \in V_G \cup V_H\) a sequence of pairwise distinct vertices
from \(G, H\) (with \(n > 1\)), and let \(e_i\) denote the unordered pair \(x_i x_{i+1}\)
for all \(1 \leq i < n\).

\(x_1, \ldots, x_n\) is an alternating \(X\)-labeled path between \(G\) and \(H\)
through the interface \(I\) if and only if

* \(x_i \in I\) for all \(1 < i < n\) (all internal vertices belong to the interface);

* either \(e_i \adin^I_G X\) for all odd \(1 \leq i < n\) and \(e_i \adin^I_H X\)
for all even \(1 \leq i < n\), or \(e_i \adin^I_H X\) for all odd \(1 \leq i < n\) and
\(e_i \adin^I_G X\) for all even \(1 \leq i < n\).

We call the path complete iff \(x_1, x_n \notin I\).

If \(z_1, \ldots, z_n\) is a complete \(X\)-labeled alternating path between
bl-graphs \(G, H\) through interface \(I\), then \(z_1, z_n \in X\).

By <ref> \(n > 1\), hence there is \(K \in \{G, H\}\)
and \(Y \in \data{Br}(K)\) such that \(z_1 z_2 \adin_K Y\) with \(X = Y \setminus I\).
By <ref> \(z_1 z_2 \subseteq Y\), and because \(z_1 \notin I\) by
hypothesis, we must have \(z_1 \in X\). Similar reasoning shows that \(z_n \in X\).

Let \(G, H\) be arbitrary bl-graphs, \(I \subseteq \mathcal{N}\) a set of names.
We define the composite of \(G\) and \(H\) on interface \(I\) as the bl-graph

\[
G \odot_I H = \langle V, {\adin} \rangle
\]

\[
V = (V_G \cup V_H) \setminus I
\]

and for all \(x \neq y \in V\) and \(X \subseteq V\), \(xy \adin X\) if and only if there
is a complete alternating \(X\)-labeled path \(z_1, \ldots, z_n\) between \(G\) and \(H\)
through the interface \(I\), such that \(z_1 = x\) and \(z_n = y\).
<Ref> guarantees that \(xy \subseteq X\).

§.§ Interpreting derivations

Finally, we define the new inductive interpretation function for derivations. Special attention
must be paid to the weakening case: it is not possible to handle it by a simple graph union,
like in the original axiom graph construction, as we need to update all branch labels to take
weakened formulas into account. Weakenings are then interpreted by an operator on bl-graphs.
Identities also need to be tweaked to account for the way non-atomic axioms are expanded by the
inversion procedures.

For any bl-graph \(G\) and sharing-free set \(\Gamma\) of named formulas, let

\[
\blwk{\Gamma}(G) = \langle V_G \cup \data{names}(\Gamma), \{ (e, X \cup Y) \mid e \adin_G X,\,Y \in \data{Br}(\Gamma) \} \rangle.
\]

For any pair \(A, \dl{B}\) of disjoint and sharing-free named formulas such that
\(A \equiv B\), we define by induction on the height of \(A\) the bl-graph \(\blid{\{A, \dl{B}\}}\):

\begin{gather*}
\blid{\{\nm{x}{\alpha}, \nm{y}{\dl{\alpha}}\}} = \langle \{x, y\}, \{ (xy, \{x, y\}) \} \rangle;\\
\blid{\{A_1 \lor A_2, \dl{B}_1 \land \dl{B}_2\}}
= \blwk{A_2}(\blid{\{A_1, \dl{B}_1\}}) \sqcup \blwk{A_1}(\blid{\{A_2, \dl{B}_2\}}).
\end{gather*}

To each derivation tree \(P \in \data{GS4}^\mathcal{N}\) we associate a bl-graph \(\blaxg{P}\),
called branch-labeled axiom graph of \(P\), defined by structural induction on \(P\):
if \(P\) has the form

\[
\prfbyaxiom{\rl[\{A, \dl{B}\}]{ax}}
{\th \Gamma, A, \dl{B}}
\]

where \(A \equiv B\), then let \(\blaxg{P} = \blwk{\Gamma}(\blid{\{A,\dl{B}\}})\);
as for simple axiom graphs, cuts are interpreted by composition and all other rules
by taking the bl-graph union over their subderivations.

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma\),

\[
V_{\blaxg{P}} = \data{names}(\Gamma) \text{ and } \data{Br}(\blaxg{P}) \subseteq \data{Br}(\Gamma).
\]

§ MAIN RESULTS

§.§ Behaviour under inversion and isolation

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma, A\),
where \(A\) is any non-atomic named formula,

\[
\blaxg{\data{isl}(P, A)} = \blaxg{P}.
\]

The proof of <ref> rests upon the following three lemmas,
whose proofs are detailed in <ref>.

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma, A \lor B\),

\[
\blaxg{\data{inv}(P, A \lor B)} = \blaxg{P}.
\]

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma, A \land B\),

\[
\blaxg{\data{inv_l}(P, A \land B)} = \blaxg{P} \rst_{\Gamma, A} \text{ and }
\blaxg{\data{inv_r}(P, A \land B)} = \blaxg{P} \rst_{\Gamma, B};
\]

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma, A \land B\),

\[
\blaxg{P} = \blaxg{P} \rst_{\Gamma, A} \cup \blaxg{P} \rst_{\Gamma, B}.
\]

Immediate by <ref> if \(A\) is a disjunction.
If instead \(A = B \land C\) is a conjunction, we have by construction[See
the proof of <ref>.]

\[
\blaxg{\data{isl}(P, A)} = \blaxg{\data{inv_l}(P, A \land B)} \sqcup \blaxg{\data{inv_r}(P, A \land B)}
\]

and then by <ref>

\[
\blaxg{\data{inv_l}(P, A \land B)} \sqcup \blaxg{\data{inv_r}(P, A \land B)}
= {\blaxg{P} \rst_{\Gamma, B}} \sqcup {\blaxg{P} \rst_{\Gamma, C}} = \blaxg{P}. \qedhere
\]

§.§ Cut-elimination theorem

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma\),
there is a cut-free derivation \(Q \in \data{GS4}^\mathcal{N}\) with conclusion
\(\th \Gamma\) and such that \(\blaxg{P} = \blaxg{Q}\).

Since we lack a cut-reduction procedure compatible with the interpretation, we have
to prove <ref> through a normalisation-by-evaluation argument,
where we first compute the interpretation of the derivation, then reconstruct a cut-free
derivation with the same interpretation.

However, thanks to <ref>, we can employ the isolation
procedure to commute cuts up the derivation until they are reduced to atomic contexts.
We are thus able to limit the need for evaluation to the very specific and much simpler
case of quasi-cut-free derivations[I.e., those formed by cutting together
two cut-free derivations] with atomic conclusion.

The proof then looks like a standard cut-elimination argument, with a lemma for the quasi-cut-free
case and a final general argument by induction on the height of the derivation. We start
with a kind of semantic cut-admissibility result. All omitted proofs are provided as usual
in <ref>, except that of <ref>
to which we devote the whole of <ref> because of its

Let \(P \in \data{GS4}^\mathcal{N}\) be any derivation with conclusion \(\th \Gamma\).
All edges in \(\blaxg{P}\) link dual atom occurrences, i.e. for all \(xy \in E_{\blaxg{P}}\)
we have \(\Gamma[x] = \dl{\Gamma[y]}\).

Let \(P, Q \in \data{GS4}^\mathcal{N}\) be cut-free derivations with conclusion
\(\th \Gamma, A\) and \(\th \Gamma, \dl{A}\) respectively, where all elements of
the context \(\Gamma\) are atomic formulas. Then the composite bl-graph \(\blaxg{P}
\odot_A \blaxg{Q}\) has at least one edge.

Let \(P, Q \in \data{GS4}^\mathcal{N}\) be cut-free derivations with conclusion
\(\th \Gamma, A\) and \(\th \Gamma, \dl{A}\) respectively, where all elements of
the context \(\Gamma\) are atomic formulas. There is a cut-free derivation \(R \in
\data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma\) and such that \(\blaxg{R} =
\blaxg{P} \odot_A \blaxg{Q}\).

For brevity, let \(G = \blaxg{P} \odot_A \blaxg{Q}\). Observe that the vertex set of \(G\)
is finite by <ref>, hence \(G\) has finitely many edges.
Moreover, \(\data{Br}(G) \subseteq \data{Br}(\Gamma) = \{\data{names}(\Gamma)\}\)
(<ref>), i.e. all edges have the same branch
label \(\data{names}(\Gamma)\). Finally, by <ref> and
the assumption that \(\Gamma\) is atomic, there are for all edges \(xy \in E_G\)
named formulas \(\nm{x}{\alpha}, \nm{y}{\dl{\alpha}} \in \Gamma\) where \(\alpha =
\Gamma[x]\) and \(\dl{\alpha} = \Gamma[y]\).

Now let \(|E_G|\) denote the number of edges in \(G\): by <ref>
we know that \(|E_G| > 0\). We construct the derivation \(R\) by induction on \(n\):

* if \(|E_G| = 1\), then there is a unique edge \(xy \in E_G\): let \(\alpha
= \Gamma[x]\), and let \(R\) be the derivation

\[
\prfbyaxiom{\rl[\{\nm{x}{\alpha}, \nm{y}{\dl{\alpha}}\}]{ax}}{\th \Gamma}
\]

* if \(|E_G| > 1\), then there is at least one edge \(xy \in E_G\) and we can
decompose \(G\) as \(G' \sqcup G''\), where

\[
G' = \langle V_G, \{ (xy, \data{names}(\Gamma)) \} \rangle
\text{ and }
G'' = \langle V_G, {\adin_G} \setminus \{ (xy, \data{names}(\Gamma)) \} \rangle.
\]

We have obviously \(|E_{G'}|, |E_{G''}| < |E_G|\), hence there are by induction
hypothesis derivations \(R', R''\) with conclusion \(\th \Gamma\) and such that
\(\blaxg{R'} = G'\), \(\blaxg{R''} = G''\): let then \(R\) be the derivation

\[
\prftree[r]{\rl{\sqcup}}
{\prfsummary[\(R'\)]{\th \Gamma}}
{\prfsummary[\(R''\)]{\th \Gamma}}
{\th \Gamma}
\]

Readers may check easily – using the facts recalled above –  that \(\blaxg{R} = G\),
as required.

We come finally to the general cut-elimination proof, but first we must handle an important
technical detail. Because the isolation procedure might expand axioms, it does not preserve
in general the height of the derivation, hence we cannot proceed by induction on that
measure. We define instead an alternative measure called virtual height, which
provides an upper bound to the height that may be attained by expanding the axioms, and
therefore does not increase under isolation:

For any derivation \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma\),

* if \(P\) ends with an axiom rule application, let \(\data{vh}(P) = 1 +
\data{deg}(\Gamma)\) (<ref>);

* otherwise \(P\) has the form

\[
\prftree[r]{\(r\)}
{\prfsummary[\(P_1\)]{\th \Gamma_1}}
{\prfsummary[\(P_n\)]{\th \Gamma_n}}
{\th \Gamma}
\]

where \(r \in \{\rl{cut}, \rl{\sqcup}, \rl{\lor}, \rl{\land}\}\): let then
\(\data{vh}(P) = 1 + \max_{i = 1}^n \data{vh}(P_i)\).

Let \(P \in \data{GS4}^\mathcal{N}\) be any derivation with conclusion \(\th \Gamma, A\)
where \(A\) is non-atomic; then \(\data{vh}(\data{isl}(P, A)) \leq \data{vh}(P)\).

If \(P\) is cut-free, let \(Q = P\). Otherwise, proceed by induction on the virtual
height of \(P\):

* if \(P\) has the form

\[
\prftree[r]{\(r\)}
{\prfsummary[\(P_1\)]{\th \Gamma_1}}
{\prfsummary[\(P_n\)]{\th \Gamma_n}}
{\th \Gamma}
\]

where \(r \in \{\rl{\sqcup}, \rl{\lor}, \rl{\land}\}\), then apply the induction
hypothesis to \(P_1, \ldots, P_n\) to get cut-free derivations \(Q_1, \ldots, Q_n\)
with the same conclusion as \(P_1, \ldots, P_n\) respectively, and let \(Q\) be the
cut-free derivation

\[
\prftree[r]{\(r\)}
{\prfsummary[\(Q_1\)]{\th \Gamma_1}}
{\prfsummary[\(Q_n\)]{\th \Gamma_n}}
{\th \Gamma}
\]

We have \(\blaxg{Q_i} = \blaxg{P_i}\) for all \(1 \leq i \leq n\) and therefore
\(\blaxg{Q} = \bigsqcup_{i = 1}^n \blaxg{Q_i} = \bigsqcup_{i = 1}^n \blaxg{P_i} = \blaxg{P}\),
as required;

* if \(P\) has the form

\[
\prftree[r]{\rl{cut}}
{\prfsummary{\th \Gamma, B, A \vphantom{\dl{A}}}}
{\prfsummary{\th \Gamma, B, \dl{A}}}
{\th \Gamma, B}
\]

where \(B\) is non-atomic, there is a derivation \(P' = \data{isl}(P, B)\) of the form

\[
\prftree[r]{\(r\)}
{\prfsummary[\(P'_1\)]{\th \Gamma_1}}
{\prfsummary[\(P'_n\)]{\th \Gamma_n}}
{\th \Gamma, B}
\]

where the last rule application \(r \in \{\rl{\lor}, \rl{\land}\}\) introduces
the formula \(B\), and such that \(\blaxg{P'} = \blaxg{P}\) (<ref>)
and \(\data{vh}(P') \leq \data{vh}(P)\) (<ref>): we can
then apply the induction hypothesis to the \(P'_i\) and proceed as in the previous
case to get a cut-free derivation \(Q\) such that \(\blaxg{Q} = \blaxg{P'} = \blaxg{P}\);

* finally, if \(P\) has the form

\[
\prftree[r]{\rl{cut}}
{\prfsummary[\(P_1\)]{\th \Gamma, A \vphantom{\dl{A}}}}
{\prfsummary[\(P_2\)]{\th \Gamma, \dl{A}}}
{\th \Gamma}
\]

where all elements of \(\Gamma\) are atomic formulas, we apply first the induction
hypothesis to \(P_1, P_2\) to get cut-free derivations \(Q_1, Q_2\) with the same
conclusions and such that \(\blaxg{Q_i} = \blaxg{P_i}\) for \(i \in \{1,2\}\).
We can now apply <ref> to \(Q_1, Q_2\) to get
a cut-free derivation \(Q\) such that \(\blaxg{Q} = \blaxg{Q_1} \odot_A \blaxg{Q_2}
= \blaxg{P_1} \odot_A \blaxg{P_2} = \blaxg{P}\).

§ TOTALITY AND CANONICAL FORMS

The availability of a cut-elimination procedure that preserves branch-labeled axiom graphs
unlocks a powerful technique for proving properties of the interpretation: we can reason
about cut-free derivations and the result generalizes immediately to all derivations.
An important example is the following property, which together with the one described
in <ref> characterises the class of bl-graphs induced by
derivations in \(\data{GS4}^\mathcal{N}\).

For all cut-free derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma\),

\[
\data{Br}(\blaxg{P}) = \data{Br}(\Gamma).
\]

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma\),

\[
\data{Br}(\blaxg{P}) = \data{Br}(\Gamma).
\]

<Ref> guarantees the existence of a cut-free derivation \(Q\) such
that \(\blaxg{Q} = \blaxg{P}\), to which we can apply <ref>.

Call a bl-graph \(G\) total w.r.t. a sharing-free named sequent \(\th \Gamma\)
if and only if

* \(V_G = \data{names}(\Gamma)\) (\(G\) is a bl-graph on the names of \(\Gamma\));

* \(\data{Br}(G) = \data{Br}(\Gamma)\) (the branches of \(G\) are those of \(\Gamma\));

* for all \(xy \in E_G\), \(\Gamma[x] = \dl{\Gamma[y]}\) (the edges of \(G\) link dual atoms).

For all derivations \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma\),
\(\blaxg{P}\) is total w.r.t. \(\th \Gamma\).

Immediate consequence of <ref>.

Let \(G\) be any bl-graph that is total w.r.t. a sharing-free named sequent \(\th \Gamma\):
there is a derivation \(P \in \data{GS4}^\mathcal{N}\) with conclusion \(\th \Gamma\)
and such that \(\blaxg{P} = G\).

Any bl-graph \(G\) total w.r.t. \(\th \Gamma, A \lor B\) is also total w.r.t. \(\th \Gamma, A, B\).

Any bl-graph \(G\) total w.r.t. \(\th \Gamma, A \land B\) is decomposable as

\[
G = {G \rst_{\Gamma, A}} \sqcup {G \rst_{\Gamma, B}},
\]

with \(G \rst_{\Gamma, A}\) and \(G \rst_{\Gamma, B}\) total w.r.t. \(\th \Gamma, A\)
and \(\th \Gamma, B\), respectively.

By induction on the complexity degree of \(\th \Gamma\) (<ref>,
<ref>). Observe first that \(\Gamma\) cannot be empty, because then \(G\)
would be the empty graph and we would have \(\data{Br}(G) = \emptyset \neq \{\emptyset\}
= \data{Br}(\Gamma)\), contradicting the totality of \(G\) w.r.t. \(\Gamma\); then:

* if \(\th \Gamma\) only contains atomic formulas, we can perform the construction
described in the proof of <ref>;

* if \(\th \Gamma = \th \Delta, A \lor B\), then \(G\) is total w.r.t.
\(\th \Delta, A, B\) by <ref>: we apply
the induction hypothesis to get a derivation \(Q\) with conclusion \(\th \Delta, A, B\)
and such that \(\blaxg{Q} = G\); we conclude by applying a disjunction rule to \(Q\):

\[
\prftree[r,l]{\rl{\lor}}{\(P =\)}
{\prfsummary[\(Q\)]{\th \Delta, A, B}}
{\th \Delta, A \lor B}
\]

* if \(\th \Gamma = \th \Delta, A \land B\), then \(G = {G \rst_{\Delta, A}}
\sqcup {G \rst_{\Delta, B}}\) by <ref>,
with \(G \rst_{\Delta, A}\) and \(G \rst_{\Delta, B}\) total w.r.t. \(\th \Delta, A\)
and \(\th \Delta, B\) respectively: we apply the induction hypothesis twice to get
derivations \(Q, R\) with conclusion \(\th \Delta, A\) and \(\th \Delta, B\)
respectively, and such that \(\blaxg{Q} = G \rst_{\Delta, A}\), \(\blaxg{R} =
G \rst_{\Delta, B}\); we conclude by applying a conjunction rule to \(Q, R\):

\[
\prftree[r,l]{\rl{\land}}{\(P =\)}
{\prfsummary[\(Q\)]{\th \Delta, A}}
{\prfsummary[\(R\)]{\th \Delta, B}}
{\th \Delta, A \land B}
\qedhere
\]

Let bl-graphs \(G, H\) be total w.r.t. the sequents \(\th \Gamma, A\) and \(\th \Gamma,
\dl{A}\), respectively: then their composite \(G \odot_A H\) on \(A\) is total w.r.t. the
sequent \(\th \Gamma\).

§.§ The proof system BLG

Upon inspection of the proof above, one sees clearly that this is a kind of sequentialization
theorem. The natural question then is whether total bl-graphs can provide a canonical
representation of cut-free derivations up to arbitrary permutations of logical rules.

Let \(\data{BLG}\) denote the set of all pairs \(\langle G, \Gamma \rangle\) such that

* \(G\) is a finite bl-graph;

* \(\Gamma\) is a finite sharing-free set of named formulas;

* \(G\) is total w.r.t. \(\th \Gamma\).

We know by <ref> that there exists \(\langle G,
\Gamma \rangle \in \data{BLG}\) if and only if the sequent \(\th \Gamma\) is a classical
tautology. Is \(\data{BLG}\) a proof system for classical propositional logic?
The question is subtle: as recalled in the introduction, the mere presence of a correctness
criterion is not sufficient to provide a reasonable notion of proof. We define a notion of
size of a bl-graph/sequent pair and show that totality is checkable in polynomial
time: \(\data{BLG}\) is therefore a proof system in the sense of Cook and Reckhow <cit.>.

For any pair \(\mathbf{G} = \langle G, \Gamma \rangle\) where \(G\) is a finite
bl-graph and \(\Gamma\) a finite sharing-free set of named formulas, let

\[
\data{size}(\mathbf{G}) = \data{size}(\th \Gamma) + |V_G| + \sum_{e \adin_G X} |X|,
\]

where \(\data{size}(\th \Gamma)\) is the size of the sequent (<ref>,
<ref>), \(|V_G|\) is the number of vertices in the bl-graph \(G\),
and the last term is the total number of vertices in the branch labels of \(G\).

For any pair \(\mathbf{G} = \langle G, \Gamma \rangle\) where \(G\) is a finite
bl-graph and \(\Gamma\) a finite sharing-free set of named formulas, membership
in \(\data{BLG}\) is decidable in polynomial time in the size of \(\mathbf{G}\).

xα, zαx/z
xα, wαx/w
yα, zαy/z
yα, wαy/w
þxα yα, zα wα

xα, zβ, vα, wγx/v
xα, uγ, vα, wγx/v, u/w
yβ, zβ, vα, wγy/z
yβ, uγ, vα, wγu/w
þxα yβ, zβ uγ, vα wγ
A graphical representation of \(\data{BLG}\) proofs. Each proof is drawn as
a generalised inference rule, with branch labels above the line and the conclusion
below. Above each branch we draw the associated edges as black lines.

§.§ Properties of the system BLG

The proof system \(\data{BLG}\) enjoys very good properties. To begin with, all logical
rules of \(\data{GS4}^\mathcal{N}\) are admissible and invertible:

\begin{gather*}
\prftree[r]{\rl{{\downarrow}{\lor}}}
{\prfassumption{\langle G, (\Gamma, A, B) \rangle \in \data{BLG}}}
{\langle G, (\Gamma, A \lor B) \rangle \in \data{BLG}}
\qquad
\prftree[r]{\rl{{\uparrow}{\lor}}}
{\prfassumption{\langle G, (\Gamma, A \lor B) \rangle \in \data{BLG}}}
{\langle G, (\Gamma, A, B) \rangle \in \data{BLG}}
\\[1em]
\prftree[r]{\rl{{\downarrow}{\land}}}
{\prfassumption{\langle G, (\Gamma, A) \rangle \in \data{BLG}}}
{\prfassumption{\langle H, (\Gamma, B) \rangle \in \data{BLG}}}
{\langle G \sqcup H, (\Gamma, A \land B) \rangle \in \data{BLG}}
\\[1em]
\prftree[r]{\rl{{\uparrow}{\land_l}}}
{\prfassumption{\langle G, (\Gamma, A \land B) \rangle \in \data{BLG}}}
{\langle G \rst_{\Gamma, A}, (\Gamma, A) \rangle \in \data{BLG}}
\qquad
\prftree[r]{\rl{{\uparrow}{\land_r}}}
{\prfassumption{\langle G, (\Gamma, A \land B) \rangle \in \data{BLG}}}
{\langle G \rst_{\Gamma, B}, (\Gamma, B) \rangle \in \data{BLG}}
\end{gather*}

The cut-rule is also admissible by <ref>:

\[
\prftree[r]{\rl{cut}}
{\prfassumption{\langle G, (\Gamma, A) \rangle \in \data{BLG}}}
{\prfassumption{\langle H, (\Gamma, \dl{A}) \rangle \in \data{BLG}}}
{\langle G \odot_A H, \Gamma \rangle \in \data{BLG}}
\]

Finally, axiom and superposition rules are obviously admissible through their interpretation:

\begin{gather*}
\prftree[r]{\rl{ax}}
{\prfassumption{A \equiv B}}
{\langle \blwk{\Gamma}(\blid{\{A, \dl{B}\}}), (\Gamma, A, \dl{B}) \rangle \in \data{BLG}}
\qquad
\prftree[r]{\rl{\sqcup}}
{\prfassumption{\langle G, \Gamma \rangle \in \data{BLG}}}
{\prfassumption{\langle H, \Gamma \rangle \in \data{BLG}}}
{\langle G \sqcup H, \Gamma \rangle \in \data{BLG}}
\end{gather*}

Isolation is as expected an identity on \(\data{BLG}\) proofs. The inversion procedure
amounts to a simple replacement of the conclusion for disjunctions; in the case of conjunctions
some time must be spent computing the graph restriction, but it will be often significantly
less than the time spent to perform inversion on a sequent calculus derivation, especially
when all axioms in the derivation are atomic. These facts – together with the immediate
notation and the availability of equational reasoning – make \(\data{BLG}\) a very
efficient tool for reasoning about proof content and transformations.

The price to be paid lies in the size of proof objects, which is often exponential in the
complexity of the conclusion even when much smaller derivations would be available in the
context-splitting formulation of sequent calculus or even in \(\data{GS4}\) with non-atomic
axioms. This is a well-known problem that \(\data{BLG}\) shares with \(\data{GS4}\) when
restricted to atomic axioms. It is an open question whether some proof-compression method
could be devised to reduce the size \(\data{BLG}\) proofs without loosing the good properties
of the system.

§ ON THE ABSENCE OF A CUT-REDUCTION PROCEDURE

By cut-reduction procedure we mean a set of syntactical rewriting steps capable
of reducing the complexity of cut-rule applications in a derivation until they become atomic,
while at the same time preserving correctness and the conclusion of the derivation. One such
step is implemented in the proof of <ref>, where we apply the isolation
procedure to permute cuts towards the top of the derivation, thus reducing the complexity
of their context.

At present, however, we don't know of any rewriting step capable of reducing the complexity
of cut-formulas in \(\data{GS4}^\mathcal{N}\) derivations while preserving their associated
bl-graph. There is a known pair of natural cut-reduction steps, considered by Pulcini
in <cit.>:

\begin{gather*}
\makebox[\textwidth]{\small\(
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \vphantom{\dl{AB}}}}
{\th \Gamma, A \lor B}}
{\prfsummary[\(Q\)]{\th \Gamma, \dl{A}}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{B}}}
{\th \Gamma, \dl{A} \land \dl{B}}}
{\th \Gamma}}
\quad\rwr\quad
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \vphantom{\dl{A}}}}
{\prfsummary[\(\data{wk}(Q, B)\)]{\th \Gamma, \dl{A}, B}}
{\th \Gamma, B}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{B}}}
{\th \Gamma}}
\)}
\\[1em]
\makebox[\textwidth]{\small\(
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \vphantom{\dl{AB}}}}
{\th \Gamma, A \lor B}}
{\prfsummary[\(Q\)]{\th \Gamma, \dl{A}}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{B}}}
{\th \Gamma, \dl{A} \land \dl{B}}}
{\th \Gamma}}
\quad\rwr\quad
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \vphantom{\dl{B}}}}
{\prfsummary[\(\data{wk}(R, A)\)]{\th \Gamma, A, \dl{B}}}
{\th \Gamma, A}}
{\prfsummary[\(Q\)]{\th \Gamma, \dl{A}}}
{\th \Gamma}}
\)}
\end{gather*}

These are straightforward adaptations of the usual key steps for context-splitting systems
to the context-sharing setting of the system \(\data{GS4}^\mathcal{N}\). The resulting
cut reduction procedure is non-deterministic at the syntactical level, but both rewriting
steps preserve the axiom graph obtained through the unrefined construction (<ref>).

Unfortunately, the two steps are incompatible with the refined interpretation (<ref>).
To see why, one must remember that the branch-sensitive notion of composition is designed
to omit all those paths that connect the two sides of conjunctions occurring outside
the interface. The two rewriting steps above, in reducing one cut to two cuts of
lower complexity, select one subformula of the disjunction to bring temporarily outside the
interface. This might result in the loss of some paths when the selected formula is a conjunction:

\[
\makebox[\textwidth]{\small\(
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \land C \vphantom{\dl{ABC}}}}
{\th \Gamma, A \lor (B \land C)}}
{\prfsummary[\(Q\)]{\th \Gamma, \dl{A}}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{B} \lor \dl{C}}}
{\th \Gamma, \dl{A} \land (\dl{B} \lor \dl{C})}}
{\th \Gamma}}
\quad\rwr\quad
\vcenter{\prftree[r]{\rl{cut}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \land C \vphantom{\dl{A}}}}
{\prfsummary[\(\data{wk}(Q, B \land C)\)]{\th \Gamma, \dl{A}, B \land C}}
{\th \Gamma, B \land C}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{B} \lor \dl{C}}}
{\th \Gamma}}
\)}
\]

Here the left side of the rewriting rule is associated to the bl-graph

\[
\blaxg{P} \odot_{(A \lor (B \land C))} (\blaxg{Q} \sqcup \blaxg{R}),
\]

while the right side is interpreted as

\[
(\blaxg{P} \odot_A \blaxg{Q}) \odot_{B \land C} \blaxg{R};
\]

the conjunction \(B \land C\) is contained in the interface in the former expression, where
the interpretation is computed by a single composition step, but lies outside the interface
in the first half of the latter expression, where we compute first the intermediate step
\(\blaxg{P} \odot_A \blaxg{Q}\). To show that this is an actual problem, not just a hypothetical
possibility, we provide a complete (but slightly involved) counter-example in <ref>.

It remains unclear whether there is some syntactical counterpart to the semantical cut-elimination
procedure described in <ref>. It is possible that the problem could be
solved simply by superposing the two reducts, thus making the rewriting step deterministic:

\[
\makebox[\textwidth]{\small\(
\prftree[r]{\rl{\sqcup}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \vphantom{\dl{A}}}}
{\prfsummary[\(\data{wk}(Q, B)\)]{\th \Gamma, \dl{A}, B}}
{\th \Gamma, B}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{B}}}
{\th \Gamma}}
{\prfsummary[\(P\)]{\th \Gamma, A, B \vphantom{\dl{B}}}}
{\prfsummary[\(\data{wk}(R, A)\)]{\th \Gamma, A, \dl{B}}}
{\th \Gamma, A}}
{\prfsummary[\(Q\)]{\th \Gamma, \dl{A}}}
{\th \Gamma}}
{\th \Gamma}
\)}
\]

We have not been able to find a counter-example so far, but we have yet to attempt a proof.
We would have to show somehow that whenever some path is erased on one side, then it
must be preserved on the other side, and vice versa.

A different possibility would be to further refine the interpretation so as to make it
invariant under the two traditional cut-reduction steps. The key observation in this regard
is that all counter-examples known to us – including indeed the one in <ref>
– seem to rely critically on the possibility of constructing alternating paths using edges
from both branches of a superposition rule. This happens because superposition is not
interpreted as a non-deterministic sum of separate proofs, but as some kind of parallel
composition that “blends” two proofs together, thus obtaining a new and generally distinct one.
We conjecture that by treating superpositions as proper non-deterministic sums we should be
able to recover invariance under the traditional logical reduction steps. The picture however
is complicated by the fact that superpositions might be introduced when reducing weakening-
weakening cuts: it is not clear then how the new composition operator should look like.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

Springer Milan

titleLogica: Volume 1 - Dimostrazioni e modelli al primo ordine

IEEE Computer Society

journaltitleIEEE Trans. Comput.
titleRefutations by Matings
merge,first-order logic,clause-occurrence,refutation,mating,resolution,Automatic theorem proving,cycle,unsatisfiability.

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitle5th Conference on Automated Deduction
titleTransforming matings into natural deduction proofs

journaltitleInformation and Computation
titleA Symmetric Lambda-Calculus for Classical Program Extraction

booktitleProceedings of TACS'97
title“Classical” programming-with-proofs in $\lambda^{Sym}_{PA}$:an analysis of non-confluence

journaltitleAnnals of Pure and Applied Logic
titleThe undecidability of k-provability

journaltitleAnnals of Pure and Applied Logic
titleInterpolants, cut elimination and flow graphs for the propositional calculus
Cut elimination,Interpolation,Graphs of proofs

Cambridge University Press

journaltitleThe Journal of Symbolic Logic
titleThe relative efficiency of propositional proof systems

[Association for Symbolic Logic, Cambridge University Press]

abstractThe main concern of this paper is the design of a noetherian and confluent normalization for LK2 (that is, classical second order predicate logic presented as a sequent calculus). The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD ([10, 12, 32, 36]), delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' ([26, 27]) to classical logic; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic (for non-additive proof nets, to be precise) using appropriate embeddings (so-called decorations); it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making. A comparison of our method to that of embedding LK into LJ (intuitionistic sequent calculus) brings to the fore the latter's defects for these `deconstructive purposes'.
journaltitleThe Journal of Symbolic Logic
titleA New Deconstructive Logic: Linear Logic

Cambridge University Press

booktitleAdvances in Linear Logic
seriesLondon Mathematical Society Lecture Note Series
titleLKQ and LKT: Sequent calculi for second order logic based upon dual linear decompositions of classical implication

IEEE Computer Society

booktitleProceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004
titleOn the geometry of interaction for classical logic

journaltitleMathematische Zeitschrift
titleUntersuchungen über das logische Schließen. I

Cambridge University Press

journaltitleMathematical Structures in Computer Science
titleA new constructive logic: classical logic

Berlin, Heidelberg

Springer Berlin Heidelberg

titleGeometry of interaction II: Deadlock-free algorithms

abstractThe familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
journaltitleTheoretical Computer Science
titleLinear logic

Cambridge University Press

seriesCambridge Tracts in Theoretical Computer Science
titleProofs and Types

journaltitleLogical Methods in Computer Science
titleNormalisation Control in Deep Inference via Atomic Flows

journaltitleAnnals of Pure and Applied Logic
titleA minimal classical sequent calculus free of structural rules

Annals of Mathematics

journaltitleAnnals of Mathematics
titleProofs without Syntax

journaltitleElectronic Notes in Theoretical Computer Science
noteProceedings of the 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006)
titleTowards Hilbert's 24th Problem: Combinatorial Proof Invariants: (Preliminary version)
Combinatorial proof,Hilbert's 24th Problem,sequent calculus,Herbrand's Theorem

titleMathematical Logic

Schloss Dagstuhl–Leibniz-Zentrum für Informatik

booktitle20th International Conference on Types for Proofs and Programs, TYPES 2014
titleOn the Structure of Classical Realizability Models of ZF

Société Mathématique de France

booktitleInteractive Models of Computation and Program Behaviour
seriesPanoramas et synthèses
titleRealizability in classical logic

Berlin, Heidelberg

Springer Berlin Heidelberg

abstractThis paper shows how a symmetric and non-deterministic cut elimination procedure for a classical sequent calculus can be faithfully simulated using a non-deterministic choice operator to combine different `double-negation' translations of each cut. The resulting interpretation of classical proofs in a $\lambda$-calculus with non-deterministic choice leads to a simple proof of termination for cut elimination.
booktitleTyped Lambda Calculi and Applications
titleA Deconstruction of Non-deterministic Classical Cut Elimination

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitleTyped Lambda Calculi and Applications
titleNaming Proofs in Classical Propositional Logic

journaltitleTheoretical Computer Science
titleFocusing and Polarization in Linear, Intuitionistic, and Classical Logics

Cambridge University Press

titleStructural Proof Theory

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitleLogic Programming and Automated Reasoning
titleλμ-Calculus: An algorithmic interpretation of classical natural deduction

Cambridge University Press

journaltitleThe Review of Symbolic Logic
titleFractional Semantics for Classical Logic

abstractIn Schwichtenberg (Studies in logic and the foundations of mathematics, vol 90, Elsevier, pp 867–895, 1977), Schwichtenberg fine-tuned Tait's technique (Tait in The syntax and semantics of infinitary languages, Springer, pp 204–236, 1968) so as to provide a simplified version of Gentzen's original cut-elimination procedure for first-order classical logic (Gallier in Logic for computer science: foundations of automatic theorem proving, Courier Dover Publications, London, 2015). In this note we show that, limited to the case of classical propositional logic, the Tait–Schwichtenberg algorithm allows for a further simplification. The procedure offered here is implemented on Kleene's sequent system G4 (Kleene in Mathematical logic, Wiley, New York, 1967; Smullyan in First-order logic, Courier corporation, London, 1995). The specific formulation of the logical rules for G4 allows us to provide bounds on the height of cut-free proofs just in terms of the logical complexity of their end-sequent.
journaltitleArchive for Mathematical Logic
titleA note on cut-elimination for classical propositional logic

Springer Berlin Heidelberg

journaltitleGrundlehren der mathematischen Wissenschaften
titleProof Theory

Stanford University

titleStructural Complexity of Proofs

Université Paris-Diderot - Paris VII

titleTowards a Theory of Proofs of Classical Logic
typeHabilitation à diriger des recherches

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitleThe Syntax and Semantics of Infinitary Languages
titleNormal derivability in classical logic

Cambridge University Press

seriesCambridge Tracts in Theoretical Computer Science
titleBasic Proof Theory

A graph (also known as simple graph) is defined by a pair
\(G = \langle V_G, E_G \rangle\) where \(V_G\) is a set of vertices and
\(E_G\) is a set of unordered pairs of vertices, i.e. two-element subsets
of \(V_G\), called the edges of \(G\). For any pair of distinct vertices
\(u \neq v \in V_G\), let \(uv\) denote the set \(\{u, v\}\) and say that \(u\)
and \(v\) are adjacent in \(G\) iff \(uv \in E_G\).

Given graphs \(H, G\), say that \(H\) is a subgraph of \(G\) and write
\(H \sqsubseteq G\) iff \(V_H \subseteq V_G\) and \(E_H \subseteq E_G\). Write
\(H \sqsubset G\) iff \(H \sqsubseteq G\) and \(H \neq G\).

Given a graph \(G\), any set \(S\) of vertices induces a subgraph \(H \sqsubseteq G\)
by letting \(V_H = V_H \cap S\) and restricting the edge set:

\[
E_H = \{ e \in E_G \mid e \subseteq S \}.
\]

We say that \(H\) is an induced subgraph of \(G\) and denote it by \(G \rst_S\).

Graphs can be combined by an operation related to set-theoretic union, which constructs the least
upper bound of a family of graphs w.r.t. the subgraph order \({\sqsubseteq}\):

Let \(I\) be a set, \((G_i)_{i \in I}\) a family of graphs indexed by \(I\). We define
the union or superposition of the family as the graph

\[
\bigsqcup_{i \in I} G_i = \langle \bigcup_{i \in I} V_{G_i}, \bigcup_{i \in I} E_{G_i} \rangle.
\]

As a special case, given \(n \geq 0\) and graphs \(G_1, \ldots, G_n\), we define the
finite union

\[
G_1 \sqcup \ldots \sqcup G_n = \bigsqcup_{i = 1}^n G_i.
\]

Let \(I\) be a set, \((G_i)_{i \in I}\) a family of graphs indexed by \(I\); the union
graph \(\bigsqcup_{i \in I} G_i\) is the least upper bound of the family w.r.t. the
subgraph order \({\sqsubseteq}\).

Let \(I\) be any set, \((G_i)_{i \in I}\) a family of graphs indexed by \(I\), \(S\) an
arbitrary set of vertices: then

\[
\left(\bigsqcup_{i \in I} G_i\right)\rst_S = \bigsqcup_{i \in I} (G_i\rst_S)
\]

§ COMPLEXITY MEASURES ON FORMULAS, SEQUENTS AND DERIVATIONS

We define in the following paragraphs some useful measures of the complexity of formulas,
sequents and derivations, and discuss the relationships between them.

We define by structural induction four different measures on named formulas \(A\):
the height \(\data{h}(A)\), the atom count \(\data{\#at}(A)\), the
degree \(\data{deg}(A)\) and the size \(\data{size}(A)\):

* if \(A\) is atomic, let

\begin{gather*}
\data{h}(A) = \data{deg}(A) = 0,\\
\data{\#at}(A) = \data{size}(A) = 1;
\end{gather*}

* if \(A = B \lor C\) or \(A = B \land C\), let

\begin{align*}
\data{h}(A)    &= 1 + \max\{\data{h}(B), \data{h}(C)\},\\
\data{\#at}(A)  &= \data{\#at}(B) + \data{\#at}(C),\\
\data{deg}(A)  &= 1 + \data{deg}(B) + \data{deg}(C),\\
\data{size}(A) &= 1 + \data{size}(B) + \data{size}(C).
\end{align*}

The height tracks the length of the longest branch in the syntax tree of the formula,
the atom count is self-explanatory, the degree is the number of logical operators occurring
in the formula, and the size is the number of symbols (atoms and operators).

For all named formulas \(A\):

* \(\data{\#at}(A) = 1 + \data{deg}(A)\);

* \(\data{size}(A) = \data{\#at}(A) + \data{deg}(A) = 1 + 2 \cdot \data{deg}(A)\);

* \(\data{h}(A) \leq \data{deg}(A) < \data{\#at}(A) \leq \data{size}(A)\).

The inequalities \(\deg(A) < \data{\#at}(A)\) and \(\data{\#at}(A) \leq \data{size}(A)\)
are direct consequences of facts (i) and (ii). We prove facts (i) and (ii) and the first
inequality simultaneously by structural induction on \(A\):

* if \(A\) is atomic, then

\begin{gather*}
0 = \data{h}(A) \leq \data{deg}(A) = 0,\\
\data{\#at}(A) = 1 = 1 + 0 = 1 + \data{deg}(A) \text{, and}\\
\data{size}(A) = 1 = 1 + 0 = \data{\#at}(A) + \data{deg}(A);
\end{gather*}

* if \(A = B \lor C\) or \(A = B \land C\), then

\begin{align*}
\data{\#at}(A) &= \data{\#at}(B) + \data{\#at}(C)                                       & \text{(def.~\ref{defn:formula-complexity})}\\
&= \data{deg}(B) + 1 + \data{deg}(C) + 1                                  & \text{(ind.\ hyp.)}\\
&= 1 + \data{deg}(B) + \data{deg}(C) + 1                                  \\
&= \data{deg}(A) + 1                                                      & \text{(def.~\ref{defn:formula-complexity})}\\[1em]
\data{size}(A) &= 1 + \data{size}(B) + \data{size}(C)                                   & \text{(def.~\ref{defn:formula-complexity})}\\
&= 1 + \data{\#at}(B) + \data{deg}(B) + \data{\#at}(C) + \data{deg}(C)   & \text{(ind.\ hyp.)}\\
&= \data{\#at}(B) + \data{\#at}(C) + 1 + \data{deg}(B) + \data{deg}(C)   \\
&= \data{\#at}(A) + \data{deg}(A)                                        & \text{(def.~\ref{defn:formula-complexity})}\\[1em]
\data{h}(A) &= 1 + \max\{\data{h}(B), \data{h}(C)\}                                     & \text{(def.~\ref{defn:formula-complexity})}\\
&\leq 1 + \data{h}(B) + \data{h}(C)                                         \\
&\leq 1 + \data{deg}(B) + \data{deg}(C)                                     & \text{(ind.\ hyp.)}\\
&= \data{deg}(A)                                                            & \text{(def.~\ref{defn:formula-complexity})}
\end{align*}

We define for sequents the same measures as for formulas, by taking sums over all
formulas contained in the sequent: for all named sequents \(\th \Gamma\) let

\begin{align*}
\data{h}(\th \Gamma)   &= \sum_{A \in \Gamma} \data{h}(A),   &\data{\#at}(\th \Gamma) &= \sum_{A \in \Gamma} \data{\#at}(A),\\[.5em]
\data{deg}(\th \Gamma) &= \sum_{A \in \Gamma} \data{deg}(A), &\data{size}(\th \Gamma) &= \sum_{A \in \Gamma} \data{size}(A).
\end{align*}

Since \(\Gamma\) is required to be finite, all measures are well-defined.

For all named sequents \(\th \Gamma\):

* \(\data{\#at}(\th \Gamma) = |\Gamma| + \data{deg}(\th \Gamma)\);

* \(\data{size}(\th \Gamma) = \data{\#at}(\th \Gamma) + \data{deg}(\th \Gamma) = |\Gamma| + 2 \cdot \data{deg}(A)\);

* \(\data{h}(\th \Gamma) \leq \data{deg}(\th \Gamma) < \data{\#at}(\th \Gamma) \leq \data{size}(\th \Gamma)\).

For fact (i), observe that

\begin{align*}
\data{\#at}(\th \Gamma) &= \sum_{A \in \Gamma} \data{\#at}(A)           & \text{(def.~\ref{defn:sequent-complexity})}\\[.5em]
&= \sum_{A \in \Gamma} 1 + \data{deg}(A)         & \text{(lemma~\ref{propo:formula-complexity-relationships} (i))}\\[.5em]
&= \left(\sum_{A \in \Gamma} 1\right) + \left(\sum_{A \in \Gamma} \data{deg}(A)\right) & \text{(associativity)}\\[.5em]
&= \#\Gamma + \data{deg}(\th \Gamma)             & \text{(def.~\ref{defn:sequent-complexity}).}
\end{align*}

Fact (ii) follows from <ref> and the associativity of sums;
fact (iii) follows from <ref>, point (iii) and
the fact that addition is strictly monotonic over the natural numbers.

We define by structural induction two complexity measures on named derivation
trees \(P \in \data{GS4}^\mathcal{N}\): the height \(\data{h}(P)\) and the
size \(\data{size}(P)\):

* if \(P\) has the form

\[
\prfbyaxiom{\rl[\{A,\dl{B}\}]{ax}}{\th \Gamma, A, \dl{B}}
\]

where \(A \equiv B\), then let

\[
\data{h}(P) = 0,\ \data{size}(P) = 1;
\]

* otherwise \(P\) has the form

\[
\prftree[r]{\(r\)}
{\prfsummary[\(Q_1\)]{\th \Gamma_1}}
{\prfsummary[\(Q_n\)]{\th \Gamma_n}}
{\th \Gamma}
\]

where \(r \in \{\rl{cut}, \rl{\sqcup}, \rl{\lor}, \rl{\land}\}\)
and \(n > 0\): then let

\begin{align*}
\data{h}(P)    &= 1 + \max_{1 \leq i \leq n} \data{h}(Q_i),\\[.5em]
\data{size}(P) &= 1 + \sum_{1 \leq i \leq n} \data{size}(Q_i).
\end{align*}

§ PROOFS OF THE INVERSION LEMMAS

We collect in the present section all proofs of the inversion lemmas from <ref>
plus the proofs of admissibility for contraction and weakening.

By structural induction on \(P\):

* if \(P\) has the form

\[
\prfbyaxiom{\rl[\{\dl{C} \land \dl{D}, A \lor B\}]{ax}}
{\th \Delta, \dl{C} \land \dl{D}, A \lor B}
\]

where \(A \equiv C\), \(B \equiv D\) and \(\Gamma = \Delta \cup \{\dl{C} \land \dl{D}\}\),
then let \(\data{inv}(P, A \lor B)\) be

\[
\prftree[r]{\rl{\land}}
{\prfbyaxiom{\rl[\{\dl{C}, A\}]{ax}}{\th \Delta, \dl{C}, A, B}}
{\prfbyaxiom{\rl[\{\dl{D}, B\}]{ax}}{\th \Delta, \dl{D}, A, B}}
{\th \Delta, \dl{C} \land \dl{D}, A, B}
\]

* if \(P\) has the form

\[
\prfbyaxiom{\rl[\{C, \dl{D}\}]{ax}}
{\th \Delta, C, \dl{D}, A \lor B}
\]

where \(C \equiv D\) and \(\Gamma = \Delta \cup \{C, \dl{D}\}\), then let \(\data{inv}(
P, A \lor B)\) be

\[
\prfbyaxiom{\rl[\{C, \dl{D}\}]{ax}}
{\th \Delta, C, \dl{D}, A, B}
\]

* if \(P\) has the form

\[
\prftree[r]{\rl{\lor}}
{\prfsummary[\(Q\)]{\th \Gamma, A, B}}
{\th \Gamma, A \lor B}
\]

then let \(\data{inv}(P, A \lor B) = Q\);

* if \(P\) has the form

\[
\prftree[r]{\(r\)}
{\prfsummary[\(Q_1\)]{\th \Gamma_1, A \lor B}}
{\prfsummary[\(Q_n\)]{\th \Gamma_n, A \lor B}}
{\th \Gamma, A \lor B}
\]

where \(r \in \{\rl{cut}, \rl{\sqcup}, \rl{\lor}, \rl{\land}\}\)
and \(n > 0\), then apply \(\data{inv}({-}, A \lor B)\) recursively to each \(Q_i\)
and let \(\data{inv}(P, A \lor B)\) be

\[
\prftree[r]{\(r\)}
{\prfsummary[\(\data{inv}(Q_1, A \lor B)\)]{\th \Gamma_1, A, B}}
{\prfsummary[\(\data{inv}(Q_n, A \lor B)\)]{\th \Gamma_n, A, B}}
{\th \Gamma, A, B}\qedhere
\]

By structural induction on \(P\):

* if \(P\) has the form

\[
\prfbyaxiom{\rl[\{\dl{C} \lor \dl{D}, A \land B\}]{ax}}
{\th \Delta, \dl{C} \lor \dl{D}, A \land B}
\]

where \(A \equiv C\), \(B \equiv D\) and \(\Gamma = \Delta \cup \{\dl{C} \lor \dl{D}\}\),
then let \(\data{inv_l}(P, A \land B)\) be

\[
\prftree[r]{\rl{\lor}}
{\prfbyaxiom{\rl[\{\dl{C}, A\}]{ax}}{\th \Delta, \dl{C}, \dl{D}, A}}
{\th \Delta, \dl{C} \lor \dl{D}, A}
\]

* if \(P\) has the form

\[
\prfbyaxiom{\rl[\{C, \dl{D}\}]{ax}}
{\th \Delta, C, \dl{D}, A \land B}
\]

where \(C \equiv D\) and \(\Gamma = \Delta \cup \{C, \dl{D}\}\), then let \(\data{inv_l}(
P, A \land B)\) be

\[
\prfbyaxiom{\rl[\{C, \dl{D}\}]{ax}}
{\th \Delta, C, \dl{D}, A}
\]

* if \(P\) has the form

\[
\prftree[r]{\rl{\land}}
{\prfsummary[\(Q\)]{\th \Gamma, A}}
{\prfsummary[\(R\)]{\th \Gamma, B}}
{\th \Gamma, A \land B}
\]

then let \(\data{inv_l}(P, A \land B) = Q\);

* if \(P\) has the form

\[
\prftree[r]{\(r\)}
{\prfsummary[\(Q_1\)]{\th \Gamma_1, A \land B}}
{\prfsummary[\(Q_n\)]{\th \Gamma_n, A \land B}}
{\th \Gamma, A \land B}
\]

where \(r \in \{\rl{cut}, \rl{\sqcup}, \rl{\lor}, \rl{\land}\}\)
and \(n > 0\), then apply \(\data{inv_l}({-}, A \land B)\) recursively to each \(Q_i\)
and let \(\data{inv_l}(P, A \land B)\) be

\[
\prftree[r]{\(r\)}
{\prfsummary[\(\data{inv_l}(Q_1, A \land B)\)]{\th \Gamma_1, A}}
{\prfsummary[\(\data{inv_l}(Q_n, A \land B)\)]{\th \Gamma_n, A}}
{\th \Gamma, A}\qedhere
\]

By structural induction on \(P\):

* if \(P\) has the form

\[
\prfbyaxiom{\rl[\{\dl{C} \lor \dl{D}, A \land B\}]{ax}}
{\th \Delta, \dl{C} \lor \dl{D}, A \land B}
\]

where \(A \equiv C\), \(B \equiv D\) and \(\Gamma = \Delta \cup \{\dl{C} \lor \dl{D}\}\),
then let \(\data{inv_r}(P, A \land B)\) be

\[
\prftree[r]{\rl{\lor}}
{\prfbyaxiom{\rl[\{\dl{D}, B\}]{ax}}{\th \Delta, \dl{C}, \dl{D}, B}}
{\th \Delta, \dl{C} \lor \dl{D}, B}
\]

* if \(P\) has the form

\[
\prfbyaxiom{\rl[\{C, \dl{D}\}]{ax}}
{\th \Delta, C, \dl{D}, A \land B}
\]

where \(C \equiv D\) and \(\Gamma = \Delta \cup \{C, \dl{D}\}\), then let \(\data{inv_r}(
P, A \land B)\) be

\[
\prfbyaxiom{\rl[\{C, \dl{D}\}]{ax}}
{\th \Delta, C, \dl{D}, B}
\]

* if \(P\) has the form

\[
\prftree[r]{\rl{\land}}
{\prfsummary[\(Q\)]{\th \Gamma, A}}
{\prfsummary[\(R\)]{\th \Gamma, B}}
{\th \Gamma, A \land B}
\]

then let \(\data{inv_r}(P, A \land B) = R\);

* if \(P\) has the form

\[
\prftree[r]{\(r\)}
{\prfsummary[\(Q_1\)]{\th \Gamma_1, A \land B}}
{\prfsummary[\(Q_n\)]{\th \Gamma_n, A \land B}}
{\th \Gamma, A \land B}
\]

where \(r \in \{\rl{cut}, \rl{\sqcup}, \rl{\lor}, \rl{\land}\}\)
and \(n > 0\), then apply \(\data{inv_r}({-}, A \land B)\) recursively to each \(Q_i\)
and let \(\data{inv_r}(P, A \land B)\) be

\[
\prftree[r]{\(r\)}
{\prfsummary[\(\data{inv_r}(Q_1, A \land B)\)]{\th \Gamma_1, B}}
{\prfsummary[\(\data{inv_r}(Q_n, A \land B)\)]{\th \Gamma_n, B}}
{\th \Gamma, B}\qedhere
\]

Let us fix once and for all a complete enumeration \(x_1, x_2, \ldots\) without
repetitions of the countable set \(\mathcal{N}\) of names. The \(\data{wk}\)-transformation
will be deterministic up to our choice of enumeration. We are also gonna need the theory of
renamings from <ref>. We proceed by induction on the height of \(P\):

* if \(P\) has the form

\[
\prfbyaxiom{\rl[\{C, \dl{D}\}]{ax}}
{\th \Gamma', C, \dl{D}}
\]

where \(C \equiv D\) and \(\Gamma = \Gamma' \cup \{C, \dl{D}\}\), then let \(\data{wk}(
P, \Delta)\) be

\[
\prfbyaxiom{\rl[\{C, \dl{D}\}]{ax}}
{\th \Gamma', C, \dl{D}, \Delta}
\]

* if \(P\) has the form

\[
\prftree[r]{\(r\)}
{\prfsummary[\(Q_1\)]{\th \Gamma_1}}
{\prfsummary[\(Q_n\)]{\th \Gamma_n}}
{\th \Gamma}
\]

where \(r \in \{\rl{\sqcup}, \rl{\lor}, \rl{\land}\}\) and \(n > 0\),
then one may check easily (by inspection of the three rules listed before) that
\(\data{names}(\Gamma_i) \subseteq \data{names}(\Gamma)\) for all \(1 \leq i
\leq n\): apply \(\data{wk}({-}, \Delta)\) recursively to each \(Q_i\) and
let \(\data{wk}(P, \Delta)\) be

\[
\prftree[r]{\(r\)}
{\prfsummary[\(\data{wk}(Q_1, \Delta)\)]{\th \Gamma_1, \Delta}}
{\prfsummary[\(\data{wk}(Q_n, \Delta)\)]{\th \Gamma_n, \Delta}}
{\th \Gamma, \Delta}
\]

* if \(P\) has the form

\[
\prftree[r]{\rl{cut}}
{\prfsummary[\(Q\)]{\th \Gamma, A \vphantom{\dl{A}}}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{A}}}
{\th \Gamma}
\]

we must take into account the possibility that \(A, \dl{A}\) and \(\Delta\) share some
names, as the hypothesis only guarantees that \(\Delta\) share no names with \(\Gamma\).
Let then \(k\) be the smallest natural number such that, for all \(1 \leq i \geq k\),
\(x_i \notin \data{names}(P) \cup \data{names}(\Delta)\): such a \(k\) must exist
because only finitely many names may occur either in \(P\) or \(\Delta\), and the
enumeration has no repetitions. We construct a renaming \(\phi: \data{names}(P) \to \mathcal{N}\)
of \(P\) by letting

\[
\phi(x_i) = \begin{cases}
x_{i+k}     & \text{if } x_i \in \data{names}(\Delta),\\
x_i         & \text{otherwise,}
\end{cases}
\]

for all \(i \in \N\) such that \(x_i \in \data{names}(P)\). Because no name
in \(\Gamma\) occurs also in \(\Delta\), \(\phi\) is guaranteed to act as the
identity on all formulas in \(\Gamma\), i.e. \(\phi P\) has the form

\[
\prftree[r]{\rl{cut}}
{\prfsummary[\(\phi Q\)]{\th \Gamma, \phi A \vphantom{\sdl{(\phi A)}}}}
{\prfsummary[\(\phi R\)]{\th \Gamma, \sdl{(\phi A)}}}
{\th \Gamma}
\]

where \(\phi A, \sdl{(\phi A)}\) share no location with \(\Delta\) by construction
of \(\phi\), and \(\phi Q, \phi R\) have by <ref>
the same height as \(Q, R\) respectively: let then \(\data{wk}(P, \Delta)\) be

\[
\prftree[r]{\rl{cut}}
{\prfsummary[\(\data{wk}(\phi Q, \Delta)\)]{\th \Gamma, \phi A, \Delta \vphantom{\sdl{(\phi A)}}}}
{\prfsummary[\(\data{wk}(\phi R, \Delta)\)]{\th \Gamma, \sdl{(\phi A)}, \Delta}}
{\th \Gamma, \Delta}
\qedhere
\]

§ RENAMINGS

A renaming of a named formula \(A\) (resp. set \(\Gamma\) of named formulas) is an
injective map from \(\data{names}(A)\) (resp. \(\data{names}(\Gamma)\))
to \(\mathcal{N}\). For any named formula \(A\) and renaming \(\phi\) of \(A\), let

\[
\phi A = \begin{cases}
\nm{\phi x}{\alpha}         & \text{if } A = \nm{x}{\alpha} \text{ for some } \alpha \in \mathcal{A}, x \in \mathcal{N}, \\
\phi B \lor \phi C          & \text{if } A = B \lor C, \\
\phi B \land \phi C         & \text{if } A = B \land C.
\end{cases}
\]

The application of a renaming \(\phi\) to a set \(\Gamma\) is defined by taking its image
under \(\phi\), observing that, for each \(A \in \Gamma\), the restriction of \(\phi\)
to \(\data{names}(A)\) is necessarily a renaming of \(A\).

For any named formula \(A\) and renaming \(\phi\) of \(A\), \(\phi A\) is also a named
formula with \(A \equiv \phi A\), \(\data{names}(\phi A) = \phi(\data{names}(A))\),
and sharing-free iff so is \(A\).

The equivalence result and that about name sets are more or less immediate, by structural
induction on \(A\). As regards sharing-freedom, we reason again by structural induction
on \(A\):

* if \(A\) is atomic then so is \(\phi A\) and they are both sharing-free
by definition;

* if \(A = B \diamond C\) (where \({\diamond} \in \{{\lor},{\land}\}\)), then
\(\phi A = \phi B \diamond \phi C\). By induction hypothesis \(B, C\) are
sharing-free if and only if so are \(\phi B, \phi C\), respectively. Moreover,
because \(\phi\) is injective, \(\data{names}(\phi B) = \phi(\data{names}(B))\)
and the same holds for \(C\) mutatis mutandis, \(B, C\) are disjoint
if and only if so are \(\phi B, \phi C\). Then \(A\) is sharing-free, by definition,
iff \(B, C\) are disjoint and both sharing-free, iff \(\phi B, \phi C\) are disjoint
and both sharing-free, iff again by definition \(\phi A\) is sharing-free.

Let \(A\) be any named formula:

* \(\phi\) is a renaming of \(A\) if and only if it is a renaming of \(\dl{A}\);

* for any renaming \(\phi\) of \(A\), \(\phi(\dl{A}) = \sdl{(\phi A)}\).

Left to the reader.

Let \(\Gamma\) be a set of named formulas, \(\phi\) a renaming of \(\Gamma\):

* for all \(A, B \in \Gamma\), \(A = B\) if and only if \(\phi A = \phi B\);

* for all \(A, B \in \Gamma\), \(A, B\) share names if and only if so do \(\phi A, \phi B\);

* for all \(\Delta, \Delta' \subseteq \Gamma\), \(\Delta, \Delta'\) share
names if and only if so do \(\phi\Delta, \phi\Delta'\).

Point (ii) is a special case of point (iii), which is in turn an immediate consequence
of the injectivity of \(\phi\) plus the obvious facts that \(\data{names}(\phi\Delta) =
\phi(\data{names}(\Delta))\) and \(\data{names}(\phi\Delta') = \phi(\data{names}(\Delta'))\).
For point (i) we proceed by structural induction on \(A\):

* \(A\) is atomic: then \(A = B\) if and only if \(A = \nm{x}{\alpha} = B\)
(resp. \(A = \nm{x}{\dl{\alpha}} = B\)) for some \(\alpha \in \mathcal{A}\)
and \(x \in \mathcal{N}\), if and only if \(\phi A = \nm{\phi x}{\alpha} = \phi B\)
(resp. \(\phi A = \nm{\phi x}{\dl{\alpha}} = \phi B\));

* \(A = C \diamond D\) where \({\diamond} \in \{{\lor},{\land}\}\): then \(A = B\)
if and only if \(B = C \diamond D\), if and only if \(\phi A = \phi C \lor \phi D =
\phi B\).

For all named sequents \(\th \Gamma\) and renamings \(\phi\) of \(\th \Gamma\),
\(\phi(\th \Gamma)\) is also a named sequent with \((\th \Gamma) \equiv \phi(\th \Gamma)\),
and sharing-free iff so is \(\th \Gamma\).

The fact that \(\phi(\th \Gamma)\) is a named sequent and sharing-free iff so is \(\th
\Gamma\) follows from <ref>,
point (ii). For the equivalence, observe that by <ref>, point (i),
\(\phi\) induces a bijection between \(\Gamma\) and \(\phi\Gamma\) such that (again by
<ref>) \(A \equiv \phi A\) for all \(A \in \Gamma\).

Finally, we can rename whole derivation trees while preserving their structure and
conclusion (obviously up to renaming):

A renaming of a named derivation tree \(P \in \data{GS4}^\mathcal{N}\) is an injective
map \(\phi: \data{names}(P) \to \mathcal{N}\).

The application of \(\phi\) to \(P\), noted \(\phi P\), is the tree obtained by applying \(\phi\)
recursively to the named sequents labeling each node of \(P\) (plus the selected formulas in
axiom rules).

Let \(P \in \data{GS4}^\mathcal{N}\) be any named derivation tree with conclusion
\(\th \Gamma\), \(\phi\) a renaming of \(P\): then \(\phi P \in \data{GS4}^\mathcal{N}\)
is also a derivation tree with conclusion \(\phi(\th \Gamma)\) and height \(\data{h}(\phi P)
= \data{h}(P)\), cut-free (resp. superposition-free) iff so is \(P\).

By a simple structural induction on \(P\), using <ref>
and <ref> to prove that constraints on the shape
of rules are satisfied by \(\phi P\) at every step.

§ PROOFS OF LEMMAS REGARDING SIMPLE AXIOM GRAPHS

By structural induction on \(P\):

* if \(P\) has the form

\[
\prfbyaxiom{\rl[\{A, \dl{B}\}]{ax}}
{\th \Delta, A, \dl{B}}
\]

where \(\Gamma = \Delta \cup \{A, \dl{B}\}\) and \(A \equiv B\) then by
<ref> \(V_{\axg{P}} = \data{names}(
\Delta) \cup \data{names}(\{A, \dl{B}\}) = \data{names}(\Gamma)\);

* if \(P\) has the form

\[
\prftree[r]{\rl{cut}}
{\prfsummary[\(Q\)]{\th \Gamma, A \vphantom{\dl{A}}}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{A}}}
{\th \Gamma}
\]

then by induction hypothesis and <ref>

\[
V_{\axg{P}} = (\data{names}(\Gamma, A) \cup \data{names}(\Gamma, \dl{A})) \setminus \data{names}(A);
\]

the statement follows from the fact that \(\data{names}(A) = \data{names}(\dl{A})\);

all other cases follow immediately from the induction hypothesis.

By structural induction on \(P\). For the sake of brevity we let \(P' = \data{inv}(P,
A \lor B)\) and omit at each step the shape of \(P, P'\): the interested reader may
inspect the corresponding steps in the proof of <ref>
(<ref>). Because \(\data{names}(\Gamma, A, B) = \data{names}(
\Gamma, A \lor B)\), we have in any case \(V_{\axg{P'}} = V_{\axg{P}}\) and it is
enough to show that \(E_{\axg{P'}} = E_{\axg{P}}\):

* if \(P\) ends with an axiom rule application of the kind \(\data{ax}_{\{\dl{C}
\land \dl{D}, A \lor B\}}\) with conclusion \(\th \Delta, \dl{C} \land \dl{D}, A \lor B\)
where \(\Gamma = \Delta \cup \{\dl{C} \land \dl{D}\}\), then by <ref>

\[
\axg{P'} = (\data{Wk}_{\Delta, B} \sqcup \data{Id}_{\{\dl{C}, A\}})
\sqcup (\data{Wk}_{\Delta, A} \sqcup \data{Id}_{\{\dl{D}, B\}})
\]

and by <ref> we have

\begin{align*}
\axg{P'} &= \data{Wk}_{\Delta} \sqcup \data{Id}_{\{\dl{C}, A\}}
\sqcup \data{Id}_{\{\dl{D}, B\}}\\
&= \data{Wk}_{\Delta} \sqcup \data{Id}_{\{\dl{C} \land \dl{D}, A \lor B\}}
= \axg{P};
\end{align*}

* if \(P\) ends with an axiom rule application of the kind \(\data{ax}_{\{C,\dl{D}\}}\)
with conclusion \(\th \Delta, A \lor B, C, \dl{D}\) where \(\Gamma = \Delta \cup
\{C, \dl{D}\}\), then by <ref>

\[
\axg{P'} = \data{Wk}_{\Delta, A, B} \sqcup \data{Id}_{\{C, \dl{D}\}}
= \data{Wk}_{\Delta, A \lor B} \sqcup \data{Id}_{\{C, \dl{D}\}} = \axg{P};
\]

* if \(P\) ends with a -rule application introducing \(A \lor B\)
with premiss subtree \(Q\), then \(P' = Q\) and \(\axg{P'} = \axg{Q} = \axg{P}\);

* if \(P\) ends with a cut-rule application on formulas \(C, \dl{C}\),
with premiss subderivations \(Q, R\), we have by induction hypothesis \(\axg{\data{inv}(
Q, A \lor B)} = \axg{Q}\) and \(\axg{\data{inv}(R, A \lor B)} = \axg{R}\), hence

\[
\axg{P'} = \axg{\data{inv}(Q, A \lor B)} \odot_C \axg{\data{inv}(R, A \lor B)}
= \axg{Q} \odot_C \axg{R} = \axg{P};
\]

* if \(P\) ends with a sum-, - or -rule
application that does not introduce \(A \lor B\), with premiss subtrees \(Q_1, \ldots, Q_n\),
we have \(\axg{\data{inv}(Q_i, A \lor B)} = \axg{Q_i}\) by induction hypothesis
for all \(1 \leq i \leq n\): then

\begin{multline*}
\axg{P'} = \axg{\data{inv}(Q_1, A \lor B)} \sqcup \ldots \sqcup \axg{\data{inv}(Q_n, A \lor B)}\\
= \axg{Q_1} \sqcup \ldots \sqcup \axg{Q_n} = \axg{P}.
\end{multline*}

We only prove the first part of the statement, i.e. that

\[
\axg{\data{inv_l}(P, A \land B)} \sqsubseteq \axg{P} \rst_{\Gamma, A};
\]

the argument for the second part is analogous. Let \(P' = \data{inv_l}(P, A \land B)\),