# Proof Compression via Subatomic Logic and Guarded Substitutions

Victoria Barrett, Alessio Guglielmi, Benjamin Ralph, Lutz Straßburger

► To cite this version:

Victoria Barrett, Alessio Guglielmi, Benjamin Ralph, Lutz Straßburger. Proof Compression via Subatomic Logic and Guarded Substitutions. LICS 2025 - 40th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2025, Singapore, Singapore. pp.183-195, 10.1109/LICS65433.2025.00021. hal-05356083

HAL Id: hal-05356083

https://inria.hal.science/hal-05356083v1

Submitted on 10 Nov 2025

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
Proof Compression via Subatomic Logic and
Guarded Substitutions

Victoria Barrett

Partout

Inria Saclay

Ile-de-France, France

Alessio Guglielmi

Department of Computer Science

University of Bath

Bath, United Kingdom

Benjamin Ralph

Department of Computer Science

University of Bath

Bath, United Kingdom

Lutz Straßburger

Partout

Inria Saclay

Ile-de-France, France

**Abstract**—Subatomic logic is a recent innovation in structural proof theory where atoms are no longer the smallest entity in a logical formula, but are instead treated as binary connectives. As a consequence, we can give a subatomic proof system for propositional classical logic such that all derivations are strictly linear: no inference step deletes or adds information, even units. In this paper, we introduce a powerful new proof compression mechanism that we call *guarded substitutions*, a variant of explicit substitutions, which substitute only guarded occurrences of a free variable, instead of all free occurrences. This allows us to construct “superpositions” of derivations, which simultaneously represent multiple subderivations. We show that a subatomic proof system with guarded substitution can p-simulate a Frege system with substitution, and moreover, the cut-rule is not required to do so.

This work was supported by the Inria Exploratory Action IMPROOF and PHC Sophie Germain “Formal Verification for Large Language Models”

# I. INTRODUCTION

The affinity between structural proof theory and the mathematical foundations of computation establishes mechanisms of proof compression as a natural object of study. The most prominent proof compression mechanism is the *cut rule* [15], [16], which allows lemmas to be reused in a proof. And indeed, eliminating the cuts from a proof can lead to a non-elementary blow-up [7]. In propositional logic, this blow-up is still exponential [28].

In the area of proof complexity, a distinct subfield of proof theory, other mechanisms of proof compression have been studied, the most notable ones being substitution [13] and Tseitin extension [29]. In both cases, proof compression is achieved by permitting propositional variables to replace arbitrary subformulae in a proof. The cost of eliminating either rule from a proof is an exponential blow-up (and it is not known whether this can be done more efficiently).

Given their conceptual similarity, it is perhaps not so surprising that, in the presence of cut, extension and substitution are *p-equivalent*, i.e., a system with cut and substitution can polynomially simulate one with cut and Tseitin extension [13], and vice versa [22]. This has been shown in the setting of Frege systems, which always contain the cut because of the presence of the *modus ponens* rule. Moreover, even in the absence of cut, it has also been demonstrated that the two proof compression mechanisms of substitution and Tseitin extension

are *p-equivalent* [25], [27]. However, it is not known if cut-free systems with extension or substitution can *p-simulate* systems with cut and extension or substitution.

This leaves us with two powerful proof compression mechanisms: (i) the cut and (ii) extension/substitution. It is an open question whether one of them subsumes the other, or whether they are truly independent.

In this paper we give a surprising answer to this question. We observe that both proof compression mechanisms are subsumed by a more general one, namely, *guarded substitution*, which is a variant of explicit substitutions [1].

To see how this is possible, let us first observe that the proof compression of cut and substitution comes from the ability of reusing information. And the most basic inference rules that deal with duplication of information are the rules of *contraction* and *cocontraction* shown below:<fnref n="1" />

$$ c \downarrow \frac{A \lor A}{A} \quad \text{and} \quad c^{\uparrow} \frac{A}{A \land A} \qquad (1) $$

A move to a deep inference proof system [8], [20], which allow for finer granularity in the design of the inference rules, enables the restriction of these rules to their atomic form, shown below, provided there is an additional purely linear inference rule in the system [8]. This rule, called *medial*, is shown in the middle below:

$$ ac \downarrow \frac{a \lor a}{a} \qquad m \frac{(A \land B) \lor (C \land D)}{(A \lor C) \land (B \lor D)} \qquad ac^{\uparrow} \frac{a}{a \land a} \qquad (2) $$

This leads to the proof system SKS [8], consisting only of atomic rules (like $ac \downarrow$ and $ac^{\uparrow}$ above) that change the size of a formula, and purely linear rules (like $m$ above) that only rearrange subformulae without changing the size.

The next insight comes from the concept of *subatomic proof theory* [2], [4], [6] which splits the atoms into binary connectives. A formula “$A a B$” is then interpreted as “if $a$ is false then $A$, and if $a$ is true then $B$”. In this setting, we can

<footnote n="1">¹In fact, the combination of contraction and cocontraction form another mechanism of proof compression, when cut is absent. This has been investigated in [10], [14], [21]. However, we will not go into further details of this, as we present in this paper a cut-free system that can *p-simulate* cut.</footnote>
$$ \text{cut} \frac{\vdash \Gamma, A \quad \vdash \bar{A}, \Delta}{\vdash \Gamma, \Delta} \rightsquigarrow i\uparrow \frac{A \wedge \bar{A}}{0} \rightsquigarrow a\uparrow \frac{a \wedge \bar{a}}{0} \rightsquigarrow \hat{a} \wedge \frac{(0 a 1) \wedge (1 a 0)}{(0 \wedge 1) a (1 \wedge 0)} \rightsquigarrow \hat{a} \wedge \frac{(A a B) \wedge (C a D)}{(A \wedge C) a (B \wedge D)} $$

<caption>Fig. 1. Evolution of cut from the sequent calculus via deep inference to subatomic proof theory</caption>

write $a$ as $0 a 1$ and its dual $\bar{a}$ as $1 a 0$. The two rules of ac↓ and ac↑ from above now become:

$$ \frac{(0 a 1) \lor (0 a 1)}{(0 \lor 0) a (1 \lor 1)} \quad \text{and} \quad \frac{(0 \land 0) a (1 \land 1)}{(0 a 1) \land (0 a 1)} \quad (3) $$

which are just instances of the general rules

$$ \tilde{\vee}_a \frac{(A \ a \ B) \lor (C \ a \ D)}{(A \lor C) \ a \ (B \lor D)} \quad \text{and} \quad \hat{\vee}_a \frac{(A \land B) \ a \ (C \land D)}{(A \ a \ C) \land (B \ a \ D)} \quad (4) $$

which have the same shape as the medial rule in (2) above. The same principle also applies to the cut rule: in Figure 1 we see the evolution of the cut, starting from the sequent calculus, first becoming an atomic rule, and finally a subatomic rule. In this way we can obtain a proof system for propositional logic in which all inference rules are linear rewriting steps [2], except for the rules dealing with the units, for example

$$ \frac{A}{A \wedge 1} \qquad \frac{A}{A \lor 0} \qquad \frac{A \wedge 1}{A} \qquad \frac{A \lor 0}{A} \quad (5) $$

Even though these are rather trivial inference steps in a standard proof system, they are the only ones that break a rigidly defined notion of linearity in a subatomic proof system. To achieve what is called a strictly linear system, these can be eliminated, but the naive way of doing so leads to an exponential blow-up of the size of the proof [5], [6]. However, by allowing explicit substitutions as constructors in formulae and derivations, the size of the proof expansion can be reduced to a polynomial [6]. The resulting system (called KDTS in [6]) is p-equivalent to SKS (and therefore also to standard Frege systems without extension or substitution) and still contains the cut (in its linear form, as shown on the right in Figure 1). And, unsurprisingly, eliminating the cut from this system leads to an exponential blow-up [6]. Furthermore, it is unknown whether these explicit substitutions can in any way polynomially simulate Tseitin extension or substitution in Frege systems.

In other words, in terms of proof complexity, nothing has been gained so far with respect to what we said at the beginning of this introduction; even in the unfamiliar climes of a subatomic proof system with explicit substitutions, it appears that both cut and extension/substitution operate as independent means of compressing proofs.

This motivates our paper, in which we introduce *guarded substitutions* that offer us a distinct new means of proof compression.

Guarded substitutions are a variant of explicit substitution that, instead of representing the replacement of every occurrence of a free variable, only select a certain subset of the free occurrences of the given variable. To make this

formal, we assign to every variable occurrence a *range*, and to every guarded substitution a *guard*, and the substitution can apply to the variable occurrence, if the guard is in the range. For example, the formula $\langle A|x \rangle((x \land x) \lor (y \land x))$ with an ordinary explicit substitution becomes $(A \land A) \lor (y \land A)$ when the substitution is carried out, whereas the formula $\langle A|x \rangle^p((x^{q,p} \land x^r) \lor (y^p \land x^{p,r}))$ becomes $(A \land x^r) \lor (y^p \land A)$ when the substitution is carried out, because only the first and the last $x$ have the guard $p$ in its range.

With this additional construct, the new system, that we call KSubG, can polynomially simulate Frege systems with substitution. Furthermore, we can do this with the cut-free fragment KSubG-. In other words, guarded substitution can polynomially simulate the cut, as well as Tseitin extension and substitution in Frege systems. And surprisingly, this can even be done when we only allow the units 0 and 1 in the place of the formula to be substituted (the $A$ in the example above).

Since Frege systems with substitution are known to be the most potent propositional proof systems, in the sense that they can polynomially simulate every other proof system for classical propositional logic, our system KSubG has now the same property, with the additional feature that every inference step is linear. There is never an inference that adds or deletes information.

This becomes possible because a subatomic derivation can be interpreted as a *superposition* of standard derivations. Even though this idea has been around since the beginning of subatomic proof theory [17], only our guarded substitutions allow to make use of this. We can see such a superposition as executing several similar shaped derivations in parallel, and the guarded substitutions can be used to read out the correct results. This allows for the factorisation of lemmas with different inputs, essentially performing the work of both modus ponens and the Frege substitution rule.

This paper is organized as follows.

* In the next section we present our system KSubG. We introduce the principles of subatomic proof theory, as presented in [2], [4], together with the explicit substitutions of [6], and our guarded substitutions.

* Then, in Section III, we show how subatomic proof theory is related to standard proof theory.

* In Section IV, we discuss the cut and cut elimination in subatomic systems, and we formalize the notion of *superposition*.

* In Section V, we formally introduce Frege systems with substitution.

* And finally, in Section VI, we prove our main result, showing that the cut-free fragment of our system KSubG polynomially simulates Frege systems with substitution.
• We end with a discussion in Section VII on the possible use of guarded substitutions beyond the restricted setting of this paper.

## II. A SUBATOMIC SYSTEM WITH GUARDED SUBSTITUTION

### A. Subatomic formulae

We begin our exposition by recalling the basic notions of subatomic proof theory [3], [4] with explicit substitution, as introduced in [6]. At the same time, we introduce guarded substitutions, for which we need a notion of guards that will be attached to variables.

**Definition 1.** We start from the following countable sets:

• **Variables**: $V = \{x, y, z, w, \dots\}$,

• **Atoms**: $A = \{a, b, c, \dots\}$,

• **Connectives**: $C = \{\wedge, \vee\}$,

• **Units**: $U = \{0, 1\}$,

• **Guards**: $G = \{p, q, r, \dots\}$.

A set of guards is called a **range**, and we denote the set of ranges with $R = \mathcal{P}(G) = \{R, S, \dots\}$.

The set $\mathcal{F} = \{A, B, C, \dots\}$ of (subatomic) formulae is defined as follows:

$$ \mathcal{F} ::= \mathcal{V}^{\mathcal{R}} | \mathcal{U} | \mathcal{F} \mathcal{A} \mathcal{F} | \mathcal{F} \mathcal{C} \mathcal{F} | \langle \mathcal{F} | \mathcal{V} \rangle \mathcal{F} | \langle \mathcal{U} | \mathcal{V} \rangle^{\mathcal{G}} \mathcal{F} $$

On the set $\mathcal{F}$ we define the **negation function** $\neg$: $\mathcal{F} \to \mathcal{F}$ inductively as follows:

$$ \begin{align*} \overline{x^R} &= x^R & \overline{A \ a \ \overline{B}} &= \overline{A \ a \ \overline{B}} \\ \overline{0} &= 1 & \overline{A \ \wedge \ \overline{B}} &= \overline{A \ \vee \ \overline{B}} \\ \overline{1} &= 0 & \overline{A \ \vee \ \overline{B}} &= \overline{A \ \wedge \ \overline{B}} \end{align*} $$

It follows that $\overline{\overline{B}} = B$.

**Notation 2.** Every variable occurrence in a formula $A$ is equipped with a range $R$, which is a set of guards. We omit the range when it is empty, writing $x$ instead of $x^0$.

**Notation 3.** In the subatomic setting, atoms do not behave as atomic formulae or nullary connectives, but as binary connectives. We make this distinction by writing atomic connectives in bold: $a, b, c, \dots$. The intended semantics of a formula $A \ a \ B$ is $A$ whenever $a$ is false and $B$ whenever $a$ is true. This means we can recover the standard (i.e. non-subatomic) atom $a$ with $0 \ a \ 1$ and its negation $\bar{a}$ with $1 \ a \ 0$.<fnref n="2" />

**Definition 4.** The term $\langle A | y \rangle$ is an **explicit substitution** and the term $\langle A | y \rangle^p$ is a **protected (explicit) substitution**. If $A$ and $B$ are formulae then both $\langle A | y \rangle$ and $\langle A | y \rangle^p$ are formulae, and in both cases, every occurrence of $y$ in $B$ is **bound**. Every variable occurrence that is not bound is **free**. We denote the set of free variables of a formula $A$ by $\underline{A}$. We do not consider the substitution variable $y$ in $\langle A | y \rangle$ or in $\langle A | y \rangle^p$ to be an occurrence of the variable $y$, so it is neither free nor bound. A **flat** formula contains neither explicit nor guarded substitutions.

For guarded substitutions, we restrict the formula $A$ that is substituted to be a unit: this restriction still provides us with a system strong enough for all our present purposes, while simplifying many definitions and proofs.

**Remark 5.** We write $\lceil A \rceil^S$ to denote the formula obtained from $A$ by adding $S$ to the range of every free variable occurrence in $A$, i.e., $\lceil x^R \rceil^S = x^{R \cup S}$. We often omit the braces to improve readability, for example writing $\lceil A \rceil^r$ for $\lceil A \rceil^{\{r\}}$ and $x^{p,r}$ for $x^{\{p,r\}}$.

**Definition 6.** We write $[A|y]$ to denote an **actual substitution**, that is, $[A|y]B$ denotes the formula that is obtained from $B$, by replacing every free variable occurrence $y^S$ in $B$ by $\lceil A \rceil^S$. We use $[A|_p y]B$ to denote a **protected actual substitution**, that is, $[A|_p y]B$ denotes the formula that is obtained from $B$ where every free occurrence $y^S$ in $B$ is replaced by $A$ whenever $p \in S$, and remains untouched whenever $p \notin S$.<fnref n="3" />

**Notation 7.** We use lower case Greek letters $\sigma, \nu, \tau, \rho, \eta, \mu$ to denote substitutions. Furthermore, if $B$ is a formula, and $V = \{v_1, v_2, \dots, v_n\}$ is a finite set of variables, and $A_1, \dots, A_n$ is a list of formulae, then $[A_i|v_i]_V B$ stands for the simultaneous actual substitution of all free occurrences of the variables $v_1, \dots, v_n$ in $B$ for $A_1, \dots, A_n$, respectively. In the same way we can define $\langle A_i|v_i \rangle_V B$ as the simultaneous explicit substitution of $\langle A_1|v_1 \rangle \dots \langle A_n|v_n \rangle$. But note that in the case of explicit substitution we need that none of the $v_i$ occurs freely in any of the $A_j$.

We often write $[A_i|v_i]_B B$ or $\langle A_i|v_i \rangle_B B$ to indicate the simultaneous substitutions of all the free variables of $B$. We often encounter guarded substitutions in pairs, and we write $\langle A|x, B|y \rangle^p$ as abbreviation for $\langle A|x \rangle^p \langle B|y \rangle^p$. Finally, we allow for empty explicit and guarded substitutions, denoting them both by $\epsilon$, and then we have $\epsilon A = A$ for all $A$.

**Definition 8.** The **size** of a formula $A$, denoted by $|A|$ is defined inductively as follows: For $A \in \mathcal{U}$ we have $|A| = 1$, for $A^R \in \mathcal{V}^R$ we have $|A| = 1 + |R|$, for $\otimes \in \mathcal{A} \cup \mathcal{C}$ we have $|B \otimes C| = |B| + |C|$, and we have $|\langle B|y \rangle C| = |\langle B|y \rangle^p C| = |B| + |C|$.

**Example 9.** Let $A = \langle 0|x \rangle^r \langle x \ a \ 0|y \rangle (y^{p,q} \vee y^{p,r})$, where $x, y \in \mathcal{V}$ and $p, q, r \in \mathcal{G}$, and $a \in \mathcal{A}$. The variable occurrence $x$ is bound by the guarded substitution $\langle 0|x \rangle^r$ and the variable occurrences $y^{p,q}$ and $y^{p,r}$ are bound by the explicit substitution $\langle x \ a \ 0|y \rangle$, and we have $|A| = 9$.

### B. Subatomic derivations

In this paper, we use the open deduction framework of deep inference [19], in which derivations are built with the same constructors that are used for formulae with additional constructors for vertical composition.

<footnote n="2">²We will make this formal in the next section.</footnote>

<footnote n="3">³As this will only be used when $A$ is a unit, we substitute just with $A$ instead of $\lceil A \rceil^S$ as in the general case.</footnote>
**Definition 10.** The set $\mathcal{D} = \{\Phi, \Psi, \Theta, \dots\}$ of (subatomic) pre-derivations, is defined by the grammar:

$$ \mathcal{D} ::= \mathcal{V}^{\mathcal{R}} | \mathcal{U} | \mathcal{D} \mathcal{A} \mathcal{D} | \mathcal{D} \mathcal{C} \mathcal{D} | \langle \mathcal{D} | \mathcal{V} \rangle \mathcal{D} | \\ \langle \mathcal{U} | \mathcal{V} \rangle^{\mathcal{G}} \mathcal{D} \quad \left| \quad \begin{array}{c|c} \mathcal{D} & \mathcal{D} \\ \hline \mathcal{D} & \mathcal{D} \end{array} \right. $$

The notions of bound and free variables carry over from formulae to derivations. In particular, in $\langle\Phi|y\rangle\Psi$, every occurrence of $y$ in $\Psi$ is **bound**, the substitution variable $y$ in $\langle\Phi|y\rangle$ is not considered an occurrence of the variable $y$, and every variable occurrence that is not bound is **free**. Similarly, a derivation is **flat** if it contains no explicit and no guarded substitution. We say that a derivation is **open** if it contains no units, i.e., every leaf in the syntax tree is a free variable that can be substituted into; and we say that a derivation is **closed** if it contains no free variables, i.e., no leaf in the syntax tree can be substituted into.

We note that because guarded substitutions always substitute units, no open derivation can contain guarded substitutions.

We can define the two maps **premise** and **conclusion**, pr, cn: $\mathcal{D} \to \mathcal{F}$, and the two maps **width** and **height**, w, h: $\mathcal{D} \to \mathbb{N}$ in the standard way.<fnref n="4" />

**Example 11.** Below are two pre-derivations:

$$ \Phi = \frac{\left( (x \mathbf{a} z) \wedge \frac{\left( \left\langle \begin{array}{c} w \wedge x \\ w \vee x \end{array} \right| y \right) y^p \mathbf{a} y^q}{(w^p \vee x^p) \mathbf{a} (w^q \vee x^q)} \right)}{\hat{\lambda}_{\mathbf{a}} \frac{(x \wedge (w^p \vee x^p)) \mathbf{a} (z \wedge (w^q \vee x^q))}{\hat{\lambda}_{\mathbf{a}}}} \quad (6) $$

and

$$ \Psi = \frac{(0 \mathbf{a} 1) \wedge \left( \left\langle \frac{\text{mix}}{w \vee 1} \frac{w \wedge 1}{w \vee 1} \mathbf{a} \frac{\text{mix}}{w \vee 0} \frac{w \wedge 0}{w \vee 0} \right\rangle \right)}{\hat{\lambda}_{\mathbf{a}} \frac{(0 \wedge (w \vee 1)) \mathbf{a} (1 \wedge (w \vee 0))}{\hat{\lambda}_{\mathbf{a}}}} \quad (7) $$

The first, $\Phi$, is open, because it contains no units. And the second, $\Psi$, is flat because it contains no explicit or guarded substitutions. The reader can ignore for now the labels at the vertical compositions, which will be defined below.

The width of $\Phi$ is 10 and its height is 4. Its premise is $(x \mathbf{a} z) \wedge \langle w \wedge x | y \rangle (y \mathbf{a} y)$ and its conclusion is $(x \wedge (w \vee x)) \mathbf{a} (z \wedge (w \vee x))$. The width of $\Psi$ is 6 and its height is 3. Its premise is $(0 \mathbf{a} 1) \wedge ((w \wedge 1) \mathbf{a} (w \wedge 0))$ and its conclusion is $(0 \wedge (w \vee 1)) \mathbf{a} (1 \wedge (w \vee 0))$.

In order to define derivations, i.e. correct pre-derivations, we need to put restrictions on each mode of vertical composition. The first, $\mathcal{D}/\mathcal{D}$ is the familiar **composition by inference**, the application of an inference rule. The second, $\mathcal{D}/\mathcal{D}^{\sim}$, is called **composition by expansion**, representing the application of an explicit or guarded substitution.

In the remainder of this section, we define this formally. As said before, in the subatomic setting, atoms are not the smallest entity of a derivation but behave like binary connectives. This is made explicit in the definition of the inference rules.

**Definition 12.** On the set $\mathcal{A} \cup \mathcal{C}$, we define the two operations **down-saturation** $\sim$ and **up-saturation** $\hat{\wedge}$ as follows: $\tilde{\lambda} = \tilde{\nu} = \vee$ and $\hat{\lambda} = \hat{\nu} = \wedge$ and $\hat{\mathbf{a}} = \tilde{\mathbf{a}} = \mathbf{a}$ for every $\mathbf{a} \in \mathcal{A}$. These operations can be extended to formulae: $\tilde{\mathcal{A}}$ and $\hat{\mathcal{A}}$ are obtained from a formula $\mathcal{A}$ by saturating all connectives down or up respectively, and leaving all variables and units unchanged.

**Definition 13.** A **subatomic rule scheme** is any of the following:

$$ \begin{align} \hat{\lambda} \circled{\circ} \frac{(x \hat{\oplus} y) \odot (z \oplus w)}{(x \odot z) \otimes (y \odot w)} & \quad \hat{\lambda} \circled{\circ} \frac{(x \oplus y) \odot (z \hat{\oplus} w)}{(x \odot z) \otimes (y \odot w)} \tag{8} \\ \tilde{\lambda} \circ \frac{(x \odot y) \otimes (z \odot w)}{(x \tilde{\oplus} z) \odot (y \otimes w)} & \quad \tilde{\lambda} \circ \frac{(x \odot y) \otimes (z \odot w)}{(x \oplus z) \odot (y \tilde{\oplus} w)} \nonumber \end{align} $$

where $\odot, \ominus \in \mathcal{A} \cup \mathcal{C}$. We call any inference rule generated by this scheme a **subatomic rule**.

We also use in this paper the following inference rules, which we call the **algebraic rules**:

$$ \begin{align} \mathfrak{s} \frac{x \wedge (y \vee z)}{(x \wedge y) \vee z} & \quad \mathfrak{ass} \frac{x \vee (y \vee z)}{(x \vee y) \vee z} & \quad \mathfrak{ass} \frac{x \wedge (y \wedge z)}{(x \wedge y) \wedge z} \tag{9} \\ \mathfrak{mix} \frac{x \wedge y}{x \vee y} & \quad \mathfrak{com} \frac{x \vee y}{y \vee x} & \quad \mathfrak{com} \frac{x \wedge y}{y \wedge x} \nonumber \end{align} $$

We define the proof system KSubG to be the set of all subatomic and algebraic rules.<fnref n="5" />

**Remark 14.** Note that KSubG is a **strictly linear system**, which does not have any inference rules that can create or delete information, even units [6].

**Definition 15.** An **instance** of an **inference rule** $\mathfrak{r} \frac{A}{B}$ is given by $\mathfrak{r} \frac{\eta A}{\eta B}$, where $\eta$ is an arbitrary actual substitution. A **proof system** $\mathcal{S}$ is a set of inference rules. We say that the composition by inference of two pre-derivations $\Phi$ and $\Psi$,

$$ \frac{\Phi}{\Psi} \text{ is correct (in } \mathcal{S}) \text{ if } \mathfrak{r} \frac{\text{cn } \Phi}{\text{pr } \Psi} \text{ is an instance of an inference rule in } \mathfrak{r} \in \mathcal{S}, \text{ and we write this as } \mathfrak{r} \frac{\Phi}{\Psi}. $$

**Definition 16.** On formulas, we define two binary **expansion relations** $\rightsquigarrow$ on and $\rightsquigarrow$.

$$ \begin{align} \sigma(A \oplus B) & \rightsquigarrow \sigma A \oplus \sigma B \nonumber \\ \langle C | x \rangle \langle A | y \rangle B & \rightsquigarrow \langle \langle C | x \rangle A | y \rangle \langle C | x \rangle B \tag{10} \\ \langle A | y \rangle D & \rightsquigarrow [A | y] D \nonumber \end{align} $$

<footnote n="4">⁴The detailed definition is in the appendix.</footnote>

<footnote n="5">⁵The reader familiar with subatomic systems might observe that the algebraic rules are not needed. We will come back to this point at the end of the next section.</footnote>
where $\sigma$ is a guarded or explicit substitution, and $\oplus \in A \cup C$, and $A, B, C$ are arbitrary formulas, and $D$ is a formula that does not contain any guarded substitutions.

$$ \begin{align} \langle U | y \rangle^p F &\rightsquigarrow [U |_p y] F \notag \\ \langle U | y \rangle^p \langle F | x \rangle E &\rightsquigarrow \langle [U |_p y] F | x \rangle E \tag{11} \\ \langle U | y \rangle^p E &\rightsquigarrow E \notag \end{align} $$

where $U \in \mathcal{U}$, and $F$ is a flat formula, and $E$ is a formula such that either $y$ does nor occur in $E$ (bound or free), or such that every variable occurrence in $E$ (bound or free) has a range $R$ with $p \notin R$.

**Definition 17.** Let $\Phi$ and $\Psi$ be pre-derivations. Their composition by expansion $\overset{\Phi}{\widetilde{\Psi}}$ is correct iff one of the following
$$ \text{cn} \Phi \rightsquigarrow \text{pr} \Psi \text{ or } \text{cn} \Phi \rightsquigarrow \text{pr} \Psi \text{ or } \text{pr} \Psi \rightsquigarrow \text{cn} \Phi . $$

**Definition 18.** Let $S$ be a set of inference rules. A *derivation in S* (or *S derivation*) is a pre-derivation in which every composition by inference is correct in $S$ and every composition by expansion is correct. We write $\Phi \parallel_S \mathbf{s}$ for a derivation $\Phi$ in $S$, $B$

where $S$ may be given as a rule scheme such as $\overset{\oplus\odot}{\ominus}$. If $S$ is empty then every vertical composition in $\Phi$ is by expansion; in this case we may instead annotate the derivation with its height.

**Example 19.** The two pre-derivations $\Phi$ and $\Psi$ given in Example 11 are derivations in KSubG, with the correct rule names indicated at the compositions by inference.

**Remark 20.** Our main contribution in this paper is to show that a strictly linear system equipped with explicit substitution of derivations and guarded substitutions of units can share and redistribute logical material very efficiently.

For this reason, the definition of the expansion relations $\rightsquigarrow$ and $\rightsquigarrow$ is more restrictive than necessary. For example, guarded substitutions can only be applied downwards in a derivation, and have a weaker distributive relation than explicit substitutions, which is all that we need to prove the main result in this paper. This restrictive definition makes it easy to see that the time complexity of checking correctness of a derivation is quadratic in the size of the derivation. Usually, in deep inference systems this is linear, because all rules are given either linearly or atomically. In KSubG it is linear for almost all cases, except for the composition by expansion of $\langle A | y \rangle D \rightsquigarrow [A | y] D$, which is quadratic because we additionally need to check that the ranges of the free occurrences of $y$ in $D$ are correctly inherited by the free variables in $A$. If we allow guarded substitutions to freely apply to formulae containing explicit substitutions, then it is not immediately obvious how to check correctness in polynomial time.

### C. Subatomic Merge

We end this section by presenting two crucial lemmas that are needed in many subatomic constructions, and that we

call merge lemmas. The first is a generalization of the merge contraction of [26] and of the generalized medial map of [23].

**Lemma 21.** Let $A$ be an open formula with $\underline{A} = \{x_1, \dots, x_n\}$. Then for all $\oplus \in A \cup C$ and $B_1, C_1, \dots, B_n, C_n \in \mathcal{F}$, there exist derivations

$$ \begin{align*} [B_i | x_i]_{\underline{A}} A \overset{\ominus}{\otimes} [C_i | x_i]_{\underline{A}} A & \qquad [B_i \oplus^{\ominus} C_i | x_i]_{\underline{A}} A \\ & \parallel \overset{\ominus\odot, \odot\ominus}{\otimes} \\ [B_i \overset{\ominus}{\otimes} C_i | x_i]_{\underline{A}} A & \qquad [B_i | x_i]_{\underline{A}} A \oplus^{\ominus} [C_i | x_i]_{\underline{A}} A \end{align*} $$

The height of each of these derivations is $O(|A|)$ and their width is $O(\sum (|B_i| + |C_i|))$.

The second merge lemma is a generalization of the construction that is usually used to show that in a well-designed system (sequent calculus or deep inference) the general identity axiom can be reduced to an atomic form.

**Lemma 22.** Let $A$ be an open formula with $\underline{A} = \{x_1, \dots, x_n\}$. Then for all $\oplus \in A \cup C$ and $B_1, C_1, \dots, B_n, C_n \in \mathcal{F}$, there exist derivations

$$ \begin{align*} [B_i \oplus^{\ominus} C_i | x_i]_{\underline{A}} \hat{A} & \qquad [B_i | x_i]_{\underline{A}} A \oplus^{\ominus} [C_i | x_i]_{\underline{A}} \bar{A} \\ & \parallel \overset{\ominus\odot, \ominus\odot}{\otimes} \\ [B_i | x_i]_{\underline{A}} A \oplus^{\ominus} [C_i | x_i]_{\underline{A}} \bar{A} & \qquad [B_i \oplus^{\ominus} C_i | x_i]_{\underline{A}} \tilde{A} \end{align*} $$

The height of each of these derivations is $O(|A|)$ and their width is $O(\sum (|B_i| + |C_i|))$.

### III. FROM SUBATOMIC PROOFS TO STANDARD PROOFS

#### A. Interpretation map

For translating subatomic formulae and derivations into standard formulae and derivations, we use **interpretation maps**. These are partial functions from subatomic derivations to standard derivations. They are partial, as not every subatomic formula has a standard correspondence.

While interpretation functions also exist for linear logics [2], in this paper we are solely concerned with classical propositional logic and therefore provide an interpretation function from the subatomic system with guarded substitutions KSubG, defined in the previous section, to the standard deep-inference proof system SKS [8], [11], [19].

**Definition 23.** We first define the set $\bar{A} = \{\bar{a}, \bar{b}, \bar{c}, \dots\}$ of *negated atoms*, and an in operation $\bar{\cdot}: A \to \bar{A}$, mapping each atom $a \in A$ to $\bar{a} \in \bar{A}$.

We can now define the set $\mathcal{F}' = \{A, B, C, \dots\}$ of *standard formulae*, and the set $\mathcal{D}'$ of *standard pre-derivations* as follows:

$$ \begin{array}{l} \mathcal{F}' ::= U \mid A \mid \bar{A} \mid \mathcal{F}' C \mathcal{F}' \\ \mathcal{D}' ::= U \mid A \mid \bar{A} \mid \mathcal{D}' C \mathcal{D}' \mid \frac{\mathcal{D}'}{\mathcal{D}'} \end{array} $$

The mapping $\bar{\cdot}$ is extended to all standard formulae by defining $\bar{\cdot}: \mathcal{F}' \to \mathcal{F}'$ inductively as

$$ \bar{a} = a \quad \bar{0} = 1 \quad \bar{1} = 0 \quad \overline{A \wedge B} = \bar{A} \vee \bar{B} \quad \overline{A \vee B} = \bar{A} \wedge \bar{B} $$
We inherit all the applicable definitions from Section II, noting that in standard systems atoms behave like units, and not like connectives, and we have neither explicit nor guarded substitutions and therefore no composition by expansion.

We define **standard derivations** to be correct standard pre-derivations according to the inference rules of SKS [8], [11], [19],<fnref n="6" /> which is sound and complete for classical propositional logic.

**Definition 24.** Let $\Phi$ and $\Psi$ be two standard derivations such that $\text{cn } \Phi = \text{pr } \Psi$. A **synchronial composition** of $\Phi$ and $\Psi$ is a standard derivation, denoted $\begin{array}{c} \Phi \\ \vdots \\ \Psi \end{array}$, that can inductively obtained as follows:

$$ \begin{array}{l} \text{if } \Phi \in \mathcal{F}', \text{ then } \begin{array}{c} \Phi \\ \vdots \\ \Psi \end{array} = \Psi; \quad \text{if } \Psi \in \mathcal{F}', \text{ then } \begin{array}{c} \Phi \\ \vdots \\ \Psi \end{array} = \Phi; \\[2ex] \text{if } \Phi = \frac{\Phi_1}{\Phi_2}, \text{ then } \begin{array}{c} \Phi \\ \vdots \\ \Psi \end{array} = \begin{array}{c} \Phi_1 \\ \vdots \\ \Psi_2 \end{array}; \quad \text{if } \Psi = \frac{\Psi_1}{\Psi_2}, \text{ then } \begin{array}{c} \Phi \\ \vdots \\ \Psi \end{array} = \begin{array}{c} \Phi \\ \vdots \\ \Psi_2 \end{array}; \\[2ex] \text{if } \left\{ \begin{array}{l} \Phi = \Phi_1 \oplus \Phi_2, \\ \text{and } \Psi = \Psi_1 \oplus \Psi_2, \\ \text{with } \oplus \in \mathcal{C} \end{array} \right. \text{, then } \begin{array}{c} \Phi \\ \vdots \\ \Psi \end{array} = \begin{array}{c} \Phi_1 \\ \vdots \\ \Psi_1 \end{array} \oplus \begin{array}{c} \Phi_2 \\ \vdots \\ \Psi_2 \end{array}. \end{array} $$

Note that this operation is not necessarily uniquely defined. But whenever we use this notation, any synchronial composition of $\Phi$ and $\Psi$ can be used.

**Definition 25.** We define the (partial) **interpretation map** $[[\cdot]] : \mathcal{D} \to \mathcal{D}'$ from subatomic derivations to standard derivations as indicated in Figure 2. On the top of that figure we show the case analysis for the base case $[[\Phi \ a \ \Psi]]$.

**Proposition 26.** If $\Phi$ is a subatomic derivation in KSubG and $[[\Phi]]$ is defined, then $[[\Phi]]$ is a standard derivation in SKS.

**Example 27.** Let us look again at the two derivations in Example 11. Both $[[\Phi]]$ and $[[\Psi]]$ are undefined. However, we have

$$ [[\langle 0 | w \rangle \Psi]] = \underset{\text{ai}\uparrow}{a \wedge \begin{array}{c} \text{aw}\downarrow \\ 0 \end{array}} \quad \text{and} \quad [[\langle 1 | w \rangle \Psi]] = \underset{\text{a}}{a \wedge \begin{array}{c} \text{aw}\uparrow \\ \frac{\bar{a}}{1} \end{array}} $$

**Remark 28.** It should be noted that the size of $[[\Phi]]$ is not polynomially bounded by $\Phi$ since all explicit and guarded substitutions are converted to actual substitutions. Nevertheless in some situations we need not perform every substitution in order to determine the interpretation, so that it may be computed in polynomial time. An example is given by the Proposition below.

**Proposition 29.** Let A be an open formula with free variables $\{v_1, \dots, v_n\}$ and let $B_1, \dots, B_n$ be formulae. If $[[B_1]] = \dots = [[B_n]] = U \in \mathcal{U}$ then $[[\langle B_i | v_i \rangle_A A]] = U$.

$$ \begin{array}{c} [[\Phi \ a \ \Psi]] : \\ \begin{array}{c} [[\Phi]] = 1 \\ [[\Phi]] = 0 \\ [[\text{pr } \Phi]] = 0 \\ [[\text{cn } \Phi]] = 1 \end{array} \end{array} \quad \begin{array}{c} [[\Psi]] = 1 \\ 1 \\ a \\ \frac{a}{1} \end{array} \quad \begin{array}{c} [[\Psi]] = 0 \\ \bar{a} \\ 0 \\ \frac{\bar{a}}{1} \end{array} \quad \begin{array}{c} [[\text{pr } \Psi]] = 0 \\ [[\text{cn } \Psi]] = 1 \\ \frac{\bar{a}}{1} \\ \frac{0}{a} \\ \frac{0}{1} \end{array} \end{array} $$

$[[1]] = 1,$

$[[0]] = 0,$

$$ [[\Phi \wedge \Psi]] = \begin{cases} \text{undefined} & \text{if one of } [[\Phi]], [[\Psi]] \text{ is undefined} \\ [[\Phi]] & \text{if } [[\Psi]] = 1 \\ [[\Psi]] & \text{if } [[\Phi]] = 1 \\ 0 & \text{if } [[\Phi]] = 0 \text{ and } [[\Psi]] = 0 \\ [[\Phi]] \wedge [[\Psi]] & \text{otherwise} \end{cases} $$

$$ [[\Phi \vee \Psi]] = \begin{cases} \text{undefined} & \text{if one of } [[\Phi]], [[\Psi]] \text{ is undefined} \\ [[\Phi]] & \text{if } [[\Psi]] = 0 \\ [[\Psi]] & \text{if } [[\Phi]] = 0 \\ 1 & \text{if } [[\Phi]] = 1 \text{ and } [[\Psi]] = 1 \\ [[\Phi]] \vee [[\Psi]] & \text{otherwise} \end{cases} $$

$$ [[\langle \Phi | x \rangle \Psi]] = \begin{cases} [[\Phi | x] \Psi] & \text{if } [[\Phi]] \text{ and } [[\Psi]] \text{ are both defined} \\ \text{undefined} & \text{otherwise} \end{cases} $$

$$ [[\langle \Phi | x \rangle^p \Psi]] = \begin{cases} [[\Phi]_p | x] \Psi & \text{if } [[\Phi]] \text{ and } [[\Psi]] \text{ are both defined} \\ \text{undefined} & \text{otherwise} \end{cases} $$

$$ \left[ \left[ \frac{\Phi}{\Psi} \right] \right] = \begin{cases} \frac{[\Phi]}{[\Psi]} & \text{if } [[\Phi]] \text{ and } [[\Psi]] \text{ are both defined} \\ \frac{[\Phi]}{[\Psi]} & \text{and } [[\text{cn } \Phi]] \neq [[\text{pr } \Psi]] \\ \frac{[\Phi]}{[\Psi]} & \text{if } [[\Phi]] \text{ and } [[\Psi]] \text{ are both defined} \\ \frac{[\Phi]}{[\Psi]} & \text{and } [[\text{cn } \Phi]] = [[\text{pr } \Psi]] \\ \text{undefined} & \text{otherwise} \end{cases} $$

$$ \left[ \left[ \frac{\Phi}{\Psi} \right] \right] = \begin{cases} \frac{[\Phi]}{[\Psi]} & \text{if } [[\Phi]] \text{ and } [[\Psi]] \text{ are both defined} \\ \frac{[\Phi]}{[\Psi]} & \text{and } [[\text{cn } \Phi]] = [[\text{pr } \Psi]] \\ \frac{[\Phi]}{[\Psi]} & \text{otherwise} \end{cases} $$

<caption>Fig. 2. The interpretation map $[[\cdot]] : \mathcal{D} \to \mathcal{D}'$</caption>

## B. Soundness and Completeness

The main purpose of the interpretation map is to carry the soundness and completeness of SKS to KSubG.

**Definition 30.** A **(subatomic) proof** is a derivation $\Phi$ such that $[[\text{pr } \Phi]] = 1$. A subatomic formula $A$ is **provable** in KSubG if there is a proof $\Phi$ in KSubG with $\text{cn } \Phi = A$, and a standard formula $A$ is **provable** in KSubG if there is a proof $\Phi$ in KSubG with $[[\text{cn } \Phi]] = A$.

**Theorem 31.** Let A be a standard formula. The following are equivalent:

1) A is a Boolean tautology.

2) A is provable in SKS.

3) A is provable in KSubG.

<footnote n="6">⁶For convenience, we give the inference rules of SKS in the appendix.</footnote>
4) A is provable in KSubG without the algebraic rules.

**Remark 32.** The equivalence of 3) and 4) in Theorem 31 indicates that the algebraic rules of (9) are, in fact, not needed. However, the presentation of the technicalities in the following sections greatly benefits from the presence of the algebraic rules and therefore they are included in KSubG.

## IV. CUT FREENESS AND SUPERPOSITION OF PROOFS

### A. Cuts and projections in subatomic systems

Figure 1 in the introduction shows that the atomic cut rule $a↑$ is the interpretation of an instance of the $\hat{a}∧$. This motivates the following definition.

**Definition 33.** A (subatomic) cut is an instance of the rule scheme $\hat{a}∧$ or $∧\hat{a}$ shown below:

$$ \hat{a} \wedge \frac{(x \mathbf{a} \ y) \wedge (z \mathbf{a} \ w)}{(x \wedge z) \ \mathbf{a} \ (y \wedge w)} \quad (12) $$

A subatomic proof system is cut-free if it does not contain any cuts. We denote by KSubG<sup>-</sup> the cut-free fragment of KSubG, that is, KSubG with the rules $\hat{a}∧$ and $∧\hat{a}$ removed for all $a \in \mathcal{A}$.

This definition is justified by the following proposition which says that any interpretation of a proof in KSubG<sup>-</sup> is also cut-free in SKS.

**Proposition 34.** If $\Phi$ is a cut-free subatomic derivation then $[[\Phi]]$ contains no instances of the atomic cut rule. [4]

In [4] it has been shown that any subatomic proof can be transformed into a cut-free subatomic proof, and in [6] this result has been extended to the strictly linear proof system without unit equality inference steps.

In both cases, cut elimination is achieved via projections. The left-projection (resp. right-projection) of a derivation $\Phi$ with respect to an atom $a$, denoted by $l_a \Phi$ (resp. $r_a \Phi$) is obtained from $\Phi$ by discarding everything in the right (resp. left) scope of an atom and collapsing inference rules whenever possible.

**Example 35.** The left- and right-projections of

$$ \Phi = \wedge \hat{a} \frac{\boxed{a \tilde{\vee} \frac{(0 \mathbf{a} \ 1) \vee (0 \mathbf{a} \ 1)}{(0 \vee 0) \ \mathbf{a} \ (1 \vee 1)}} \wedge \boxed{\text{mix} \frac{1 \wedge 0}{1 \vee 0} \ \mathbf{a} \ \text{mix} \frac{0 \wedge 0}{0 \vee 0}}}{((0 \vee 0) \wedge (1 \vee 0)) \ \mathbf{a} \ ((1 \vee 1) \wedge (0 \vee 0))} $$

with respect to $a$ are

$$ l_a \Phi = (0 \vee 0) \wedge \text{mix} \frac{1 \wedge 0}{1 \vee 0} \qquad r_a \Phi = (1 \vee 1) \wedge \text{mix} \frac{0 \wedge 0}{0 \vee 0} $$

A subatomic derivation containing an atomic connective $a$ can be viewed as a juxtaposition of two derivations: the one in which that atom is false and the one in which it is true.

We can also read atomic connectives as decision trees [4], so that $AaB$ means “if $a$ is true then $B$ else $A$”. Correspondingly, the left-projection of a derivation with respect to $a$ is the

derivation in which that atom is false, and its right-projection is the derivation in which it is true.

The left- and right-projections can then be recombined to obtain a formula which is equivalent under the interpretation map to the conclusion of the original proof:

$$ \frac{(l_a \Phi) \ \mathbf{a} \ (r_a \Phi)}{\Xi \parallel C} \quad (13) $$

where $Ξ$ is a cut-free subatomic derivation. In a strictly linear proof system, where unit equality inference steps are not available, Lemma 21 can be applied, so any leaves $v$ or $u$ which are not in the scope of $a$ in $c \nabla \Phi$ are replaced by $v \mathbf{a} v$ or $u \mathbf{a} u$ in $C$, which are nevertheless interpreted as $v$ or $u$. Examples of this are given in [6].

The construction of $Ξ$ in (13) above, as detailed out in [4] and [6], can also be applied to our system. However, as in [4] and [6], this construction would lead to an exponential blow-up in the size of the proof. For this reason, we will not repeat that construction here, as we will prove a much stronger result in Section VI below.

### B. Superpositions

One of the insights of our work is that if the translation of a standard derivation (SKS or Frege) into subatomic logic is done carefully, then the underlying structure of projections will match. The following example shows that this is not immediate.

**Example 36.** The projections of $\Phi$ given in Example 35 have matching structures, in the sense that there exists a derivation

$$ \Psi = (x \vee x) \wedge \text{mix} \frac{y \wedge 0}{y \vee 0} $$

such that $[0|x, 1|y] \Psi = l_a \Phi$ and $[1|x, 0|y] \Psi = r_a \Phi$.

The interpretation of $\Phi$ is

$$ [[\Phi]] = \mathbf{a} \uparrow \frac{\boxed{\mathbf{a} \vee \mathbf{a}}}{\mathbf{a}} \wedge \boxed{\mathbf{a} \vee \mathbf{0}}}{\mathbf{a} \uparrow \mathbf{0}} $$

exhibiting a contraction, a weakening, and a cut.

However, the derivation

$$ \Theta = \wedge \hat{a} \frac{\boxed{a \tilde{\vee} \frac{(0 \mathbf{a} \ 1) \vee (0 \mathbf{a} \ 1)}{(0 \vee 0) \ \mathbf{a} \ (1 \vee 1)}} \wedge \boxed{\text{mix} \frac{1 \wedge 0}{1 \vee 0} \ \mathbf{a} \ 0}}{((0 \vee 0) \wedge (1 \vee 0)) \ \mathbf{a} \ ((1 \vee 1) \wedge 0)} $$

has the same interpretation as $\Phi$, but its projections do not match:

$$ l_a \Theta = (0 \vee 0) \wedge \text{mix} \frac{1 \wedge 0}{1 \vee 0} \qquad r_a \Theta = (1 \vee 1) \wedge 0 $$

**Definition 37.** We say that $\Psi$ is a superposition of $\Phi$ with respect to an atom $a$ if there exist free variables $x$ and $y$ in $\Psi$ such that $[0|x, 1|y] \Psi = l_a \Phi$ and $[1|x, 0|y] \Psi = r_a \Phi$.
As said before, the method of cut elimination given in [6] increases the size of a proof exponentially: to eliminate all of the cuts from a proof $\Phi$, we project with respect to each atom in turn and merge the conclusions. Since the left- and right-projections can be almost as large as the original derivation, the elimination of each atom can double the size of the proof. However, by bringing together superpositions and guarded substitutions, we are able to compress this construction.

**Example 38.** If $\Psi$ is a superposition of $\Phi$ with respect to $a$, then we can construct:

$$ \langle\langle 0|x, 1|y \rangle\rangle^l \langle\langle 1|x, 0|y \rangle\rangle^r \frac{\left[ \frac{\langle\langle \Psi|z \rangle\rangle^l a z^r}{\lceil \text{cn}\,\Psi \rceil^l a \lceil \text{cn}\,\Psi \rceil^r} \right]}{[0|x, 1|y] \lceil \text{cn}\,\Psi \rceil^l a [1|x, 0|y] \lceil \text{cn}\,\Psi \rceil^r} $$

which has the same conclusion as $l_a \Phi a r_a \Phi$ but is in general much smaller because $O(|\Psi|) = O(|l_a \Phi|) = O(|r_a \Phi|)$.

This idea forms the basis of how we are able to polynomially simulate substitution Frege systems with our cut-free system KSubG$^-$.

## V. SUBSTITUTION FREGE

To substantiate our claim that guarded substitutions are a highly effective means of proof compression, we compare our cut-free system KSubG$^-$ to substitution Frege systems [13], which are a class of p-equivalent systems for propositional logic with a substitution rule. No system is known to be more powerful than substitution Frege systems in compressing the size of proofs, and this therefore serves as a benchmark. In this section, we show that any substitution Frege proof can be transformed into a KSubG$^-$ proof with only a polynomial increase in size.

**Definition 39.** A *Frege substitution* is a function $\rho: A \to F'$ which is the identity almost everywhere.

We use for Frege substitutions the same notation as for actual substitutions, i.e., if $\{a_1, \dots, a_n\}$ is the set of atoms on which $\rho$ is not the identity, and $\rho = \{a_1 \mapsto A_1, \dots, a_n \mapsto A_n\}$ then

$$ \rho B = [A_1|a_1, \dots, A_n|a_n] B \qquad (14) $$

is the formula obtained from $B$ by simultaneously replacing all occurrences of $a_i$ with $A_i$ and all occurrences of $\bar{a}_i$ with $\bar{A}_i$ for all $i \in \{1, \dots, n\}$.

**Definition 40.** A *Frege proof with substitution* $\Phi = P_1, \dots, P_h$ is a finite sequence of standard formulae such that for every $i \in \{1, \dots, h\}$, the formula $P_i \in F'$ is one of the following:

* An instance of one of the axioms below:

$$ F_1 = \bar{A} \lor (B \lor A) $$

$$ F_2 = (A \land (B \land \bar{C})) \lor ((A \lor \bar{B}) \lor (\bar{A} \lor C)) $$

$$ F_3 = (\bar{A} \land B) \lor (\bar{B} \lor A) $$

$$ F_4 = 1 $$

* The conclusion of an instance of the *modus ponens rule*:

$$ \text{mp} \frac{A \quad \bar{A} \lor B}{B} \qquad (15) $$

where the premises are $P_k$ and $P_l$ for some $k, l < i$.

* The conclusion of the *substitution rule*:

$$ \text{sub} \frac{B}{\rho B} \qquad (16) $$

where the premise is $P_k$ for some $k < i$, and $\rho$ is an arbitrary Frege substitution.

The conclusion of $\Phi$ is $P_h$, the size is given by $|\Phi| = \sum |P_i|$, and the width by $\max |P_i|$. We denote by sFrege the proof system that comprises all Frege proofs with substitution.

**Definition 41.** We denote by sFrege$_{01}$ the proof system that comprises all Frege proofs with substitution where for every instance of the substitution rule, the image of the substitution $\rho$ is $U$, i.e., all formulae $A_1, \dots, A_n$ in (14) are either 0 or 1.

In the case of sFrege$_{01}$, we can write (14) as follows

$$ \rho B = [A_1|a_1, \dots, A_n|a_n] B = [A_1|a_1] \dots [A_n|a_n] B $$

**Theorem 42.** sFrege and sFrege$_{01}$ are p-equivalent. [12]

We are now ready to state the main theorem of this paper.

**Theorem 43.** System KSubG$^-$ p-simulates sFrege.

In other words, there is a $k \in \mathbb{N}$ such that for every sFrege proof $\Phi = P_1, \dots, P_h$, there is a derivation $\Psi$ in KSubG$^-$, such that $[[\text{pr}\,\Psi]] = 1$ and $[[\text{cn}\,\Psi]] = P_h$ and $|\Psi| = O(|\Phi|^k)$.

The following section is dedicated to the proof of Theorem 43. We will make use of Theorem 42, and show p-simulation of sFrege$_{01}$, as this simplifies the presentation.

## VI. P-SIMULATION OF SUBSTITUTION FREGE

The proof of Theorem 43 will be in three phases. In the first phase, we construct a KSubG$^-$ derivation $\Psi$ which tracks the relations between formulae in a given sFrege$_{01}$ proof $\Phi$, using explicit substitutions and ranges.

This derivation is cut-free; in fact, it contains no atomic connectives at all. We can view this derivation as a superposition with respect to every atom which occurs in the sFrege$_{01}$ proof $\Phi$. The atoms in $\Phi$ correspond to variables in $\Psi$, in the same way that the atom $a$ corresponds to the variables $x$ and $y$ in Example 36.

The second and the third phase of the simulation take the derivation $\Psi$ produced in the first phase and apply a rearrangement of subformulas (phase 2) and guarded substitutions (phase 3) to obtain a proof in KSubG$^-$ whose interpretation is a proof of the conclusion of the Frege proof $\Phi$.

### A. Simulating mp and sub in KSubG$^-$

In a sFrege$_{01}$ proof, a formula can act as a premise for multiple applications of the mp and sub rules.

**Example 44.** Consider a sFrege$_{01}$ proof $P_1, \dots, P_h$ which contains the following fragment:
$$P_{k-2} = ((\bar{a} \lor a) \land (b \land \bar{b})) \lor (c \lor \bar{c})$$

$$P_{k-1} = \bar{a} \lor a$$

$$P_k = (a \land \bar{a}) \lor (\bar{b} \lor b)$$

$$P_{k+1} = (1 \land 0) \lor (\bar{b} \lor b) \quad (\text{sub}(P_k))$$

$$P_{k+2} = \bar{b} \lor b \quad (\text{mp}(P_{k-1}, P_k))$$

$$P_{k+3} = c \lor \bar{c} \quad (\text{mp}(P_k, P_{k-2}))$$

$$P_{k+4} = (a \land \bar{a}) \lor (0 \lor 1) \quad (\text{sub}(P_k))$$

Then $P_k$ is used as a premise in obtaining $P_{k+1}$, $P_{k+2}$, $P_{k+3}$, and $P_{k+4}$.

It has been shown in [9] that SKS p-simulates Frege systems, and that SKS extended by a substitution rule p-simulates sFrege.<fnref n="7" /> In order to simulate instances of mp, it is assumed in [9] that the conjunction of all previous lines of the proof is proven. The premises for the mp inference steps are duplicated via cocontractions and used to prove the mp conclusion using switch and cut. In a strictly linear proof system, it is cumbersome to duplicate and permute formulae, but we can profit from using explicit substitutions instead.

**Example 45.** The applications of modus ponens in Example 44 could be simulated by a construction like the following:

$$\langle P_k | y_k \rangle \langle P_{k-1} \land y_k | y_{k+2} \rangle \langle y_k \land P_{k-2} | y_{k+3} \rangle \dots y_h \\ \text{\Large{\left|}} \begin{array}{c} P_{k-1} \land P_k \\ \Psi_{k+2} \parallel S \\ P_{k+2} \end{array} \text{\Large{\right|}} \text{\Large{\left|}} \begin{array}{c} P_k \land P_{k-2} \\ \Psi_{k+3} \parallel S \\ P_{k+3} \end{array} \text{\Large{\right|}} \dots y_h$$

where $\Psi_{k+2}$ and $\Psi_{k+3}$ perform the modus ponens in some proof system $S$, and each $y_i$ is a fresh variable. That is, each successive step of the sFrege<sub>01</sub> proof is proven inside an explicit substitution, and then the formula is substituted every time the conclusion is used further down in the proof.

Note that this construction is not yet precise; in particular $\Psi_{k+2}$ and $\Psi_{k+3}$ are not strictly linear, and the formulae are not translated into subatomic logic.

In SKS, atomic cuts, switches and unit equality rules are used to cancel out the antecedent $A$ of modus ponens (15) and its negation $\bar{A}$ in the other premise, and the resulting formula $B$ can then be used as a premise in future inference steps (just as in sFrege) without duplicating any material unnecessarily.

In our strictly linear system, unit equality inference steps are not available, and so we are unable to destroy the cut formulae. Instead of cuts, we can use explicit substitutions to ensure that when we substitute the conclusion into future inference steps, we do not bring along material which will blow up the size of the proof, using Lemma 22 to transform $A \land \bar{A}$ into a formula composed entirely of conjunctions of 1 and 0, which will therefore vanish under the interpretation function.

But observe that we would need the derivation on the right in Lemma 22, using the rules $\hat{\odot} \land$ and $\land \hat{\odot}$. If $\odot \in A$ then

this derivation will not be cut-free. For this reason, we have to ensure that our derivation $\Psi$ does not contain any atomic connectives, and so we use instead a superposition. The atomic connectives are recovered in a later phase in the construction.

Besides having to simulate modus ponens, we also need a way of dealing with substitution inference steps. Not only are we constrained by the linearity of our proof system, but also by how we can apply substitutions. In sFrege<sub>01</sub>, substitutions arrive ex nihilo: we can proceed from $C$ to $[B|a]C$, for any formula $B$. This is not allowed in KSubG, where substitutions only move between being explicit and actual: we must proceed from $\langle B|a \rangle C$ to $[B|a]C$.

Nevertheless the finer control over where substitutions apply afforded by guarded substitutions allows us to simulate the substitutions of sFrege<sub>01</sub>.

**Example 46.** In Example 44, the substitution rule is applied twice to $P_k$, to obtain $P_{k+1}$ and $P_{k+4}$. In order to achieve the same proof compression as sFrege<sub>01</sub>, we want to prove $P_k$ once and reuse it, without any conflict between the substitutions.

Limiting ourselves to explicit substitutions, and using the idea from Example 45 we might consider derivations with either of the premises

$$\langle 1 | x_b \rangle \langle 0 | \tilde{x}_b \rangle \langle 1 | x_a \rangle \langle 0 | \tilde{x}_a \rangle \langle P_k | y_k \rangle \langle y_k | y_{k+1} \rangle \langle y_k | y_{k+4} \rangle \dots y_h$$

$$\langle P_k | y_k \rangle \langle \langle 1 | x_a \rangle \langle 0 | \tilde{x}_a \rangle y_k | y_{k+1} \rangle \langle \langle 1 | x_b \rangle \langle 0 | \tilde{x}_b \rangle y_k | y_{k+4} \rangle \dots y_h $$

where the variables $x_a$ and $\tilde{x}_a$ represent the atom $a$ (see Example 36), and the variable $x_b$ and $\tilde{x}_b$ represent the atom $b$, and the explicit substitutions $\langle 1 | x_b \rangle$, $\langle 0 | \tilde{x}_b \rangle$, $\langle 1 | x_a \rangle$, and $\langle 0 | \tilde{x}_a \rangle$ are intended to simulate the substitution inference steps. In the first case, the substitutions $\langle 1 | x_a \rangle$ and $\langle 0 | \tilde{x}_a \rangle$ will also catch $P_{k+4}$; in the second case, we would need to apply $\langle P_k | y_k \rangle$ in a variable capturing way, which we cannot do. However, by introducing guarded substitutions, we can use the premise

$$\langle 1 | x_b, 0 | \tilde{x}_b \rangle^s \langle 1 | x_a, 0 | \tilde{x}_a \rangle^r \langle P_k | y_k \rangle \langle y_k^r | y_{k+1} \rangle \langle y_k^s | y_{k+4} \rangle \dots y_h$$

which can be expanded as

$$\langle 1 | x_b, 0 | \tilde{x}_b \rangle^s \quad \langle 1 | x_a, 0 | \tilde{x}_a \rangle^r \quad \langle P_k | y_k \rangle \langle y_k^r | y_{k+1} \rangle \langle y_k^s | y_{k+4} \rangle \dots y_h \\ \quad \langle \lceil P_k \rceil^r | y_{k+1} \rangle \langle \lceil P_k \rceil^s | y_{k+4} \rangle \dots y_h \\ \quad \langle [1 | x_a, 0 | \tilde{x}_a] \lceil P_k \rceil^r | y_{k+1} \rangle \langle \lceil P_k \rceil^s | y_{k+4} \rangle \dots y_h $$

$$\langle [1 | x_a, 0 | \tilde{x}_a] \lceil P_k \rceil^r | y_{k+1} \rangle \langle [1 | x_b, 0 | \tilde{x}_b] \lceil P_k \rceil^s | y_{k+4} \rangle \dots y_h $$

in order to obtain the formulae $P_{k+1}$ and $P_{k+4}$. We note that this construction accumulates the ranges $r$ and $s$, so that the size of these formulae grow, but this will not have a greater than polynomial effect on the size of the construction.

## B. From Standard Formulae to Subatomic Formulae

Every line in a sFrege<sub>01</sub> proof is a standard formula. We now show how we translate such a standard formula into a subatomic formula.

**Definition 47.** An actual substitution is *elementary* if it maps variables only to units or variables. An actual substitution $\sigma$

<footnote n="7">⁷In fact the authors of [9] use the variant SKS<sub>g</sub>, obtained from SKS by loosening the restriction that the structural rules should be atomic, but it is very straightforward to show p-equivalence between SKS and SKS<sub>g</sub>.</footnote>
closes a formula A if $\sigma A$ is closed. An actual substitution $\sigma$ is dualising with respect to two variables $x$ and $y$ if $\sigma x = \overline{\sigma y}$.

**Definition 48.** We call any finite sequence of positive and negative atoms $A_n = \{a_1, \bar{a}_1, \dots, a_n, \bar{a}_n\}$ an atomic enumeration. If $\Phi$ is an sFrege<sub>01</sub> proof, we write $A_\Phi$ for the set of atoms appearing in $\Phi$, including the pair of dual atoms, even if only one of the pair appears in the proof. Given an injective map from $v: A \to V$, we define a variable enumeration, $V_{A_n}$ to be the image of an atomic enumeration $A_n$, writing $V_n$ for $V_{A_n}$ and $V_\Phi$ for $V_{A_\Phi}$. We call the image of dual atoms $a_j$ and $\bar{a}_j$ in a variable enumeration $V_n$ pseudo-dual variables, writing them as $v(a_j) = x_j$ and $v(\bar{a}_j) = \tilde{x}_j$, but we emphasise that this is not an extension of the negation operation $\neg$ to variables. Instead, for a subatomic formula $A$, given a variable enumeration $V_n$ we can define the pseudo-dual formula $\tilde{A}$ to be $[\tilde{x}_i|x_i]_A \tilde{A}$.

**Definition 49.** Given an atomic enumeration $A_n$ with variable enumeration $V_n$, and a subatomic formula $A$ with $A \subseteq V_n$, we say that $A$ is tautological with respect to $V_n$ if for every elementary substitution $\eta$ which is dualising with respect to all pseudo-dual variables, we have $[\eta A] = 1$, and it is contradictory with respect to $V_n$ if $[\eta A] = 0$.

**Definition 50.** Given a formula $Q$, we define its factorisation to be composed of two parts: an open formula $A$ whose every variable appears only once and an elementary substitution $\eta$, such that $\eta A = Q$. We note that the factorisation is unique modulo the choice of free variables of $A$, and assume in general that these are chosen to be fresh variables.

We now give the translation that we will use to translate formulae of an sFrege<sub>01</sub> proof to the subatomic system.

**Definition 51.** Let $A_n$ be an atomic enumeration with variable enumeration $V_n$, and let $P$ be a standard formula whose every atom is in $A_n$. We obtain the open translation $Q$ of $P$ by replacing each atom by its image under the given variable enumeration, so that $Q \subseteq V_n$. We can then factorise $Q$ to obtain an open formula $A$ and an elementary substitution $\eta$ such that $\eta A = Q$; we call the pair $(\eta, A)$ the factorised (open) translation of $P$. For any two standard formulas $P_i, P_j$, we assume without loss of generality that in their factorised translations $A_i \cap A_j = \emptyset$.

It is important to note that the factorised open translation does not contain any atomic connectives, but that we have replaced each atom by an associated variable. This guarantees that we will not use the cut rule in the first phase of the simulation, because there are no atoms to cut.

**Proposition 52.** Let $A_n$ be an atomic enumeration with variable enumeration $V_n = \{x_1, \tilde{x}_1, \dots, x_n, \tilde{x}_n\}$ and let $P$ be a standard formula with factorised translation $(\eta, A)$. Then $[[0 \ a_j \ 1|x_j, 1 \ a_j \ 0|\tilde{x}_j]]_{1 \le j \le n} \eta A] = P$.

### C. Phase I: Superposition

**Convention 53.** In all the following we will use:

* $\sigma, \nu$ to denote guarded substitutions $\langle A|y \rangle^p$

* $\tau$, to denote explicit substitutions $\langle A|y \rangle$

* $\rho, \eta, \mu$ to denote actual substitutions $[A|y]$

**Construction 54.** Let $\Phi = P_1, \dots, P_h$ be an sFrege<sub>01</sub> proof, with atomic enumeration $A_\Phi$, variable enumeration $V_\Phi$, and factorised open translation $(\eta_1, A_1), \dots, (\eta_h, A_h)$.

For each line $P_i$ of the sFrege<sub>01</sub> proof $\Phi$, we will construct:

* a cut-free derivation $\Psi_i$,

* explicit substitutions $\tau_i$,

* actual substitutions $\mu_i$ and $\rho_i$

* a guarded substitution $\sigma_i$

* a flat formula $B_i$

The premise of each derivation $\Psi_i$ will be determined by the premise(s) of the inference rule by which $P_i$ is obtained; when $P_i$ is an axiom, $\mathrm{pr} \ \Psi_i$ will be $B_i$ and otherwise the formula $B_i$ will allow us to substitute in the premise needed. The guarded substitution $\sigma_i$, which is non-empty only when $P_i$ is obtained by an application of substitution, will store the information of that substitution until a later phase in the simulation. The conclusion of $\Psi_i$ will be $\tau_i z_i \lor \rho_i \mu_i A_i$, where $z_i$ is a fresh variable. The explicit substitution $\tau_i$ allows us to control the accumulation of logical material from applications of modus ponens, the actual substitution $\rho_i$ allows us to accumulate ranges so that the guarded substitutions apply correctly, and the actual substitution $\mu_i$ aids in giving strictly linear simulations of the axioms which make use of weakening and contraction. We fix a set of fresh variables $\{y_1, \dots, y_h\}$, which we will use in Construction 59 to link these pieces together.

First suppose that $P_i$ is obtained from an axiom. We only show here the case for $F_1$, the others being similar (and shown in the appendix). We have that $A_i$ is of the form $X' \lor (Y \land X)$, where $\eta_i X'$ and $\eta_i X$ are pseudo-dual formulae. For a variable $v \in X$, we denote by $v'$ the variable in $X'$ appearing in the corresponding position, and we note that $\eta_i v$ and $\eta_i v'$ are pseudo-dual. With use of Lemma 22 we construct:

$$ \Psi_i = \underbrace{0}_{\langle 0|z_i \rangle z_i} \lor \eta_i \quad \left[ \begin{array}{@{}c@{\,}c@{}} \text{mix} & \left[ \begin{array}{@{}c@{\,}c@{}} v \land 0 & v \\ v \lor 0 & \multicolumn{1}{@{}c@{}}{\boxed{v}} \end{array} \right]_{\mathcal{Y}} \quad \begin{array}{@{}c@{}} Y \lor \\ \mathcal{Y}' \end{array} & \left[ \begin{array}{@{}c@{}} [v' \lor v|v]_{\mathcal{X}} \hat{X} \\ \|_{\tilde{\mathcal{X}} \lor v \tilde{\mathcal{X}}} \\ X' \lor X \end{array} \right]_{\mathcal{X}} \\ \|_{\tilde{\mathcal{A}}\tilde{s}, \mathbb{C}\mathbb{m}} & X' \lor \left( [v \lor 0|v]_{\mathcal{Y}} \lor X \right) \end{array} \right. $$

and we obtain the substitutions $\tau_i = \langle 0|z_i \rangle$, $\rho_i = \eta_i$, $\mu_i = [v \lor 0|v]_{\mathcal{Y}}$, $\sigma_i = \epsilon$, and the formula $B_i = 0 \lor \eta_i ([v \land 0|v]_{\mathcal{Y}} \lor [v' \lor v|v]_{\mathcal{S}} \hat{X})$.

Next suppose that $P_i$ is obtained from an application of modus ponens, so that there exist $k, l < i$ such that $P_l = \tilde{P}_k \lor P_i$. Then $A_l$ is of the form $A_{k,l} \lor A_{i,l}$, where $\eta_l A_{k,l}$ and $\eta_k A_k$ are pseudo-dual formulae and $\eta_l A_{i,l} = \eta_i A_i$. For a variable $v$ occurring in $A_k$, we denote by $v'$ the variable occurring in $A_{k,l}$ in the corresponding position, and we note that $\eta_k v$ and $\eta_l v'$ are pseudo-dual. Then by Lemma 22, we construct:
**Proposition 62.** Let $A_n$ be an atomic enumeration and let $V_n$ be a variable enumeration. Let $A$ be a formula such that $A \subseteq V_n$. If $A$ is a tautology (resp. contradiction) with respect to $V_n$ then $[\nu_n \dots \nu_1 \langle A | y \rangle E_n(y)] = 1$ (resp. 0).

**Lemma 63.** Let $A_n$ be an atomic enumeration, let $y$ be a variable and let $A$ be a flat open formula. Then there exists $\langle A | y \rangle E_n(y)$ a KSubG$^-$ derivation $\|\circ\tilde{a}\|$ whose width and height $[E_n(v)|v]_A A$ are both $O(n|A|)$.

**Lemma 64.** Let $A_n$ be an atomic enumeration, let $1 \le j \le n$ and let $v$ be a variable. Then there exists a KSubG$^-$ derivation

$$E_n(v) \quad \|\mathbf{a}\tilde{\mathbf{a}}_j \quad [E_{n\setminus j}(v)]^{l_j} \mathbf{a}_j \quad [E_{n\setminus j}(v)]^{r_j}$$

whose width and height are both $O(n)$.

### E. Phase III: Guarded substitutions

Lemmas 63 and 64 above show that the formula $\langle z_h \lor \eta_h \mu_h A_h | y \rangle E_n(y)$ can be transformed into one with free variables $x_j^{l_j}, x_j^{r_j}, \tilde{x}_j^{l_j}, \tilde{x}_j^{r_j}$ for each $j \in \{1, \dots, n\}$; that is, a formula to which the guarded substitutions $\nu_1, \dots, \nu_n$ can be applied. In Lemma 66 we show that indeed by applying these guarded substitutions we can obtain a formula whose interpretation is the conclusion of the given sFrege<sub>01</sub> proof.

**Definition 65.** Let $V$ be a set of variables and let $\eta = [C_j|v_j]_V$ be an elementary substitution. The equivalence relation on $V$ given by $\eta v = \eta v'$ induces a partition on $V$, and for any $W \subseteq U \cup V^R$, we write $\eta^{-1}W$ for the set $\{v \in V \mid \eta v \in W\}$.

**Lemma 66.** For each $j \in \{1, \dots, n\}$, $\mu_h$ as given in Construction 54, and $v \in \eta_h^{-1}\{x_j, \tilde{x}_j\}$, there exists a derivation

$$\nu_n \dots \nu_1 \eta_h \mu_h (([E_{n \setminus j}(v)]^{l_j} \mathbf{a}_j [E_{n \setminus j}(v)]^{r_j}) \quad \Theta(v) \quad [0|x_j, 1|\tilde{x}_j] \eta_h \mu_h E_{n \setminus j}(v) \mathbf{a}_j [1|x_j, 0|\tilde{x}_j] \eta_h \mu_h E_{n \setminus j}(v))$$

whose height and width are each $O(n)$ and whose only vertical composition is by expansion.

Furthermore, if $\eta_h v = x_j$ then $[\mathrm{cn} \Theta(v)] = a_j$ and if $\eta_h = \tilde{x}_j$ then $[\mathrm{cn} \Theta(v)] = \tilde{a}_j$.

### F. Putting everything together

We can now combine phases I, II, and III to prove our main result. The full construction is shown in Figure 4. When we write an actual substitution $[\Xi|v]_{\eta_h^{-1}\{x_j, \tilde{x}_j\}}$, we understand this to be indexed over $j \in \{1, \dots, n\}$, so that this abbreviates the substitution $[\Xi|v]_{\eta_h^{-1}\{x_1, \tilde{x}_1\}} \dots [\Xi|v]_{\eta_h^{-1}\{x_n, \tilde{x}_n\}}$.

**Theorem 67.** KSubG$^-$ p-simulates sFrege<sub>01</sub>.

Now Theorem 43 follows immediately.

## VII. WHAT ARE GUARDED SUBSTITUTIONS?

To conclude this paper, we turn to a more speculative discussion of what guarded substitutions really are, and what we might want to do with them in the future. Here, we used the concept of guarded substitution only in very restricted way: we only discussed propositional logic, and we only allowed the units 0 and 1 to be substituted. However, the notion of guarded substitution has a much larger potential. To illustrate this, we give an informal example of how guarded substitutions could be used for compression purposes in a familiar proof.

We take the well-known [24] proof of Pythagoras' theorem using similar triangles, which, semi-formally, we can represent concisely in a first-order proof with guarded substitutions.

The proof begins by establishing that ACP and BCP are congruent to the triangle ABC, and hence shows that $|AB|^2 = |AC|^2 + |BC|^2$. These two proofs of congruency are similar but not identical, differing only in that A and B are transposed.

This can give rise to a superposition: a derivation $\Theta$ with free variables $x$ and $y$ whose conclusion is that triangles $xCP$ and $xyC$ are congruent. Applying a substitution $[A|x, B|y]$ results in a proof that triangles ACP and ABC are congruent, and so the guarded substitutions in the proof $\langle A|x, B|y \rangle^1 \langle B|x, A|y \rangle^2 (\Theta|z)(z^1 \land z^2)$ can be applied in order to recover the conclusion that both the triangles ACP and BCP are congruent to the triangle ABC, and the proof of Pythagoras' theorem can proceed as normal from there.

This proof offers us a glimpse of how guarded substitutions might lead the way towards a proof system that offers both proof compression while still retaining a notion of analyticity; and not only free composition of derivations by connective, but free substitution of derivations too [18]. Subatomic proof systems—where strict linearity allows us to restrict all duplication to expansion of substitutions rather than inference rules—offer a sterile laboratory for developing these ideas, but we expect that these concepts can, with care, be translated into familiar proof systems and eventually programming languages, while maintaining in some form the proof theoretic properties established in this paper.

<figure><img src="image_2.png" /></figure>
<figure><img src="image_3.png" /><figcaption>Fig. 4. A KSubG<sup>-</sup> proof which p-simulates the sFrege<sub>01</sub> proof Φ. Here $\vec{\nu}$, $\vec{\sigma}$, and $\vec{\tau}$ abbreviate $\nu_n...\nu_1$, $\sigma_h...\sigma_1$, and $\tau_1...\tau_h$ respectively.</figcaption></figure>

REFERENCES

[1] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy, "Explicit substitutions," *J. of Functional Programming*, vol. 1, no. 4, pp. 375-416, 1991.

[2] A. Aler Tubella, "A study of normalisation through subatomic logic," Ph.D. dissertation, University of Bath, 2017. [Online]. Available: https://people.bath.ac.uk/ag248/aaat/phd.pdf

[3] A. Aler Tubella and A. Guglielmi, "Subatomic proof systems: Splittable systems," *ACM Transactions on Computational Logic*, vol. 19, no. 1, pp. 5:1-33, 2018. [Online]. Available: https://arxiv.org/pdf/1703.10258.pdf

[4] C. Barrett and A. Guglielmi, "A subatomic proof system for decision trees," *ACM Transactions on Computational Logic*, vol. 23, no. 4, pp. 26:1-25, 2022. [Online]. Available: https://arxiv.org/pdf/2105.01382.pdf

[5] V. Barrett, "A strictly linear proof system for propositional classical logic," Ph.D. dissertation, University of Bath, 2024. [Online]. Available: https://toriebarrett.github.io/assets/Papers/Thesis.pdf

[6] V. Barrett, A. Guglielmi, and B. Ralph, "A strictly linear subatomic proof system," in *CSL 2025 - 33rd EACSL Annual Conference on Computer Science Logic*, Amsterdam, Netherlands, Feb. 2025. [Online]. Available: https://inria.hal.science/hal-04845619

[7] G. Boolos, "Don't eliminate cut," *Journal of Philosophical Logic*, vol. 13, pp. 373-378, 1984.

[8] K. Brünnler and A. F. Tiu, "A local system for classical logic," in *LPAR 2001*, ser. LNAI, R. Nieuwenhuis and A. Voronkov, Eds., vol. 2250. Springer, 2001, pp. 347-361.

[9] P. Bruscoli and A. Guglielmi, "On the proof complexity of deep inference," *ACM Transactions on Computational Logic*, vol. 10, no. 2, pp. 14:1-34, 2009. [Online]. Available: https://people.bath.ac.uk/ag248/p/PrComplDI.pdf

[10] P. Bruscoli, A. Guglielmi, T. Gundersen, and M. Parigot, "A quasipolynomial normalisation in deep inference via atomic flows and threshold formulae," *Logical Methods in Computer Science*, vol. 12, no. (1:5), pp. 1-30, 2016.

[11] K. Brünnler, *Deep Inference and Symmetry in Classical Proofs*. Berlin: Logos Verlag, 2004. [Online]. Available: https://people.bath.ac.uk/ag248/kai/phd.pdf

[12] S. R. Buss, "Some remarks on lengths of propositional proofs," *Archive for Mathematical Logic*, vol. 34, no. 6, pp. 377-394, 1995.

[13] S. A. Cook and R. A. Reckhow, "The relative efficiency of propositional proof systems," *The journal of symbolic logic*, vol. 44, no. 1, pp. 36-50, 1979.

[14] A. Das, "On the pigeonhole and related principles in deep inference and monotone systems," in *Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, T. Henzinger and D. Miller, Eds. ACM, 2014, pp. 36:1-10. [Online]. Available: http://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf

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

[16] —, "Untersuchungen über das logische Schließen. II." *Mathematische Zeitschrift*, vol. 39, pp. 405-431, 1935.

[17] A. Guglielmi, "Subatomic logic," November 2002, note.

[18] —, "Formalism B," 2004. [Online]. Available: https://people.bath.ac.uk/ag248/p/AG13.pdf

[19] A. Guglielmi, T. Gundersen, and M. Parigot, "A proof calculus which reduces syntactic bureaucracy," in *21st International Conference on Rewriting Techniques and Applications (RTA)*, ser. Leibniz International Proceedings in Informatics (LIPIcs), C. Lynch, Ed., vol. 6. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2010, pp. 135-150. [Online]. Available: http://drops.dagstuhl.de/opus/volltexte/2010/2649

[20] A. Guglielmi and L. Straßburger, "Non-commutativity and MELL in the calculus of structures," in *Computer Science Logic, CSL 2001*, ser. LNCS, L. Fribourg, Ed., vol. 2142. Springer-Verlag, 2001, pp. 54-68.

[21] E. Jeřábek, "Proof complexity of the cut-free calculus of structures," *Journal of Logic and Computation*, vol. 19, no. 2, pp. 323-339, 2009.

[22] J. Krajíček and P. Pudlák, "Propositional proof systems, the consistency
of first order theories and the complexity of computations.” *The Journal of Symbolic Logic*, vol. 54, no. 3, pp. 1063–1079, 1989.

[23] F. Lamarche, “Exploring the gap between linear and classical logic,” *Theory and Applications of Categories*, vol. 18, no. 18, pp. 473–535, 2007.

[24] E. Maor, *The Pythagorean theorem: a 4,000-year history*. Princeton University Press, 2019, vol. 65.

[25] N. Novakovic and L. Straßburger, “On the power of substitution in the calculus of structures,” *ACM Trans. Comput. Log.*, vol. 16, no. 3, p. 19, 2015.

[26] B. Ralph, “Modular normalisation of classical proofs,” Ph.D. dissertation, University of Bath, 2019. [Online]. Available: https://people.bath.ac.uk/ag248/br/phd.pdf

[27] L. Straßburger, “Extension without cut,” *Annals of Pure and Applied Logic*, vol. 163, no. 12, pp. 1995–2007, 2012.

[28] A. S. Troelstra and H. Schwichtenberg, *Basic Proof Theory*, 2nd ed. Cambridge University Press, 2000.

[29] G. S. Tseitin, “On the complexity of derivation in propositional calculus,” *Zapiski Nauchnykh Seminarov LOMI*, vol. 8, pp. 234–259, 1968.

# APPENDIX

## A. Proofs and definitions for Section II

**Definition 68.** We inductively define the four maps **premise** and **conclusion**, pr, cn: $D \to \mathcal{F}$, and **width** and **height**, w, h: $D \to \mathbb{N}$ as follows:

* If $\Phi \in \mathcal{F}$, then $\mathrm{pr}\,\Phi = \mathrm{cn}\,\Phi = \Phi$ and $w\,\Phi = |\Phi|$ and $h\,\Phi = 0$

* If $\Phi = \Psi \circled{\circ} \Theta$ for some $\circled{\circ} \in A \cup C$, then

$$ \mathrm{pr}\,\Phi = \mathrm{pr}\,\Psi \circled{\circ} \mathrm{pr}\,\Theta \quad \mathrm{w}\,\Phi = \mathrm{w}\,\Psi + \mathrm{w}\,\Theta $$

$$ \mathrm{cn}\,\Phi = \mathrm{cn}\,\Psi \circled{\circ} \mathrm{cn}\,\Theta \quad \mathrm{h}\,\Phi = \max(\mathrm{h}\,\Psi, \mathrm{h}\,\Theta) $$

* If $\Phi = \langle\Psi|x\rangle\Theta$, then

$$ \mathrm{pr}\,\Phi = \langle\mathrm{pr}\,\Psi|x\rangle\mathrm{pr}\,\Theta \quad \mathrm{w}\,\Phi = \mathrm{w}\,\Psi + \mathrm{w}\,\Theta $$

$$ \mathrm{cn}\,\Phi = \langle\mathrm{cn}\,\Psi|x\rangle\mathrm{cn}\,\Theta \quad \mathrm{h}\,\Phi = \max(\mathrm{h}\,\Psi, \mathrm{h}\,\Theta) $$

* If $\Phi = \langle\Psi|x\rangle^p\Theta$, then

$$ \mathrm{pr}\,\Phi = \langle\mathrm{pr}\,\Psi|x\rangle^p \mathrm{pr}\,\Theta \quad \mathrm{w}\,\Phi = \mathrm{w}\,\Psi + \mathrm{w}\,\Theta $$

$$ \mathrm{cn}\,\Phi = \langle\mathrm{cn}\,\Psi|x\rangle^p \mathrm{cn}\,\Theta \quad \mathrm{h}\,\Phi = \max(\mathrm{h}\,\Psi, \mathrm{h}\,\Theta) $$

* if $\Phi = \boxed{\Psi \atop \Theta}$ or $\Phi = \boxed{\Psi \atop \Theta}$, then

$$ \mathrm{pr}\,\Phi = \mathrm{pr}\,\Psi \quad \mathrm{w}\,\Phi = \max(\mathrm{w}\,\Psi, \mathrm{w}\,\Theta) $$

$$ \mathrm{cn}\,\Phi = \mathrm{cn}\,\Theta \quad \mathrm{h}\,\Phi = \mathrm{h}\,\Psi + \mathrm{h}\,\Theta + 1 $$

We now show some basic properties of composition by expansion, and we annotate the derivations constructed with their height. These are needed for later proofs.

The following lemma is used in Lemmas 21 and 22.

**Lemma 69.** Let A, B, C, D be subatomic formulae with no guarded substitutions, and let y and z be variables which occur freely in none of them. Then there exist invertible derivations

$$ \begin{array}{l@{\qquad}l} \langle A|x \rangle B \circled{\circ} \langle C|x \rangle D & \langle A|y \rangle \langle C|z \rangle [y \circled{\circ} z|x] B \\ \|^{\|} & \|^{\|} \\ \langle A|y \rangle \langle C|z \rangle ([y|x] B \circled{\circ} [z|x] D) & \langle A \circled{\circ} C|x \rangle B \end{array} $$

*Proof.* We note that $D = [x|z][z|x]D$ and $B = [x|y][y|x]B$, and we build:

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

for the derivation on the left and

<figure><img src="image_5.png" /></figure>
for the derivation on the right.

The following lemma is used $h$ many times in the derivation $\Omega$ in Figure 4 after the first phase, in order to move the explicit substitutions $\tau_1, \dots, \tau_h$ out of the way.

**Lemma 70.** Let $C, D, A, E$ be subatomic formulae with no guarded substitutions, and let $z$ be a variable which occurs freely in neither $A$ nor $E$. Then there exists an invertible derivation

$$ \begin{gathered} \langle\langle C|z\rangle D \otimes A|y\rangle E \\ \|^{4} \\ \langle C|z\rangle \langle D \otimes A|y\rangle E \end{gathered} $$

*Proof.* We note that $A = [C|z]A$ and $E = [C|z]E$, and we build:

$$ \left\{ \left. \begin{array}{c} \langle C|z\rangle D \otimes \underbrace{A}_{\substack{\sim \\ \langle C|z\rangle A}} \\ \langle C|z\rangle D \otimes A \end{array} \right| y \left. \begin{array}{c} \underbrace{E}_{\substack{\sim \\ \langle C|z\rangle E}} \\ \langle C|z\rangle \end{array} \right\} $$

**Lemma 21.** Let $A$ be an open formula with $\underline{A} = \{x_1, \dots, x_n\}$. Then for all $\otimes \in \mathcal{A} \cup C$ and $B_1, C_1, \dots, B_n, C_n \in \mathcal{F}$, there exist derivations

$$ \begin{array}{l@{\qquad}l} [B_i | x_i]_{\underline{A}} A \check{\otimes} [C_i | x_i]_{\underline{A}} A & [B_i \hat{\otimes} C_i | x_i]_{\underline{A}} A \\ & \|^{\check{\otimes}, \circ, \check{\otimes}} \\ [B_i \check{\otimes} C_i | x_i]_{\underline{A}} A & \|^{\hat{\otimes}, \circ, \hat{\otimes}} \\ & [B_i | x_i]_{\underline{A}} A \hat{\otimes} [C_i | x_i]_{\underline{A}} A \end{array} $$

The height of each of these derivations is $O(|A|)$ and their width is $O(\sum(|B_i| + |C_i|))$.

*Proof.* We prove the derivation on the left by structural induction on $A$.

If $A$ is a variable then the derivation is a formula.

If $A = D \odot E$ for some $\odot \in C \cup A$ then we build

$$ \frac{\left( \begin{array}{c} \langle [B_i | x_i]_{\underline{D}} D \odot [B_i | x_i]_{\underline{E}} E \rangle \check{\otimes} \langle [C_i | x_i]_{\underline{D}} D \odot [C_i | x_i]_{\underline{E}} E \rangle \\ \left[ \begin{array}{c} [B_i | x_i]_{\underline{D}} D \check{\otimes} [C_i | x_i]_{\underline{D}} D \\ \mathop{\mathrm{IH}}\limits \|^{\check{\otimes}, \circ, \check{\otimes}} \\ [B_i \check{\otimes} C_i | x_i]_{\underline{D}} D \end{array} \right] \end{array} \right) \check{\otimes} \left( \begin{array}{c} [B_i | x_i]_{\underline{E}} E \check{\otimes} [C_i | x_i]_{\underline{E}} E \\ \mathop{\mathrm{IH}}\limits \|^{\check{\otimes}, \circ, \check{\otimes}} \\ [B_i \check{\otimes} C_i | x_i]_{\underline{E}} E \end{array} \right)}{\frac{1}{\mathop{\mathrm{cut}}\limits}} $$

If $A = \langle D|y\rangle E$ then for variables $y_1, y_2$ not appearing in $E$ we build the derivation in Figure 5, and the case $A = \langle D|y\rangle^p E$ is similar and simpler.

The derivation on the right can be constructed analogously.

**Lemma 22.** Let $A$ be an open formula with $\underline{A} = \{x_1, \dots, x_n\}$. Then for all $\otimes \in \mathcal{A} \cup C$ and $B_1, C_1, \dots, B_n, C_n \in \mathcal{F}$, there exist derivations

$$ \begin{array}{l@{\qquad}l} [B_i \otimes C_i | x_i]_{\underline{A}} \hat{A} & [B_i | x_i]_{\underline{A}} A \otimes [C_i | x_i]_{\underline{A}} \bar{A} \\ & \|^{\check{\otimes}, \circ, \check{\otimes}} \\ [B_i | x_i]_{\underline{A}} A \otimes [C_i | x_i]_{\underline{A}} \bar{A} & [B_i \otimes C_i | x_i]_{\underline{A}} \check{A} \\ & \|^{\hat{\otimes}, \circ, \hat{\otimes}} \\ & [B_i | x_i]_{\underline{A}} A \otimes [C_i | x_i]_{\underline{A}} \check{A} \end{array} $$

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

The height of each of these derivations is $O(|A|)$ and their width is $O(\sum(|B_i| + |C_i|))$.

*Proof.* We prove the derivation on the left by structural induction on $A$.

If $A$ is a variable then the derivation is a formula.

If $A = D \odot E$ for some $\odot \in C \cup A$ then we can assume without loss of generality that $\hat{\odot} = \odot$ and $\check{\odot} = \hat{\odot}$ and we build:

$$ \frac{\left( \begin{array}{c|c} \left[ \begin{array}{c} B_i \otimes C_i | x_i \end{array} \right]_{\underline{D}} \hat{D} & \left[ \begin{array}{c} B_i \otimes C_i | x_i \end{array} \right]_{\underline{E}} \hat{E} \\ \mathop{\mathrm{IH}}\limits \|^{\check{\otimes}, \circ, \check{\otimes}} & \mathop{\mathrm{IH}}\limits \|^{\check{\otimes}, \circ, \check{\otimes}} \\ \left[ B_i | x_i \right]_{\underline{D}} D \otimes \left[ C_i | x_i \right]_{\underline{D}} \bar{D} & \left[ B_i | x_i \right]_{\underline{E}} E \otimes \left[ C_i | x_i \right]_{\underline{E}} \bar{E} \end{array} \right) \check{\otimes} \frac{\left( \left[ B_i | x_i \right]_{\underline{D}} D \odot \left[ B_i | x_i \right]_{\underline{E}} E \right) \otimes \left( \left[ C_i | x_i \right]_{\underline{D}} \bar{D} \hat{\odot} \left[ C_i | x_i \right]_{\underline{E}} \bar{E} \right)}{\mathop{\mathrm{cut}}\limits} $$

If $A = \langle D|y\rangle E$ then for variables $y_1, y_2$ not appearing in $E$ we build the derivation in Figure 6, and the case $A = \langle D|y\rangle^p E$ is similar and simpler.

The derivation on the right can be constructed analogously.

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

## B. Proofs for Section III

**Definition 71.** The proof system SKS [11], [19] consists of the following inference rules:

* The structural rules:

$$ \text{atomic} \quad \left\{ \begin{array}{l} \begin{array}{l} \text{ai}\downarrow \\ \text{identity} \end{array} \qquad \begin{array}{l} \frac{1}{a \lor \bar{a}} \\ \text{ac}\downarrow \end{array} \qquad \begin{array}{l} \frac{a \lor a}{a} \\ \text{contraction} \end{array} \qquad \begin{array}{l} \frac{0}{a} \\ \text{weakening} \end{array} \\ \\ \begin{array}{l} \text{ai}\uparrow \\ \text{cut} \end{array} \qquad \begin{array}{l} \frac{a \land \bar{a}}{0} \\ \text{ac}\uparrow \end{array} \qquad \begin{array}{l} \frac{a}{a \land a} \\ \text{cocontraction} \end{array} \qquad \begin{array}{l} \frac{a}{a \land 1} \\ \text{coweakening} \end{array} \end{array} \right\} $$

* The logical rules:

$$ \begin{array}{c} \mathop{\mathrm{switch}}\limits \\ \mathop{\mathrm{medial}}\limits \end{array} \frac{A \land (B \lor C)}{(A \land B) \lor C} \quad \frac{(A \land B) \lor (C \land D)}{(A \lor C) \land (B \lor D)} $$

* An equivalence on formulae, defined to be the minimal equivalence relation generated by the following:

$$ A \land 1 \equiv A \qquad A \land B \equiv B \land A $$

$$ A \lor 0 \equiv A \qquad A \lor B \equiv B \lor A $$

$$ 1 \lor 1 \equiv 1 \qquad A \land (B \land C) \equiv (A \land B) \land C $$

$$ 0 \land 0 \equiv 0 \qquad A \lor (B \lor C) \equiv (A \lor B) \lor C $$

We write $\equiv \frac{A}{B}$ whenever $B$ can be reached from $A$ via this equivalence relation.

* We also include the mix rule:

$$ \text{mix} \frac{0}{1} $$

to enable a straightforward definition of the interpretation function, but note that it is easily derivable from the other rules.
$$
\begin{array}{l}
\left\langle [B_i|x_i]_D y \right\rangle [B_i|x_i]_{\mathcal{E}\setminus\{y\}} E \overset{\sim}{\left\langle} [C_i|x_i]_D y \right\rangle [C_i|x_i]_{\mathcal{E}\setminus\{y\}} E \\
\text{Lemma 69} \left\| \right\|_7 \\
\left\langle [B_i|x_i]_D y_1 \right\rangle \left\langle [C_i|x_i]_D y_2 \right\rangle \left[ \begin{array}{l} y_1 | y \quad [B_i|x_i]_{\mathcal{E}\setminus y} E \overset{\sim}{\left\langle} [y_2|y] [C_i|x_i]_{\mathcal{E}\setminus y} E \\ \text{IH} \left\| \right\| \overset{\sim}{\left\langle} \circ, \circ \end{array} \right. \\
\left. \begin{array}{l} y_1 \overset{\sim}{\left\langle} y_2 | y \quad [B_i \overset{\sim}{\left\langle} C_i | x_i]_{\mathcal{E}\setminus y} E \\ \left\| \right\| \end{array} \right. \end{array}
$$

$$
\text{Lemma 69} \left\| \right\|_4
\left\{
\begin{array}{@{}l@{}}
\left\langle
  \begin{array}{@{}c@{}}
    [B_i | x_i]_D \check{\otimes} [C_i | x_i]_D D \\
    \text{IH} \left\| \right\| \check{\otimes} \circ, \check{\otimes} \\
    [B_i \check{\otimes} C_i | x_i]_D D
  \end{array}
\right| y \right\rangle [B_i \check{\otimes} C_i | x_i]_{\underline{E} \setminus y} E
\end{array}
\right\}
$$

<caption>Fig. 5. Explicit substitution case for the proof of Lemma 21</caption>

$$
\left\{
\begin{array}{@{}l@{}}
  \left\langle
    \begin{array}{@{}c@{}}
      [B_i \otimes C_i | x_i]_D \hat{D} \\
      \text{IH} \left\| \right\| \check{\otimes} \circ, \check{\otimes} \\
      [B_i | x_i]_D D \otimes [C_i | x_i]_D \bar{D}
    \end{array}
  \right| y \right\rangle [B_i \otimes C_i | x_i]_{\underline{E} \setminus y} \hat{E} \\
  \text{Lemma 69} \left\| \right\|_4 \\
  \left\langle
    \begin{array}{@{}c@{}}
      [B_i | x_i]_D D | y_1 \rangle \langle [C_i | x_i]_D \bar{D} | y_2 \rangle \\
      \text{IH} \left\| \right\| \check{\otimes} \circ, \check{\otimes} \\
      [y_1 | y] [B_i | x_i]_{\underline{E} \setminus y} E \otimes [y_2 | y] [C_i | x_i]_{\underline{E} \setminus y} \bar{E}
    \end{array}
  \right\rangle \\
  \text{Lemma 69} \left\| \right\|_7
\end{array}
\right.
$$

$$
\left\langle [B_i | x_i]_D | y \right\rangle [B_i | x_i]_{\mathcal{E} \setminus \{y\}} E \otimes \left\langle [C_i | x_i]_D \bar{D} | y \right\rangle [C_i | x_i]_{\mathcal{E} \setminus \{y\}} \bar{E}
$$

<caption>Fig. 6. Explicit substitution case for the proof of Lemma 22</caption>

A *proof* is a derivation in SKS with premise 1. And a standard formula A is *provable* if there is a proof with conclusion A.

**Theorem 72.** The system SKS is sound and complete for classical propositional logic, i.e., a formula is provable in SKS iff it is a tautology. [8], [11], [19]

**Theorem 73.** The cut is admissible from SKS. More precisely, if a formula A is provable in SKS, then it is also provable without using the rules $ai\uparrow$, $ac\uparrow$, $aw\uparrow$. [8], [11]

**Proposition 26.** If $\Phi$ is a subatomic derivation in KSubG and $[[\Phi]]$ is defined, then $[[\Phi]]$ is a standard derivation in SKS.

*Proof.* It suffices to observe that if $A$ is an instance of an inference rule in KSubG, and both $[[A]]$ and $[[B]]$ are defined, then $[[A]]$ is an instance of an inference rule in SKS. $\square$

**Proposition 29.** Let A be an open formula with free variables $\{v_1, \dots, v_n\}$ and let $B_1, \dots, B_n$ be formulae. If $[[B_1]] = \dots = [[B_n]] = U \in U$ then $[[\langle B_i | v_i \rangle_A A]] = U$.

*Proof.* By induction on the structure of A.

$$
\text{If } A \in \mathcal{V}^\mathcal{R} \text{ then } [[\langle B_1 | v_1 \rangle A]] = [[B_1]] = U.
$$

If $A = C \otimes D$ then it follows from the definition of the interpretation map that $[[\langle B_i | v_i \rangle_A C | x] \langle B_i | v_i \rangle_{\underline{D} \setminus \{x\}} D]] = [[\langle B_i | v_i \rangle_C C \otimes \langle B_i | v_i \rangle_{\underline{D}} D]]$. By induction, we can assume that

$$
\left\langle \left\langle B_i | v_i \right\rangle_C C \right\rangle = U \text{ and } \left\langle \left\langle B_i | v_i \right\rangle_D D \right\rangle = U, \text{ so it follows that} \\
\left\langle B_i | v_i \right\rangle_A A \right\rangle = U.
$$

If $A = \langle C|x \rangle D$ then it follows from the definition of the interpretation map that $[[\langle B_i | v_i \rangle_A A]] = [[\langle B_i | v_i \rangle_C C | x \rangle \langle B_i | v_i \rangle_{\underline{D} \setminus \{x\}} D]]$. By induction, we can assume that $[[\langle B_i | v_i \rangle_C C]] = U$, and so it follows by induction that $[[\langle \langle B_i | v_i \rangle_C C | x \rangle \langle B_i | v_i \rangle_{\underline{D} \setminus \{x\}} D \rangle]] = U$. $\square$

**Theorem 31.** Let A be a standard formula. The following are equivalent:

1) A is a Boolean tautology.

2) A is provable in SKS.

3) A is provable in KSubG.

4) A is provable in KSubG without the algebraic rules.

*Proof.* 1) $\Leftrightarrow$ 2) follows from Theorem 72. For 2) $\Rightarrow$ 3) observe that every instance of a rule of SKS can be seen as the interpretation of an instance of a subatomic rule. The cases of $ac\downarrow$ and $ac\uparrow$ and $ai\uparrow$ were given in the introduction. The other cases are similar. The result has also been shown in [3]. 3) $\Rightarrow$ 2) also has been shown in [3]. 3) $\Rightarrow$ 4) is shown in the same way as 2) $\Rightarrow$ 3) because the interpretation of every instance of an algebraic rule is (if defined) also the interpretation of a subatomic rule instance. Finally, 4) $\Rightarrow$ 3) is trivial. $\square$
### C. Proofs for Section VI

**Proposition 52.** Let $A_n$ be an atomic enumeration with variable enumeration $V_n = \{x_1, \tilde{x}_1, \dots, x_n, \tilde{x}_n\}$ and let $P$ be a standard formula with factorised translation $(\eta, A)$. Then
$$ \llbracket [0 \ a_j \ 1|x_j, 1 \ a_j \ 0|\tilde{x}_j]_{1\le j\le n} \eta A \rrbracket = P. $$

*Proof.* This follows immediate from the definition. □

Before we continue, we first show the remaining cases for Construction 54:

If $P_i$ is the axiom $F_2$, Then $A_i$ is of the form $(X \wedge (Y \wedge Z')) \vee ((X' \wedge Y') \vee (X'' \vee Z))$ where $\eta_i X = \eta_i X'$ and both are pseudo-dual to $\eta_i X''$, $\eta_i Y$ and $\eta_i Y'$ are pseudo-dual, and $\eta_i Z$ and $\eta_i Z'$ are pseudo-dual. For a variable $v \in \underline{X}$, we denote by $v'$ and $v''$ the variables in $\underline{X}'$ and $\underline{X}''$ respectively appearing in the corresponding position, and similarly for $Y$ and $Z$. With use of Lemmas 21 and 22 we construct the derivation $\Psi_i$ and formula $B_i$ in Figure 7. We obtain the substitutions $\tau_i = \langle 0|z_i \rangle$, $\rho_i = \eta_i$, $\mu_i = [v \vee v|v]_{\underline{X}''}$, and $\sigma_i = \epsilon$.

In the case of $F_3$, we have that $A_i$ is of the form $(X' \wedge Y) \vee (Y' \vee X)$, where $\eta_i X'$ and $\eta_i X$ are pseudo-dual formulae, and so are $\eta_i Y$ and $\eta_i Y'$; for $v \in \underline{X}$, we denote by $v'$ the variable in $\underline{X}'$ appearing in the corresponding position, and similarly for $Y$. With use of Lemma 22 we construct:

$$ \Psi_i = \left[ \begin{array}{c|c} \begin{array}{c} 0 \\ \langle 0|z_i \rangle z_i \end{array} & \vee \eta_i \\ \hline \begin{array}{c} \underbrace{[v' \vee v|v]_{\underline{X}}}_{\sim \tilde{x}, \vee \tilde{x}} \hat{X} \\ \|_{\tilde{x}, \vee \tilde{x}} \wedge X' \vee X \end{array} & \wedge \begin{array}{c} \underbrace{[v \vee v'|v]_{\underline{Y}}}_{\sim \tilde{x}, \vee \tilde{x}} \hat{Y} \\ \|_{\tilde{x}, \vee \tilde{x}} Y \vee Y' \end{array} \\ \hline \begin{array}{c} (X' \wedge Y) \vee \underbrace{\overline{X \vee Y'}}_{\sim \text{com}} \\ \| Y' \vee X \end{array} & \vee \eta_i A_i \end{array} \right] $$

and we obtain the substitutions $\tau_i = \langle 0|z_i \rangle$, $\rho_i = \eta_i$, $\mu_i = \epsilon$ and $\sigma_i = \epsilon$, and the formula $B_i = 0 \vee \eta_i ([v' \vee v|v]_{\underline{X}} \hat{X} \wedge [v \vee v'|v]_{\underline{Y}} \hat{Y})$.

In the case of $F_4$, then $\eta_i A_i = 1$. We construct

$$ \Psi_i = \left[ \begin{array}{c|c} 0 & \vee \eta_i A_i \\ \hline \langle 0|z_i \rangle z_i \end{array} \right] $$

and we obtain the substitutions $\tau_i = \langle 0|z_i \rangle$, $\rho_i = \eta_i$, $\mu_i = \epsilon$ and $\sigma_i = \epsilon$, and the formula $B_i = 0 \vee 1$.

The following lemma shows how guarded substitutions can be applied to non-flat formulae; we will use it in Lemmas 57 and 66 to show how the guarded substitutions $\vec{\sigma}$ and $\vec{\nu}$ are applied in Figure 4 in the proof of Theorem 43.

**Lemma 55.** For each $i \in \{1, \dots, h\}$, $[B_1|y_1] \dots [B_i|y_i] y_i$ is tautological with respect to $V_\Phi$.

*Proof.* By induction on the structure of $\Phi$.

If $P_i$ is obtained from an axiom $F_1$ then $B_i$ is a disjunction $0 \vee \eta_i ([v \wedge 0|v]_{\underline{Y}} \vee [v' \vee v|v]_{\underline{X}} \hat{X})$, where for each $v \in \underline{X} \cup \underline{Y}$, $\eta_i v$ and $\eta_i v'$ are pseudo-dual variables with respect to $V_\Phi$. If $P_i$ is obtained from an axiom $F_2$ or $F_3$ then $B_i$ is composed of

disjunctions of variables which are pseudo-dual with respect to $V_\Phi$ (in disjunction with 0). If $P_i$ is obtained from an axiom $F_4$ then $B_i = 0 \vee 1$. In each case (except for $F_4$, which is immediate), the interpretation of the formula is determined by disjunctions of pseudo-dual variables, and any substitution which dualises pseudo-dual variables will verify it. Therefore, $B_i$ is tautological with respect to $V_\Phi$.

If $P_i$ is obtained from modus ponens on $P_k$ and $P_l = \bar{P}_k \vee P_i$ then $B_i = y_k \wedge y_l$. We assume that $[B_1|y_1] \dots [B_k|y_k] y_k$ and $[B_1|y_1] \dots [B_l|y_l] y_l$ are tautological with respect to $V_\Phi$, so $[B_1|y_1] \dots [y_k \wedge y_l|y_i] y_i$ is tautological with respect to $V_\Phi$.

If $P_i$ is obtained from substitution on $P_k$ then $B_i = y_k^i$. We assume that $[B_1|y_1] \dots [B_k|y_k] y_k$ is tautological with respect to $V_\Phi$. It follows immediately that $[B_1|y_1] \dots [y_k^i|y_i] y_i$ is tautological with respect to $V_\Phi$. □

**Lemma 56.** For each $i \in \{1, \dots, h\}$, $\tau_1 \dots \tau_i z_i$ is contradictory with respect to $V_\Phi$.

*Proof.* By induction on the structure of $\Phi$.

If $P_i$ is an axiom then $\tau_i = \langle 0|z_i \rangle$, so $\tau_1 \dots \tau_i z_i$ is contradictory with respect to $V_\Phi$.

If $P_i$ is obtained from modus ponens on $P_k$ and $P_l = \bar{P}_k \vee P_i$ then $\tau_i = (\langle z_k \vee z_l \rangle \vee [\rho_k \mu_k v \wedge \rho_l \mu_l v'|v]_{\underline{A_k}} \tilde{A}_k |z_i \rangle)$, where $\rho_k v$ and $\rho_l v'$ are pseudo-dual variables. We assume that $\tau_1 \dots \tau_k z_k$ and $\tau_1 \dots \tau_l z_l$ are contradictory with respect to $V_\Phi$. By construction, $\rho_k \mu_k v \wedge \rho_l \mu_l v'$ is contradictory with respect to $V_\Phi$ for each $v \in \underline{A_k}$. Therefore $\tau_1 \dots \tau_i z_i$ is contradictory with respect to $V_\Phi$.

If $P_i$ is obtained from substitution on $P_k$ then $\tau_i$ is $\langle z_k^i|z_i \rangle$. We assume that $\tau_1 \dots \tau_k z_k$ is contradictory with respect to $V_\Phi$. It follows immediately that $\tau_1 \dots \tau_i z_i$ is contradictory with respect to $V_\Phi$. □

**Lemma 57.** For each $i$ and each variable $v \in \underline{A_i}$, there exists a range $R \subseteq \{1, \dots, i\}$ and a derivation

$$ \sigma_h \dots \sigma_1 \rho_i \mu_i v \\ \| \\ \eta_i \mu_i v^R $$

whose width is $O(hw)$, whose only vertical composition is by expansion and whose height is $O(h)$.

*Proof.* By induction on the structure of $\Phi$.

If $P_i$ is an axiom then by construction, $\rho_i = \eta_i$, and the range of each variable in $\rho_i \mu_i A_i$ is empty, so $R = \emptyset$. We construct the derivation by vacuously applying each guarded substitution.

If $P_i$ is obtained from modus ponens on $P_k$ and $P_l = \bar{P}_k \vee P_i$ then for each $v$ occurring in $A_i$ there is $v'$ occurring in $A_l$ such that $\mu_l v' = \mu_i v$, $\rho_l = \rho_i$, and $\eta_l = \eta_i$. By induction, we can construct

$$ \sigma_h \dots \sigma_{l+1} \left[ \begin{array}{c} \sigma_l \dots \sigma_1 \rho_i \mu_i v \\ \| \sigma_l \dots \sigma_1 \rho_i \mu_i v \\ \| \sigma_l \dots \sigma_1 \rho_i \mu_i v^R \end{array} \right. $$
$$B_i = 0 \lor \eta_i ([v \lor v''|v]_X \hat{X} \land ([v' \lor v''|v]_X \hat{X} \land ([v \lor v'|v]_Y \hat{Y} \land [v' \lor v|v]_Z \hat{Z})))$$

<figure><img src="image_8.png" /><figcaption>Fig. 7. F₂</figcaption></figure>

and we have that $R \subseteq \{1, \dots, l\}$. Therefore, all of the substitutions $\sigma_{l+1}, \dots, \sigma_h$ can be vacuously applied to $\eta_i \mu_i v^R$ in $(i-l)$ many steps.

If $P_i$ is obtained from a substitution $[u_{j_1}|x_{j_1}] \dots [u_{j_m}|x_{j_m}]$ on $P_k$ then

$$\sigma_i = \langle u_{j_1} | x_{j_1}, \bar{u}_{j_1} | \tilde{x}_{j_1} \rangle^i \dots \langle u_{j_m} | x_{j_m}, \bar{u}_{j_m} | \tilde{x}_{j_m} \rangle^i$$

and for each $v$ occurring in $A_i$, there is a corresponding $w$ occurring in $A_k$ such that

$$\mu_i v = \mu_k w$$

$$\rho_i \mu_i v = \rho_k \mu_k w^i$$

$$\eta_i = [u_{j_1} | x_{j_1}, \bar{u}_{j_1} | \tilde{x}_{j_1}] \dots [u_{j_m} | x_{j_m}, \bar{u}_{j_m} | \tilde{x}_{j_m}] \eta_k$$

By induction, there exists a derivation

$$\sigma_k \dots \sigma_1 \rho_k \mu_k w \\ \| O(k) \\ \eta_k \mu_k w^R$$

for some $R \subseteq \{1, \dots, k\}$. By construction, none of the guarded substitutions $\sigma_1, \dots, \sigma_{i-1}, \sigma_{i+1}, \dots, \sigma_h$ have a guard $i$, so it follows that we can construct

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

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

**Lemma 58.** For each $i$, the size of $\Psi_i$ is polynomial in the size of $\Phi$.

*Proof.* We note that the height of $\Phi$ is $h$. Its width, $w$, is given by $\max|P_i|$. The number of (positive and negative) atoms $2n$ is $O(hw)$.

The worst case for the width of a $\Psi_i$ is obtained in the modus ponens and unit substitution cases when there have been many unit substitution steps, so that $\rho_i$ is substituting $O(h)$ many ranges onto each of the $O(w)$ many variables in $A_i$; the width of $\Psi_i$ is then $O(hw)$.

The worst case for the height of a $\Psi_i$ is obtained in the axiom and modus ponens cases: it is $O(w)$. $\square$

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

**Lemma 60.** The size of $\Psi$ is polynomial in the size of $\Phi$: its width is $O(h^2w)$ and its height is $O(hw)$.

*Proof.* The size of $\Psi$ can be calculated as follows:

$$\begin{align*} w \Psi &\le h(\max |\tau_i| + 2 \max |z_i \lor \rho_i \eta_i A_i|) \\ &= hO(w + hw) \\ &= O(h^2w) \\ h \Psi &= hO(\max |\Psi_i|) \\ &= O(hw) \end{align*}$$

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

**Proposition 62.** Let $A_n$ be an atomic enumeration and let $V_n$ be a variable enumeration. Let $A$ be a formula such that $A \subseteq V_n$. If $A$ is a tautology (resp. contradiction) with respect to $V_n$ then $[\nu_n \dots \nu_1 \langle A | y \rangle E_n(y)] = 1$ (resp. 0).
**Proof.** If A is a tautology with respect to $V_n$, then so is $[A]^R$, for $R \in \{l_1, r_1\} \times \dots \times \{l_n, r_n\}$. Also, for each such R, the actual actual substitution obtained by applying $\nu_n \dots \nu_1$ to $[A]^R$ closes the formula and dualises pseudo-dual variables, so $[\nu_n \dots \nu_1 [A]^R] = 1$. Applying all of the explicit substitutions in $\langle A|y \rangle E_n(y)$ results in a formula composed of $2^n$ copies of A, each with a different range from $\{l_1, r_1\} \times \dots \times \{l_n, r_n\}$. It follows that $[\nu_n \dots \nu_1 \langle A|y \rangle E_n(y)] = 1$. The case for a contradictory formula is analogous. □

**Lemma 63.** Let $A_n$ be an atomic enumeration, let $y$ be a variable and let $A$ be a flat open formula. Then there exists $\langle A|y \rangle E_n(y)$ a KSubG$^-$ derivation $\|\circ\tilde{a}\|$ whose width and height $[E_n(v)|v]_A A$ are both $O(n|A|)$.

**Proof.** By induction on $n$.

If $n=1$ then $E_1(y) = \langle y^{l_1} a_1 y^{r_1} |y\rangle y$. By Lemma 21 we can construct

$$ \langle A|y \rangle \langle y^{l_1} a_1 y^{r_1} |y\rangle y \underbrace{\left\{ \begin{array}{c} [A]^l a_1 [A]^r \\ \|\circ\tilde{a}_1 \\ [v^{l_1} a_1 v^{r_1} |v]_A A \end{array} \right\}}_{\|2|A|} \underbrace{\left| y \right\rangle y}_{\|2|A|} \underbrace{[E_1(v)|v]_A A}_{\|2|A|} $$

and the height and width of this derivation are both $O(|A|)$.

If $n=k+1$ then $E_{k+1\setminus 1}(y) = \langle y^{l_2} a_2 y^{r_2} |y\rangle \dots \langle y^{l_{k+1}} a_{k+1} y^{r_{k+1}} |y\rangle y$. By induction and Lemma 21 we can construct

$$ \langle A|y \rangle \langle y^{l_1} a_1 y^{r_1} |y\rangle E_{k+1\setminus 1}(y) \underbrace{\left\{ \begin{array}{c} [A]^l a_1 [A]^r \\ \|\circ\tilde{a}_1 \\ [v^{l_1} a_1 v^{r_1} |v]_A A \end{array} \right\}}_{\|2|A|} \underbrace{\left| y \right\rangle E_{k+1\setminus 1}(y)}_{\|2|A|} \underbrace{\left\{ \begin{array}{c} \langle A|y \rangle E_{k+1\setminus 1}(y) \\ \|H\| \|\circ\tilde{a} \\ [E_{k+1\setminus 1}(v)|v]_A A \end{array} \right\}}_{\|2|A|} \underbrace{[E_{k+1}(v)|v]_A A}_{\|2|A|} $$

The height of the application of Lemma 21 is $O(|A|)$; therefore the height of this derivation is $O(n|A|)$. Its width is given by the $O(|A|)n$ many explicit substitution terms which are factored out. □

**Lemma 64.** Let $A_n$ be an atomic enumeration, let $1 \le j \le n$ and let $v$ be a variable. Then there exists a KSubG$^-$ derivation

$$ E_n(v) \|a\hat{a}_j \underbrace{[E_{n\setminus j}(v)]^{l_j}}_{\|2|A|} a_j \underbrace{[E_{n\setminus j}(v)]^{r_j}}_{\|2|A|} $$

whose width and height are both $O(n)$.

**Proof.** Let

$$ \begin{align*} E_{j-1}(v) &= \langle v^{l_1} a_1 v^{r_1} |v\rangle \dots \langle v^{l_{j-1}} a_{j-1} v^{r_{j-1}} |v\rangle v \\ E' &= \langle v^{l_{j+1}} a_{j+1} v^{r_{j+1}} |v\rangle \dots \langle v^{l_n} a_n v^{r_n} |v\rangle v \end{align*} $$

Then by making use of the construction

$$ \langle A|x \rangle (x^p \circledast x^q) \underbrace{\left[ \begin{array}{c} [A]^p \\ \langle [A]^p |x \rangle x \end{array} \right]}_{\circledast} \underbrace{\left[ \begin{array}{c} [A]^q \\ \langle [A]^q |x \rangle x \end{array} \right]}_{\circledast} $$

to pass the ranges $l_j$ and $r_j$ to the free variables and applying Lemma 21 we construct the following derivation:

$$ \begin{array}{c} E_n(v) \\ \|2j\| \\ \langle [E_{j-1}(v)]^{l_j} a_j [E_{j-1}(v)]^{r_j} |v\rangle E' \\ \underbrace{\langle [E_{j-1}(v)]^{l_j} a_j [E_{j-1}(v)]^{r_j} |v\rangle E'}_{\|2|A|} \end{array} \qquad \text{Lemma 21 } \|a\hat{a}_j \qquad \begin{array}{c} \underbrace{\left[ [E_{j-1}(v)]^{l_j} |v\rangle E' \right]}_{\|2|A|} \\ \underbrace{[E_{n\setminus j}(v)]^{l_j}}_{\|2|A|} a_j \underbrace{\left[ [E_{j-1}(v)]^{r_j} |v\rangle E' \right]}_{\|2|A|} \\ \underbrace{[E_{n\setminus j}(v)]^{r_j}}_{\|2|A|} \end{array} $$

The height of this derivation is dominated by the application of Lemma 21, which has height $O(n)$. □

**Lemma 66.** For each $j \in \{1, \dots, n\}$, $\mu_h$ as given in Construction 54, and $v \in \eta_h^{-1}\{x_j, \tilde{x}_j\}$, there exists a derivation

$$ \nu_n \dots \nu_1 \eta_h \mu_h ( ( [E_{n\setminus j}(v)]^{l_j} a_j [E_{n\setminus j}(v)]^{r_j}) \Theta(v) ) \| [0|x_j, 1|\tilde{x}_j] \eta_h \mu_h E_{n\setminus j}(v) a_j [1|x_j, 0|\tilde{x}_j] \eta_h \mu_h E_{n\setminus j}(v) $$

whose height and width are each $O(n)$ and whose only vertical composition is by expansion.

Furthermore, if $\eta_h v = x_j$ then $\llbracket \mathrm{cn} \Theta(v) \rrbracket = a_j$ and if $\eta_h = \tilde{x}_j$ then $\llbracket \mathrm{cn} \Theta(v) \rrbracket = \bar{a}_j$.

**Proof.** The only free variables in $\eta_h \mu_h [E_{n\setminus j}(v)]^{l_j} a_j [E_{n\setminus j}(v)]^{r_j}$ are either $x_j^{l_1,l_j}, x_j^{l_2,l_j}, x_j^{l_1,r_j}$, and $x_j^{r_1,r_j}$ or $\tilde{x}_j^{l_1,l_j}, \tilde{x}_j^{l_2,l_j}, \tilde{x}_j^{l_1,r_j}$, and $\tilde{x}_j^{r_1,r_j}$. The guarded substitutions $\eta_1, \dots, \eta_{j-1}$ do not apply to the variables $x_j$ or $\tilde{x}_j$, and so they are applied vacuously. The substitution $\nu_j = \langle 0|x_j, 1|\tilde{x}_j \rangle^j \langle 1|x_j, 0|\tilde{x}_j \rangle^j$ can then be applied to $\eta_h \mu_h \underbrace{[E_{n\setminus j}(v)]^{l_j} a_j [E_{n\setminus j}(v)]^{r_j}}_{\|2|A|} \circledast$, resulting in $[0|x_j, 1|\tilde{x}_j] \eta_h \mu_h E_{n\setminus j}(v) a_j [1|x_j, 0|\tilde{x}_j] \eta_h \mu_h E_{n\setminus j}(v)$. This formula has no free variables, so the guarded substitutions $\nu_{j+1}, \dots, \nu_n$ are applied vacuously.

If $\eta_h v = x_j$ then $\llbracket \langle 0|x_j, 1|\tilde{x}_j] \eta_h \mu_h v \rrbracket = 0$, and it is immediate that $\llbracket \langle 0|v \rangle E_{n\setminus j}(v) \rrbracket = 0$. Similarly, we can see that $\llbracket \langle 1|x_j, 0|\tilde{x}_j] \eta_h \mu_h E_{n\setminus j}(v) \rrbracket = 1$; therefore $\llbracket \mathrm{cn} \Theta(v) \rrbracket = \langle 0 a_j 1 \rangle = a_j$. Analogously, if $\eta_h v = \tilde{x}_j$ then $\llbracket \mathrm{cn} \Theta(v) \rrbracket = \langle 0 a_j 1 \rangle = \bar{a}_j$. □

**Theorem 67.** KSubG$^-$ p-simulates sFrege01.
<figure><img src="image_13.png" /></figure>

$$
\begin{align*}
& \langle\langle A|x, B|y\rangle\rangle^1 \langle\langle B|x, A|y\rangle\rangle^2 \left\{ \begin{array}{@{}l@{}} \left. \frac{\angle xCP = \frac{\pi}{2} - \angle yxC = \angle Cyx}{\Delta Cyx \sim \Delta xCP} \right|_z \right\} z^1 \wedge z^2 \\
& \hspace{2em} \llbracket \langle\langle A|x, B|y\rangle\rangle^1 \langle\langle B|x, A|y\rangle\rangle^2 \left[ |xC|^2 = |xy||xP| \right]^1 \wedge \left[ |xC|^2 = |xy||xP| \right]^2 \rrbracket \\
& \hspace{2em} \frac{\left( |AC|^2 = |AB||AP| \right) \wedge \left( |BC|^2 = |BA||BP| \right)}{\frac{|AC|^2 + |BC|^2 = |AB||AP| + |BA||BP|}{|AC|^2 + |BC|^2 = |AB|^2}}
\end{align*}
$$

<caption>Fig. 8. A fragment of a proof of Pythagoras’ Theorem using guarded substitutions</caption>

Proof. Let $\Phi = P_1, \dots, P_h$ be an sFrege<sub>01</sub> proof, with atomic enumeration $A_n$, variable enumeration $V_n$, and factorised translation $(\eta_1, A_1), \dots, (\eta_h, A_h)$.

Let $\Psi$ and its constituent parts be as given in Constructions 54 and 59, and let $\vec{\tau}$, $\vec{\sigma}$, and $\vec{\nu}$ abbreviate $\tau_1 \dots \tau_h$, $\sigma_h \dots \sigma_1$, and $\nu_n \dots \nu_1$ respectively. We construct the proof in Figure 4, which we call $\Omega$.

First, we construct the “superposition” derivation $\Psi$ given in Construction 59. We then extract the substitutions $\tau_1 \dots \tau_h$, and use Lemmas 63 and 64 to rearrange the formula. We distribute the substitutions $\sigma_h \dots \sigma_1$ and apply them. By Lemma 57, these work as intended, applying the substitution inference steps in the sFrege<sub>01</sub> proof $\Phi$. In particular, for all $v \in \eta_h^{-1}\mathcal{U}$, $\eta_h \mu_h E_n(v)$ is a closed formula. Finally, we distribute the substitutions $\nu_n \dots \nu_1$ and apply them; by Lemma 66 these work as intended, restoring the correct arguments to the atomic connectives.

The height of this proof is dominated by the use of Lemma 63, which is $O(nw) = O(hw^2)$.

The width of this proof is $O(hw(h+w))$. In the first phase, the width of the proof is dominated by the width of $\Psi$, which is $O(h^2w)$. After the use of Lemma 63 and before the application of the substitutions $\sigma_h \dots \sigma_1$, the width of the proof is $O(hw^2)$.

By Lemma 55, $[B_1|y_1]...[B_h|y_h]$ is tautological with respect to $V_n$. By construction, applying the substitutions $\sigma_h \dots \sigma_1$ to $[B_1|y_1]...[B_h|y_h]$ does nothing but dualise some pairs of pseudo-dual variables, and so the resulting formula is also tautological with respect to $V_n$. Then by Proposition 62, $[\nu_n \dots \nu_1 \sigma_h \dots \sigma_1 \langle B_1|y_1 \rangle \dots \langle B_h|y_h \rangle E_n(y)] = 1$.

By Lemma 56, $\tau_1 \dots \tau_h z_h$ is contradictory with respect to $V_n$. Then the flat formula obtained by applying all of the substitutions $\tau_1, \dots, \tau_h$ is also contradictory with respect to $V_n$. By construction, applying the substitutions $\sigma_h \dots \sigma_1$ to that formula does nothing but dualise some pairs of pseudo-dual variables, and so the resulting flat formula is also contradictory with respect to $V_n$. Then by Proposition 62, $[\nu_n \dots \nu_1 \sigma_h \dots \sigma_1 \tau_1 \dots \tau_h E_n(z_h)] = 0$.

Furthermore, for all $v \in \eta_h^{-1}\mathcal{U}$,

$$[\eta_h \mu_h E_n(v)] = [\eta_h v]$$

for all $v \in \eta_h^{-1}\{x_j\}$,

$$
\begin{align*}
& \llbracket [0|x_j, 1|\tilde{x}_j] \eta_h \mu_h E_{n\setminus j}(v) \mathbf{a}_j [1|x_j, 0|\tilde{x}_j] \eta_h \mu_h E_{n\setminus j}(v) \rrbracket \\
&= \llbracket [0 \mathbf{a}_j 1|\eta_h] v \rrbracket \\
&= a_j
\end{align*}
$$

and for all $v \in \eta_h^{-1}\{\tilde{x}_j\}$,

$$
\begin{align*}
& \llbracket [0|x_j, 1|\tilde{x}_j] \eta_h \mu_h E_{n\setminus j}(v) \mathbf{a}_j [1|x_j, 0|\tilde{x}_j] \eta_h \mu_h E_{n\setminus j}(v) \rrbracket \\
&= \llbracket [1 \mathbf{a}_j 0|\eta_h] v \rrbracket \\
&= \bar{a}_j
\end{align*}
$$

Therefore, the interpretation of the conclusion is $P_h$ and by Proposition 29, this can be checked in polynomial time on the size of $\Phi$. $\square$

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

**Theorem 43.** *System KSubG<sup>-</sup> p-simulates sFrege.*

*Proof.* Immediately from Theorems 42 and 67. $\square$

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

### D. Examples for Section VI

**Example 74.** Let $\Phi$ be a sFrege<sub>01</sub> proof given by

$$P_1 = \bar{a} \lor (b \lor a) \qquad (F_1)$$

$$P_2 = (a \land (\bar{b} \land \bar{a})) \lor ((a \lor b) \lor (\bar{a} \lor a)) \qquad (F_2)$$

$$P_3 = (a \lor b) \lor (\bar{a} \lor a) \qquad (\text{mp}(P_1, P_2))$$

This has atomic enumeration $A_\Phi = \{a, \bar{a}, b, \bar{b}\}$ (we use $a, b$ instead of $a_1, a_2$ to improve readability), and we take the variable enumeration $V_\Phi = \{w, \tilde{w}, x, \tilde{x}\}$ (likewise, we use $w, x$ instead of $x_1, x_2$). With respect to this variable enumeration, we obtain the open translations of the formulae of $\Phi$:

$$Q_1 = \tilde{w} \lor (x \lor w)$$

$$Q_2 = (w \land (\tilde{x} \land \tilde{w})) \lor ((w \lor x) \lor (\tilde{w} \lor w))$$

$$Q_3 = (w \lor x) \lor (\tilde{w} \lor w)$$

We factorise these formulae to obtain the factorised open translations of the formulae of $\Phi$:
$$A_1 = v_1 \lor (v_2 \lor v_3)$$

$$\eta_1 = [\tilde{w}|v_1, x|v_2, w|v_3]$$

$$A_2 = (v_4 \land (v_5 \land v_6)) \lor ((v_7 \lor v_8) \lor (v_9 \lor v_{10}))$$

$$\eta_2 = [w|v_4, \tilde{x}|v_5, \tilde{w}|v_6, w|v_7, x|v_8, \tilde{w}|v_9, w|v_{10}]$$

$$A_3 = (v_{11} \lor v_{12}) \lor (v_{13} \lor v_{14})$$

$$\eta_3 = [w|v_{11}, x|v_{12}, \tilde{w}|v_{13}, w|v_{14}]$$

We obtain $\Psi_i, \tau_i, \mu_i, \rho_i, \sigma_i, B_i$ for $1 \le i \le 3$ as follows:

* $\tau_1 = \langle 0|z_1 \rangle,$

* $\rho_1 = \eta_1,$

* $\mu_1 = [x \lor 0|v_2],$

* $\sigma_1 = \epsilon,$

* $B_1 = 0 \lor ((x \land 0) \lor (\tilde{w} \lor w))$

* $\Psi_1$ is shown as part of Figure 9

* $\tau_2 = \langle 0|z_2 \rangle,$

* $\rho_2 = \eta_2,$

* $\mu_2 = [v_9 \lor v_9|v_9],$

* $\sigma_2 = \epsilon,$

* $B_2 = 0 \lor ((w \lor \tilde{w}) \land ((w \lor \tilde{w}) \land ((\tilde{x} \lor x) \land (\tilde{w} \lor w))))$

* $\Psi_2$ is shown as part of Figure 9

* $\tau_3 = (((z_1 \lor z_2) \lor ((\tilde{w} \land w) \lor (((x \lor 0) \land \tilde{x}) \lor (w \land \tilde{w}))))|z_3),$

* $\rho_3 = \eta_3,$

* $\mu_3 = [v_{13} \lor v_{13}|v_{13}],$

* $\sigma_3 = \epsilon,$

* $B_3 = y_1 \land y_2,$

* $\Psi_3$ is shown as part of Figure 9,

where $y_1, y_2$ are fresh variables. We compose these as described in Construction 59 to obtain the derivation $\Psi$ in Figure 9

Due to space limitations, we show in Figure 10 an example of Phase II with the formula $z_3 \lor (w \land x)$ instead of $z_3 \lor ((w \land x) \lor ((\tilde{w} \lor \tilde{w}) \lor w))$. This construction ensures that when the guarded substitutions

$$\nu_a = \langle 0|w, 1|\tilde{w} \rangle^{l_a} \langle 1|w, 0|\tilde{w} \rangle^{r_a}$$

$$\nu_b = \langle 0|x, 1|\tilde{x} \rangle^{l_b} \langle 1|x, 0|\tilde{x} \rangle^{r_b}$$

are applied then the resulting formula will be interpreted as $(a \land b)$.

## E. Additional material for Section VII

In Figure 8 we give a “semi-formalization” of the proof of the Pythagoras theorem discussed in Section VII, using guarded substitutions.
<figure><img src="image_16.png" /><figcaption>Fig. 9. An example of the derivation $\Psi$ in Phase I of the p-simulation construction for the substitution Frege proof $\Phi$ shown in Example 74 consisting of two axioms and an application of modus ponens.</figcaption></figure>
<figure><img src="image_17.png" /><figcaption>Fig. 10. An example of phase II of the p-simulation construction on the formula $z_3 \lor (w \land x)$. All unlabelled derivations are only refactorings of explicit substitutions. The first part realises Lemma 63 and the second part Lemma 64.</figcaption></figure>