# Going from the huge to the small: Efficient succint representation of proofs
in Minimal implicational logic

Edward Hermann Haeusler†
Departmento de Informática
PUC-Rio
Rio de Janeiro, Brasil
<EMAIL_ADDRESS>
###### Abstract

A previous article shows that any linear height bounded normal proof of a
tautology in the Natural Deduction for Minimal implicational logic
($\mathbf{M}_{\supset}$) is as huge as it is redundant. More precisely, any
proof in a family of super-polynomially sized and linearly height bounded
proofs have a sub-derivation that occurs super-polynomially many times in it.
In this article, we show that by collapsing all the repeated sub-derivations
we obtain a smaller structure, a rooted Directed Acyclic Graph (r-DAG), that
is polynomially upper-bounded on the size of $\alpha$ and it is a certificate
that $\alpha$ is a tautology that can be verified in polynomial time. In other
words, for every huge proof of a tautology in $\mathbf{M}_{\supset}$, we
obtain a succinct certificate for its validity. Moreover, we show an algorithm
able to check this validity in polynomial time on the certificate’s size.
Comments on how the results in this article are related to a proof of the
conjecture $NP=CoNP$ appears in conclusion.

##  1 Introduction

In [13] and [12] we discuss the correlation between the size of proofs and how
redundant they can be. A proof or logical derivation is redundant whenever it
has sub-proofs that are repeated many times inside it. The articles [13] and
[12] focus on Natural Deduction (ND) proofs in the purely implicational
minimal logic $\mathbf{M}_{\supset}$. This logic, here called
$\mathbf{M}_{\supset}$, is PSPACE-complete and simulates polynomially any
proof in Intuitionistic Logic and full minimal logic, being hence an adequate
representative to study questions regarding computational complexity. The fact
that $\mathbf{M}_{\supset}$ has straightforward syntax and ND system is worthy
of notice. Moreover, compressing proofs in $\mathbf{M}_{\supset}$ can provide
very good glues to compress proofs in any one of these mentioned systems, even
for the Classical Propositional Logic. In [8] and [7], we prove that for every
$\mathbf{M}_{\supset}$tautology $\alpha$ there is a two-fold certificate for
the validity of $\alpha$ in $\mathbf{M}_{\supset}$. The certificate is
polynomially sized on the length of $\alpha$ and verifiable in polynomial time
on this length too. This is the general approach of our proof that
$NP=PSPACE$. It is well-known that $NP=PSPACE$ implies $CoNP=NP$, so we can
conclude also that $CoNP=NP$. This article, together with the articles [13],
[12], and one of the appendixes of [13], aim to show an alternative and more
intuitive proof that $NP=CoNP$. Recently, we deposited in arxiv a note, see
[9], that explains how to have a third alternative proof of $NP=CoNP$, this
time with a double certificate on linear height normal proofs, without to use
Hudelmaier result. This paper aims to show how to use the inherent redundancy
in huge proofs to have polynomial and polytime certificates by removing this
redundancy from the proofs. This is made by collapsing all the redundant sub-
proofs into only one occurrence in the proof, by type. We start with tree-like
Natural Deduction proofs and end up with a labeled r-DAG (rooted Directed
Acyclic Graph). In the sequel we explain and show what is said in the last two
phrases, previously stated. Currently, the use of the redundancy theorem and
corollary shown in [12], that is the essence of this proof’s approach, is not
easily adaptable to a proof of $NP=PSPACE$. In [8] the linearly height upper-
bounded proofs of the tautologies in $\mathbf{M}_{\supset}$are do not have
have to be normal.

In [13], we identify sets of huge proofs with sets of proofs that, when viewed
as strings, have their length lower-bounded by some exponential function.
Moreover, we can consider, without loss of generality, proof/deductions, which
are linearly height bounded, as stated in [7]. We prove that the exponentially
lower-bounded $\mathbf{M}_{\supset}$ proofs are redundant, in the sense that
there is at least one sub-proof for each proof that occurs exponentially many
times in it. In [12], we show that this result extends to super-polynomial
proofs, i.e., proofs that are lower-bounded by any polynomial. We consider
huge proofs/derivations as super-polynomial sized proofs. Thus, we prove that,
in any set of super-polynomially lower-bounded proofs in
$\mathbf{M}_{\supset}$, of tautologies, all proof are redundant. Redundancy
means that there is a sub-proof that occurs super-polynomially many times in
it for almost every proof in this set of huge proofs.

In section 2, we present a brief presentation and explanation on the proof-
theoretical terminology used here and the results from our previous articles.
For a more detailed and comprehensive reference, see [13], [12], [8] and [7].
Section 3 is the section where we show how to remove redundancies using a
recursive method adequately. Section 5 shows that the certificate obtained in
section 3 is of polynomial size and can be checked in polynomial time too. We
conclude this article in section 9. Finally, due to have a self-contained
article, and the background and previous results that this paper uses, we
advise the reader that there is an essential superposition of this article
with [12] and [13].

##  2 Background on proof-theory and brief presentation of previous results

One reason to study redundancy in proofs is to obtain a compressing method
based on redundancy removals. According to the redundancy theorem (theorem 12,
page 17 in [12]) and its corollary (corollary 13, page 18) proofs belonging to
a family of super-polynomial proofs are super-polynomial redundant. The reader
can find all the content of this section in [12] in more detail. This section
contains excerpts of [12].

The Natural Deduction system, defined in [5]), is taken as a set of inference
rules that settle the concept of a logical deduction. Natural Deduction does
not have axioms. It implements in the level of the logical calculus the
(meta)theorem of deduction, $\Gamma,A\vdash A\supset B$, via the discharging
mechanism. The $\supset$-introduction rule, for example, uses this discharging
mechanism in the logic calculus level.

[$A$] $\Pi$ $B$ $\supset$-Intro $A\supset B$

We embrace formulas occurrence $A$ in the derivation $\Pi$ of $B$ from $A$
with a pair of [] to indicate the discharge of them. An embraced formula
occurrence [$A$] means that from the $\supset$-Intro rule discharging it down
to the conclusion of the derivation, the inferred formulas do not depend
anymore on this occurrence $A$. The choice of formulas to be discharged in an
$\supset$-Intro rule is arbitrary and liberal. The range of this choice goes
from every occurrence of $A$, the discharged formula until none of them.

The following derivations show two different ways of deriving
$A\supset(A\supset A)$. Observe that in both deductions or derivations, we use
numbers to indicate the application of the $\supset$-Intro that discharged the
marked formula occurrence. For example, in the right derivation, the upper
application discharges the marked occurrences of $A$, while in the left
derivation, it is the lowest application that discharges the formula
occurrences $A$. There is a third derivation that both applications do note
discharge any $A$, and the conclusion $A\supset(A\supset A)$ keep depending on
$A$. This third alternative appears in figure 1. Natural Deduction systems can
provide logical calculi without any need to use axioms. In this article, we
focus on the system formed only by the $\supset$-Intro rule and the
$\supset$-Elim rule, as shown below, also known by modus ponens. The logic
behind this logical calculus is the purely minimal implicational logic,
$M_{\supset}$.

$A$ $A\supset B$ $\supset$-Elim $B$

Without loss of generality, we substitute the liberal discharging mechanism by
a greedy one that discharges every possible formula occurrence whenever the
$\supset$-Intro is applied. As stated and proved in [12], if there is an N.D.
proof of $\alpha$ in $\mathbf{M}_{\supset}$, then there is a proof of $\alpha$
in $\mathbf{M}_{\supset}$that has all applications of $\supset$-Intro as
greedy ones.

$[A]^{1}$ $A\supset A$ $\;{}^{1}$ $A\supset(A\supset A)$ $[A]^{1}$ $\;{}^{1}$
$A\supset A$ $A\supset(A\supset A)$

$A$ $A\supset A$ $A\supset(A\supset A)$

Figure 1: Two vacuous $\supset$-Intro applications

In our previous articles, we consider Natural Deduction as trees with the sake
of having simpler proofs of our results. There is a binary tree with nodes
labelled by the formulas and edges linking premises to the conclusion for any
ND derivation. The tree’s root is the conclusion of the derivation, and the
leaves are its assumptions. Figure 2 has the tree in figure 3 representing it.
In a proof-tree, the set of formulas that the label of $u$ depends on $v$
labels the edge from $v$ to $u$. This set of formulas is called the dependency
set of $u$ from $v$. The greedy version of the $\supset$-intro removes the
discharged formula from the corresponding dependency sets, as shown in figure
3. We need one more extra edge and the root node. The dependency set of the
conclusion labels this edge. That is why the edge links the conclusion to the
dot in figure 3.

$[A]^{1}$ $A\supset B$ $B$ $B\supset C$ $C$ 1  $\ignorespaces A\supset C$

Figure 2: A derivation in $M_{\supset}$ .$A\supset C$$C$$B$$A$$A\supset
B$$B\supset C$$\\{A\supset B,B\supset C\\}$$\\{A,A\supset B,B\supset
C\\}$$\\{B\supset C\\}$$\\{A,A\supset B\\}$$\\{A\supset B\\}$$\\{A\\}$ Figure
3: The tree representing the derivation in figure 2

Finally, we use bitstrings induced by an arbitrary linear ordering of formulas
to have a more compact representation of the dependency sets. Considering that
only subformulas of the conclusion can be in any dependency set, we only need
bitstrings of the size of the conclusion of the proof. Figure 4 shows this
final form of tree representing the derivation in figure 2 and 3, when the
linear order $\prec$ is $A\prec B\prec C\prec A\supset B\prec B\supset C\prec
A\supset C$. This explanation is an excerpt from [12].

.$A\supset C$$C$$B$$A$$A\supset B$$B\supset
C$$000110$$100110$$000010$$100100$$000100$$100000$ Figure 4: Tree with
bitstrings representing the derivation in figure 2

Without loss of generality, we consider the additional hypothesis on the
linear bound on height of the proof of $\mathbf{M}_{\supset}$tautologies. In
[7], we show that any tautology in $\mathbf{M}_{\supset}$has a Natural
Deduction normal proof of height bound by the size of this tautology. However,
proof of the tautology does not need to be normal. On the other hand, if we
consider the complexity class $CoNP$ (see the appendix in [13]) we are
naturally limited to linearly height-bounded proofs. The proofs, in
$\mathbf{M}_{\supset}$, of the non-hamiltonianicity of graphs, are linearly
height bounded.

We consider the usual definition of the syntax tree for
$\mathbf{M}_{\supset}$-formulas. Given a formula $\phi_{1}\supset\phi_{2}$ in
$\mathbf{M}_{\supset}$, we call $\phi_{2}$ its right-child and $\phi_{1}$ its
left-child. These formulas label the respective right and left child vertexes.
A right-ancestral of a vertex $v$ in a syntax-tree $T_{\alpha}$ of a formula
$\alpha$ is any vertex $u$, such that, either $v$ is the right-child of $u$,
or, there is a vertex $w$, such that $v$ is the right-child of $w$ and $u$ is
right-ancestral of $w$.

The left premise of a $\supset$-Elim rule is called a minor premise, and the
right premise is called the major premise. We should note that the conclusion
of this rule and its minor premise, are sub-formulas of its major premise. A
derivation is a tree-like structure built using $\supset$-Intro and
$\supset$-Elim rules. We have some examples depicted in the last section. The
derivation conclusion is the root of this tree-like structure, and the leaves
are what we call top-formulas. A proof is a derivation that has every top-
formula discharged by a $\supset$-Intro application in it. The top-formulas
are also called assumptions. An assumption that it is not discharged by any
$\supset$-Intro rule in a derivation is called an open assumption. If $\Pi$ is
a derivation with conclusion $\alpha$ and $\delta_{1},\ldots,\delta_{n}$ as
all of its open assumptions then we say that $\Pi$ is a derivation of $\alpha$
from $\delta_{1},\ldots,\delta_{n}$.

######  Definition 1 (Branch).

A branch in a derivation or proof $\Pi$ is any sequence
$\beta_{1},\ldots,\beta_{k}$ of formula occurrences in $\Pi$, such that:

  * •

$\delta_{1}$ is a top-formula, and;

  * •

For every $i=1,k-1$, either $\beta_{i}$ is a $\supset$-Elim major premise of
$\beta_{i+1}$ or $\beta_{i}$ is a $\supset$-Intro premise of $\beta_{i+1}$,
and;

  * •

$\delta_{k}$ either is the conclusion of the derivation or the minor premise
of a $\supset$-Elim.

A normal derivation/proof in $\mathbf{M}_{\supset}$is any derivation that does
not have any formula occurrence simultaneously a major premise of a
$\supset$-Elim and the conclusion of a $\supset$-Intro. A formula occurrence
that is a conclusion of a $\supset$-Intro and a major premise of
$\supset$-Elim is called a maximal formula. In [18], Dag Prawitz proves the
following theorem for the Natural Deduction system for the full111The full
propositional fragment is $\\{\lor,\land,\supset,\neg,\bot\\}$ propositional
fragment of minimal logic.

######  Theorem 1 (Normalization).

Let $\Pi$ be a derivation of $\alpha$ from
$\Delta=\\{\delta_{1},\ldots,\delta_{n}\\}$. There is a normal proof
$\Pi^{\prime}$ of $\alpha$ from $\Delta^{\prime}\subseteq\Delta$.

In any normal derivation/proof, a branch’s format provides worth information
on why huge proofs are redundant, as we will see in the next sections. Since
no formula occurrence can be a major premise of $\supset$-Elim and conclusion
of a $\supset$-Intro rule in a branch we have that the conclusion of a
$\supset$-Intro can only be the minor premise of a $\supset$-Elim or it is not
a premise of any rule application at all in the same branch. In this last
case, it is the derivation’s conclusion or the minor premise of a
$\supset$-Elim rule. In any case, it is the last formula in the branch. Thus,
for any branch, every conclusion of a $\supset$-Intro has to be a premise of a
$\supset$-Intro. Hence, any branch in a normal derivation splits into two
parts (possibly empty). The E-part starts it with the top-formula, and, every
formula occurrence in it is the major premise of a $\supset$-Elim. We may have
then a formula occurrence that is the conclusion of a $\supset$-Elim and
premise of a $\supset$-Intro rule that is called minimal formula of the
branch. The minimal formula starts the I-part of the branch, where every
formula is the premise of a $\supset$-Intro, excepted the last formula of the
branch. From the branches’ format, we can conclude that the sub-formula
principle holds for normal proofs in Natural Deduction for
$\mathbf{M}_{\supset}$, in fact, for many extensions. A branch in $\Pi$ is
said to be a principal branch if its last formula is the conclusion of $\Pi$.
A secondary branch is a branch that is not principal. The primary branch is
called a 0-branch. Branches, where the last formula is the minor premise of a
rule in the E-part of a $n$-branch, is a $n+1$-branch.

######  Corollary 2 (Sub-formula principle).

Let $\Pi$ be a normal derivation of $\alpha$ from
$\Delta=\\{\delta_{1},\ldots,\delta_{m}\\}$. It is the case that for every
formula occurrence $\beta$ in $\Pi$, $\beta$ is a sub-formula of either
$\alpha$ or of some of $\delta_{i}$.

To facilitate the presentation, we only handle normal proofs in expanded form.

######  Definition 2.

A normal proof/derivation is in expanded form, if and only if, all of its
minimal formulas are atomic.

Without loss of generality, we can consider that formula in
$\mathbf{M}_{\supset}$ is a tautology if and only if there is a normal proof
in expanded form that proves it. Of course, if it is a tautology, it has
proof, and so it has normal proof by normalization. We use the following fact
to obtain the expanded form from normal proof. In [12] we prove that all
tautologies have normal proofs in expanded form. See the first appendix of
[12]

$[D]$ $C$ $B$ $[A]$ $[A\supset(B\supset(C\supset q))]$ $B\supset(C\supset q)$
$C\supset q$ $q$ $A\supset q$ $[(A\supset q)\supset(D\supset q)]$ $D\supset q$
$q$ $D\supset q$ $((A\supset q)\supset(D\supset q))\supset(D\supset q)$
$(A\supset(B\supset(C\supset q)))\supset(((A\supset q)\supset(D\supset
q))\supset(D\supset q))$ $\alpha$$A\supset(B\supset(C\supset
q))$$A$$(B\supset(C\supset q))$$B$$C\supset q$$C$$q$$((A\supset
q)\supset(D\supset q))\supset(D\supset q)$$(A\supset q)\supset(D\supset
q)$$A\supset q$$A$$q$$D\supset q$$D$$q$$D\supset q$$D$$q$ Figure 5: A mapped
N.D. proof

In [12], we observed correspondence between each minimal formula of a branch,
in a normal and expanded proof $\Pi$, employing a one-to-one correspondence to
the respective top-formula occurrence of its branch. Figure 5 illustrates the
mapping from the proof into the syntax-tree of the proved formula according to
this correspondence. Note that the two positions of the atomic formula $q$ in
the syntax tree uniquely indicates the top-formula in the E-part of the
Natural Deduction proof/derivation to which it belongs. We can consider that
the two $q$’s are in fact, different. The top-formula of each $q$ is the
biggest in the inverse path (upwards) following the reverse of the right child
edge. Definition 5, in the sequel, has the purpose of setting this
correspondence in the representation of proofs formally. With the sake of a
more precise presentation, we provide below the definition of a formula’s
syntax tree.

######  Definition 3 (Syntax tree of a formula).

Let $\alpha$ be a $\mathbf{M}_{\supset}$-formula. The syntax tree of $\alpha$
is the triple $\langle V,E_{left},E_{right},L\rangle$ where $V$ is a set, of
vertexes, $E_{s}\subseteq V\times V$, $s=left,right$, the corresponding left
and right edges, such that $\langle V,E_{left},E_{right}\rangle$ is an ordered
full binary tree, and, $L$ is a bijective function from $V$ onto the
subformulas of $\alpha$, such that:

  * •

$L(r)=\alpha$, where $r\in V$ is the root of the tree $\langle
V,E_{left},E_{right}\rangle$, and;

  * •

For every formula $\varphi_{1}\supset\varphi_{2}\in Sub(\alpha)$, if
$L(v)=\varphi_{1}\supset\varphi_{2}$, $\langle v,v_{1}\rangle\in E_{left}$ and
$\langle v,v_{2}\rangle\in E_{right}$ then $L(v_{1})=\varphi_{1}$ and
$L(v_{2})=\varphi_{2}$.

######  Definition 4 (Partially mapped ND-proofs).

Let $\alpha$ be a $\mathbf{M}_{\supset}$-formula and $T_{\alpha}=\langle
V,E_{left},E_{right},L\rangle$ its syntax tree. Let $\Pi$ be a
$\mathbf{M}_{\supset}$-ND normal derivation of $\alpha$. A partially mapped
ND-proof of $alpha$ is a structure $\langle\Pi,T_{\alpha},l\rangle$, where $l$
is a partial function from the formula occurrences in $\Pi$ to $V$, such that,
the following conditions hold.

  * •

If $\gamma$ is the minimal formula of a branch $\overrightarrow{b}$ in $\Pi$
then if $\ell(\gamma)$ is defined then $L(\ell(\gamma))=\gamma$;

  * •

If $\gamma$ is the minimal formula of a branch $\overrightarrow{b}=\langle
b_{0},\ldots,b_{j}=\gamma,\ldots,b_{k}\rangle$ and $\ell(\gamma)$ is defined
then either $\ell(b_{j-1})$ or $\ell(b_{j+1})$ are defined, and;

  * •

If $\varphi_{2}$ is the conclusion of a $\supset$-Elim rule in $\Pi$, that has
premises $\varphi_{1}\supset\varphi_{2}$ and $\varphi_{1}$, and
$\ell(\varphi_{2})=v_{2}$ then there are $v$ and $v_{1}$, such that $\langle
v,v_{2}\rangle\in E_{right}$, $\langle v,v_{1}\rangle\in E_{left}$,
$\ell(\varphi_{1})=v_{1}$ and $\ell(\varphi_{1}\supset\varphi_{2})=v$;

  * •

If $\varphi_{1}\supset\varphi_{2}$ is the conclusion of a $\supset$-Intro rule
in $\Pi$, that has premise $\varphi_{2}$ and
$\ell(\varphi_{1}\supset\varphi_{2})=v$ then there is $v^{\prime}\in V$,
$\langle v,v^{\prime}\rangle\in E_{right}$ and $\ell(v^{\prime})=\varphi_{2}$.

######  Definition 5 (E-mapped Natural Deduction Normal Expanded proofs).

Let $\alpha$ be a $\mathbf{M}_{\supset}$-formula, $T_{\alpha}=\langle
V,E_{left},E_{right},L\rangle$ be the syntax tree of $\alpha$ and $\Pi$ a
normal and expanded proof of $\alpha$. The triple
$\langle\Pi,T_{\alpha},l\rangle$ is an E-mapped Natural Deduction proof, if
and only if, $l$ is defined on all formula occurrences that take part in the
E-parts of branches in $\Pi$, including the minimal formulas. Moreover the
following condition must hold:

  * •

For every branch $\overrightarrow{b}$, if $q$ is the minimal formula of
$\overrightarrow{b}$, $\ell(q)=v\in V$ and $\beta$ is the top-formula
(occurrence) of $\overrightarrow{b}$ then $\ell(\beta)=u$, where $u$ is the
right-ancestral of $v$ that is left-child of some $w\in V$.

In [12] we show that the above definition of E-mapped Natural Deduction Normal
Expanded proof, EmND for short, is well-defined. Moreover, we have the
following proposition. We consider a branch as a sequence of formula
occurrences numbered from top-formula down to the branch’s last formula. The
proof of this proposition is in [12]

######  Proposition 3.

Let $\langle\Pi,T_{\alpha},l\rangle$ be a EmND of $\alpha$. We have that to
each branch $\overrightarrow{b}=\langle\beta_{0},\ldots,\beta_{k},$ in $\Pi$
that has the minimal formula occurrence $q=\beta_{j}$, such that
$\ell(\beta_{j})=u\in V$, there exists one and only one path $p=\langle
u_{0},\ldots,u_{j}\rangle$ in $T_{\alpha}$, with $u_{j}=u$, and $u_{0}$ such
that, $\ell(\beta_{i})=u_{i}$, $i=0,\ldots,j$.

We point out that in proposition 3, above,
$\langle\beta_{0},\ldots,\beta_{j}=q\rangle$ is the E-part of
$\overrightarrow{b}$. This proposition 3 states that any given E-part
$\langle\beta_{0},\ldots,\beta_{j}\rangle$ of a branch in an EmND is an
instance of at most one path $p=\langle u_{0},\ldots,u_{j}\rangle$ in
$T_{\alpha}$, such that $L(u_{i})=\beta_{i}$, $i=0,\ldots,j$. Moreover, this
path $p$ is as stated in the definition of EmND in the its only item. Given a
EmND $\Pi$, for each E-part, in an EmND, exists a path of the form stated in
definition of EmND, in the syntax tree of the conclusion of theEmND. The
number of such paths in the syntax tree is upper-bounded by its size, then the
number of different E-parts types in any EmND is at most of the size of the
conclusion of this EmND. We have the following lemma:

######  Lemma 4 (Linear upper-bound on types of E-parts).

Let $\Pi$ be an EmND proving the $\mathbf{M}_{\supset}$-formula $\alpha$. The
number of different types of E-parts occurring in this EmND is at most the
size of the $T_{\alpha}$.

We remark, as also observed in [12], that we can label the nodes of a Natural
Deduction proof-tree with the nodes (not the labels) of the syntax tree of the
conclusion of the proof-tree. In doing that we will have the same effect on
counting different types of E-parts that is stated by lemma 4.

###  2.1 Redundancy in huge $\mathcal{M}_{\supset}$ mapped derivations

Due to the linear speedup theorem, see [19] page 63-64, Theorem 3.10, we can
consider, w.l.o.g a linear height bounded proof of $\alpha$ is a proof which
height is upper-bounded by the length of $\alpha$. In fact, in this article,
because of counting details, we consider that the upper-bounded is the size of
the syntax tree $\left|T_{\alpha}\right|$. Since
$\left|T_{\alpha}\right|=\left|\alpha\right|$, the definition is equivalent.
From [12], we have the following lemmas. In [12] the reader can fund both
proofs.

######  Lemma 5 (Spreading Branchs Repetitions).

Let $\langle\Pi,T_{\alpha},l\rangle$ be a linearly height bounded EmND proof
of $\alpha$, $0<p\in\mathbb{N}$ and $m=\left|\alpha\right|$. If there is a
branch $\overrightarrow{b}$ that has more than $m^{p}$ instances occurring in
$\Pi$ then there is a level $\mu$, such that, at least $m^{p-1}$ instances of
$\overrightarrow{b}$ have the minimal formula $q_{\overrightarrow{b}}$ of
$\overrightarrow{b}$ occurring in level $\mu$.

######  Lemma 6 (Branchs and sub-derivations).

Let $\Pi$ be a proof of $\alpha$, and $\overrightarrow{b}$ a branch in $\Pi$
under the same conditions of the lemma 5 above. Then there is a (sub)
derivation $\Pi_{\overrightarrow{b}}$ of $\Pi$, such that,
$\Pi_{\overrightarrow{b}}$ has at least $m^{p-1}$ instances occurring in
$\Pi$.

######  Definition 6 (Linearly height-bounded EmND proofs).

Let $\Lambda$ be the set of mapped linearly height-bounded ND
$\mathbf{M}_{\supset}$proofs. We use the notation $c(\Pi)$ to denote the
formula that is the conclusion of $\Pi$. Note that we can consider $\Lambda$
as a predicate $\Lambda(x)$ that is true if and only if $x$ is assigned to a
mapped linearly height-bounded ND proof.

$S_{\Lambda}=\\{\mbox{$\Pi\in\Lambda$}:\mbox{$\forall
p\in\mathbb{N},p>0,\exists n_{0},\forall n>n_{0}$, $\left|T_{c(\Pi)}\right|=n$
and $\left|\Pi\right|>n^{p}$)}\\}$

As explained in [12], $S_{\Lambda}$ contains all huge or hard linearly height
upper-bounded proofs in $\mathbf{M}_{\supset}$. Of particular interest is the
following set. Let $Taut_{\mathbf{M}_{\supset}}$ be the set of all ND mapped
proofs of $\mathbf{M}_{\supset}$tautologies. The following set:

######  Definition 7.

Let $\Theta$ be the following set:

$\Theta_{\mathbf{M}_{\supset}}=\\{\mbox{$\Pi\in
Taut_{\mathbf{M}_{\supset}}$}:\mbox{$\forall p\in\mathbb{N},p>0,\exists
n_{0},\forall n>n_{0}$, $\left|T_{c(\Pi)}\right|=n$ and
$\left|\Pi\right|>n^{p}$}\\}$

$\Theta_{\mathbf{M}_{\supset}}$ is the set of super-polynomially sized
$\mathbf{M}_{\supset}$ND mapped proofs.

In [12], we show that every $\Pi\in S_{\Lambda}$ is redundant. This means that
there is at least one sub-proof $\Pi_{s}$ of $\Pi$ that repeats as many times
as it is the size of $\Pi$. We have the following theorem 7, proved in [12].
We emphasise that the proofs in $S_{\Lambda}$ are linearly heigh-bounded.

######  Theorem 7.

For all $p\in\mathbb{N}$, $p>3$, and for all $\Pi\in S_{\Lambda}$, such that,
$\left|\mathcal{T}(c(\Pi))\right|=m$ and $\left|\Pi\right|>m^{p}$, then there
is a sub-derivation $\Pi_{s}$ of $\Pi$ and a level $\mu$ in $\Pi$, such that,
$\Pi_{s}$ has at least $m^{p-3}$ instances occurring in the level $\mu$ in
$\Pi$.

From theorem 7 we can roughly state the corollary 8.

######  Corollary 8.

All, but finitely many, proofs belonging to an arbitrary family of super-
polynomial and linearly height upper-bounded proofs, are super polynomial
redundant.

##  3 Removing redundancies from huge $\mathbf{M}_{\supset}$linearly height
bounded proofs

Corollary 8 says that any proof in an unbounded set of super-polynomial
proofs, linearly bounded on the height, is almost as redundant as it is huge.
We can show that there are level $\mu$ and a derivation $\Pi$ that occurs as
many times in $\mu$ as it is the size of the proof. This section shows a
polynomial sized certificate of validity for any huge tautology that belongs
to this set of super-polynomial proofs. Our argumentation to prove this is to
remove all redundancies in the original derivation, preserving logical
consequence.

Given a non-empty finite set $S$, $card(S)=n$, and a total order
$\mathcal{O}_{S}=\\{s_{1},\ldots,s_{n}\\}$ on $S$, the set
$B(\mathcal{O}_{S})$ is $\\{b_{1}\ldots b_{n}:\mbox{$b_{i}=0$ or $b_{i}=1$,
$i=1\ldots n$}\\}$. There is a bijection $F$ from $B(\mathcal{O}_{S})$ onto
the powerset of $S$ given by $F(b_{1}\ldots b_{n})=\\{s_{i}:b_{i}=1\\}$.
$B(\mathcal{O}_{S})$ is also called the set of bitstrings over
$\mathcal{O}_{S}$.

Given a $\mathbf{M}_{\supset}$formula $\alpha$, $sub(\alpha)$ is the set of
all sub-formulas of $\alpha$.

######  Definition 8 (r-DagProof).

A pre r-DagProof for a $\mathbf{M}_{\supset}$formula $\alpha$ is a structure
$\mathcal{C}$ = $\langle
V,E_{d},E_{A},r,\ell,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$

  1. 1.

$V$ is a non-empty set of nodes;

  2. 2.

$E_{d}\subseteq V\times V$, deduction edges;

  3. 3.

$E_{A}\subseteq V\times V$, ancestrality edges;

  4. 4.

$\mathcal{O}_{\alpha}$ is a total order on $sub(\alpha)$;

  5. 5.

$r\in V$ is the root of the $\mathcal{C}$;

  6. 6.

$\ell:V\rightarrow sub(\alpha)$, for $v\in V$, $\ell(v)$ is the (formula)
label of $v$, $sub(\alpha)$ is the set of all sub-formulas of $\alpha$;

  7. 7.

$L:E_{d}\rightarrow\mathcal{B}(\mathcal{O})$ is a function, such that, for
every $\langle u,v\rangle\in E_{d}$, $L(\langle u,v\rangle)\in
B(\mathcal{O}_{S})$;

  8. 8.

$\delta:E_{A}\rightarrow\mathbb{N}$, a total function;

  9. 9.

$\rho:E_{d}\rightarrow\mathbb{N}$, a partial function;

Subjected to the following conditions:

(Global)

$\langle V,E_{d},r\rangle$ is a connected DAG with unique root $r$ and for
each node $v\in V$, if $\langle r=u_{1},\ldots,u_{m}=v\rangle$ and $\langle
r=v_{1},\ldots,v_{n}=v\rangle$ are two inverse paths from $r$ to $v$ then
$m=n$, i.e., for any $v$, any longest path from $r$ to $v$ has the same length
of a shortest path from $r$ to $v$. Moreover, for each $v\in V$, if $v\neq r$
then there is a path from $v$ to $r$ and for every $u$, $\langle
u,u\rangle\not\in E_{d}$.

(${\mathbf{E}_{d}-(l/L)_{1}}$ consistency)

For every $\langle u,v\rangle,\langle v,w\rangle\in E_{d}$, if there is no
$\langle u^{\prime},v\rangle\in E_{d}$, such that, $u^{\prime}\neq u$ and
$\rho(\langle v,w\rangle)=\uparrow$, then $\ell(u)=\varphi_{1}$,
$\ell(v)=\varphi_{2}\supset\varphi_{1}$, $L(\langle v,w\rangle)=L(\langle
u,v\rangle)-\vec{b}_{\varphi_{2}}$;

(${\mathbf{E}_{d}-(l/L)_{2}}$ consistency)

For every $\langle u_{1},v\rangle,\langle u_{2},v\rangle,\langle v,w\rangle\in
E_{d}$, there is no $\langle u^{\prime},v\rangle\in E_{d}$, such that,
$u^{\prime}\neq u_{i}$, $i=1,2$, and $\rho(\langle v,w\rangle)=\uparrow$, then
$\ell(u_{1})=\varphi_{1}$, $\ell(u_{2})=\varphi_{1}\supset\varphi_{2}$,
$\ell(v)=\varphi_{2}$, $L(\langle v,w\rangle)=L(\langle
u_{1},v\rangle)oplusL(\langle u_{2},v\rangle$;

(${\mathbf{E}_{A}}$-target consistency)

If $\langle u,v\rangle\in E_{A}$ then either there is no $\langle
w,v\rangle\in E_{d}$ or there is $\langle v,w\rangle\in E_{A}$, $w\neq u$;

(${\mathbf{E}_{A}}$-source consistency)

If $\langle u,v\rangle\in E_{A}$ then there is $\langle w,u\rangle\in E_{d}$,
$w\neq v$ and $\delta(\langle u,v\rangle)=\rho(\langle w,u\rangle)$

(${\mathbf{E}_{A}}$-ancestrality irreflexivity)

For every $u$, $\langle u,u\rangle\not\in E_{A}$.

A pre r-DagProof, satisfying definition 8 above, is a r-DagProof, or a
certificate for $\ell(r)$, if it is sound, or equivalently, if algorithm 3
answers “Correct” when executes on it. In section 5 we define soundness of a
r-DagProof and we define the algorithm 3. In the meanwhile we deal with pre
r-DagProofs. Specifically, in this section, this difference between pre
r-DagProofs and r-DagProofs is not relevant.

We provide a bit of terminology in this part of the article. Regarding theorem
7, we denote by matrix the sub-derivation of the ambient derivation, i.e. the
huge one, that has many instances repeated. Definition 11 define the set of
nodes in an r-DagProof that is formed by top-formulas or their representatives
after collapsing. We need the definition of top-formulas and representative
top-formulas.

######  Definition 9 (Top-formula of a r-DagProof).

A node $v\in V$, of a r-DagProof $\mathcal{C}=\langle
V,E_{d},E_{A},r,l,L,P,\mathcal{O}_{\alpha},E_{\delta}\rangle$, is a top-
formula, if and only if, there is no $w\in V$, such that $\langle
w,v\rangle\in E_{d}$ or $\langle w,v\rangle\in E_{A}$.

######  Definition 10 (Representative top-formula of a r-DagProof).

Given a r-DagProof $\mathcal{C}$=$\langle
V,E_{d},E_{A},r,l,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$, $v\in V$ is a
representative top-formula, if and only if, there is no $w\in V$, such that
$\langle w,v\rangle\in E_{A}$. Moreover, there is a sequence
$v=w_{1},\ldots,w_{n}$, $w_{i}\in V$, $i=1,n$, such that, for every $i=1,n-1$,
$\langle w_{i},w_{i+1}\rangle\in E_{A}$, and there is no $w\in V$, such that,
$\langle w,w_{n}\rangle\in E_{d}$.

######  Definition 11.

Given a r-DagProof $\mathcal{C}=\langle
V,E_{d},E_{A},r,\ell,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$, its set of
initials, $I(\mathcal{C})$ is the set of representative top-formulas together
with its top-formulas.

The following mapping defines the detachment of an instance of the matrix
$\mathcal{C}$, defined by its root $k$, from $\mathcal{D}$ and link its
position to the matrix $\mathcal{C}$ accordingly. In the following
definitions, if $\mathcal{C}$ is a r-DagProof $\langle
V,E_{d},E_{A},r,l,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$, we use the
notations $E_{A}(\mathcal{C})$, $E_{d}(\mathcal{C})$, $V(\mathcal{C})$,
$r(\mathcal{C})$, $\ell(\mathcal{C})$, etc, to denote $E_{A}$, $E_{d}$, $V$,
$r$, $l$, etc, respectively. Given a set of nodes $V^{\prime}\subseteq V$,
such that $r\not\in V^{\prime}$, the restriction of $\mathcal{C}$ to the set
of nodes $V^{\prime}$ is $\mathcal{C}\mid_{V^{\prime}}$ and it is defined
below:

$\langle
V^{\prime},E_{d}\mid_{V^{\prime}},E_{A}\mid_{V^{\prime}},r,l\mid_{V^{\prime})},L\mid_{(E_{d}\mid_{V^{\prime}})},\rho\mid_{(E_{d}\mid_{V^{\prime}})},\delta\mid_{(E_{A}\mid_{V^{\prime}})},\mathcal{O}_{\alpha}\rangle$

,where if $E\subseteq V\times V$ is a set of edges and $V^{\prime}\subseteq V$
then $E\\!\\!\mid_{V^{\prime}}=\\{\langle v,u\rangle:\mbox{$v\in V^{\prime}$
and $u\in V^{\prime}$}\\}$.

######  Definition 12 (Difference of r-DagProofs).

Let $\mathcal{C}$ and $\mathcal{D}$ be two r-DagProofs, the graph difference
$\mathcal{D}-\mathcal{C}$ is
$\mathcal{D}\\!\\!\mid_{(V(\mathcal{D})-V(\mathcal{C}))}$.

The difference of r-DagProofs is not a r-DagProof itself. In the definition
below we use the notation $\mathcal{D}\\!\\!\uparrow\\!\\!\\!(k)$, where
$\mathcal{D}$ is a r-DagProof and $k\in V(\mathcal{D})$, to denote the biggest
sub r-DagProof of $\mathcal{D}$ that has $k$ as root. In the particular case
that $\mathcal{D}$ is a tree, $\mathcal{D}\\!\\!\uparrow\\!\\!\\!(k)$ is the
sub-tree of $\mathcal{D}$ that has root $k$.

######  Definition 13 (Detach and link sub r-DagProofs function).

Let $\mathcal{D}$ be a r-DagProof of $\alpha$ and $k$ a node of $\mathcal{D}$
that it is the root of an instance of the r-DagProof $\mathcal{C}$ that is its
matrix, as given by theorem 7. Let $i\in\mathbb{N}$, a label, and
$\mathcal{C}^{\prime}=\mathcal{D}\\!\\!\uparrow\\!\\!\\!(k)$. Define
$\mathcal{D}^{\prime}=(\mathcal{D}-\mathcal{C}^{\prime})\cup\mathcal{C}$. We
define $DetachLink(\mathcal{D},k,\mathcal{C},i)$ as following:

$\begin{array}[]{l}\langle V(\mathcal{D}^{\prime}),\\\
E_{d}(\mathcal{D}^{\prime})\cup\\{\langle r(\mathcal{C}),v\rangle:\langle
k,v\rangle\in E_{d}(\mathcal{D})\\},\\\
E_{A}(\mathcal{D}^{\prime})\cup\\{\langle v,w\rangle:\mbox{$\langle
k,v\rangle\in E_{d}(\mathcal{D})$ and $w\in I(\mathcal{C})$}\\},\\\
r(\mathcal{D}^{\prime}),\\\ \ell(\mathcal{D}^{\prime}),\\\
L(\mathcal{D}^{\prime})\cup\\{\langle r(\mathcal{C}),v\rangle\mapsto L(\langle
k,v\rangle):\langle k,v\rangle\in E_{d}(\mathcal{D})\\},\\\
\rho(V(\mathcal{D}^{\prime}))\cup\\{\langle v,w\rangle\mapsto i:\mbox{$\langle
k,v\rangle\in E_{d}(\mathcal{D})$ and $w\in I(\mathcal{C})$}\\},\\\
\delta(V(\mathcal{D}^{\prime}))\cup\\{\langle r(\mathcal{C}),v\rangle\mapsto
i:\langle k,v\rangle\in E_{d}(\mathcal{D})\\},\\\
\mathcal{O}_{\alpha}\rangle\end{array}$

Figures 6 and 7 illustrate what happens when we apply three DetachLink
operations in an ambient r-DagProof. When we repeat this operation to every
instance of a matrix $\mathcal{C}$ occurring in a fixed level $\mu$, we say
that we performed a collapse of the instances of $\mathcal{C}$ in
$\mathcal{D}$ in level $\mu$. This operation is described by algorithm 1 and
is denoted by $Collapse(\mathcal{C},\mathcal{D},\mu)$.

Consider a EmND proof that has more than one matrix $\mathcal{C}$ with
instances occurring super-polynomially many times in it. Thus, Lemma 9 shows
that we can use theorem 7 to obtain the list of all matrices having a super-
polynomially many instances occurring in a fixed level $\mu$ of this EmND
proof. We remember that a matrix derivation/proof, in our terminology, is
nothing but a sub-derivation/sub-proof that has at least one instance in other
proof. This lemma obtains a set of Matrices having all instances occurring in
the lowest level in a specific EmND proof. Moreover, no matrix instance is a
proper sub-derivation of any other matrix instance in the set. We call this an
independent set of matrices from $\Pi$ to this set.

######  Definition 14 (Independent set of matrices in a proof/derivation).

Let $\Pi$ be an EmND proof/derivation. A set of matrices

$S=\\{\Pi_{\nu}:\mbox{$\Pi_{\nu}$ is a matrix in $\Pi$ which only has instance
in a level $\nu$}\\}$

is an independent set of matrices, if and only if, there is no $\nu_{1}$ and
$\nu_{2}$ levels in $\Pi$, $\nu_{1}\neq\nu_{2}$, and instances $\Pi_{1}$ and
$\Pi_{2}$ of $\Pi_{\nu_{1}}$ and $\Pi_{\nu_{2}}$, respectively,
$\Pi_{\nu_{i}}\in S$, $1=1,2$, such that, $\Pi_{1}$ is a sub-derivation of
$\Pi_{2}$, or $\Pi_{2}$ is a sub-derivation of $\Pi_{1}$.

Given a set $S$ of independent matrices of a proof/derivation, we can prove
that if $\Pi_{\nu}\in S$ then no instance of $\Pi_{\nu}$ is sub-derivation of
$\Pi_{\mu}\in S$, unless $\Pi_{\mu}=\Pi_{\nu}$. Thus, if $\Pi_{\nu}\in S$ then
there is no level $\mu<\nu$ with instances that are super-derivations of
instances of $\Pi_{\nu}$. In a certain sense, $\nu$ is a local lowest level.

######  Lemma 9 (List of super-polynomially repeated matrices).

For all $p\in\mathbb{N}$, $p>3$, and for all $\Pi\in S_{\Lambda}$222The set
$S_{\Lambda}$ is defined in defintion 6, such that,
$\left|\mathcal{T}(c(\Pi))\right|=m$ and $\left|\Pi\right|>m^{p}$, then there
is a set $M$ of independent matrices for sub-derivations instances of $\Pi$,
such that, for every $\Pi_{s}\in M$, $\Pi_{s}$ has at least $m^{p-3}$
instances occurring in some level $\xi$ in $\Pi$.

###### Proof.

of lemma 9. Using the conditions on lemma, Theorem 7 provides at least one
level $\mu$ and a matrix $\Pi_{s}$ that has at least $m^{p-3}$ instances
occurring in $\mu$. Thus, the sets

$S_{\nu}=\\{\Pi_{s}:\mbox{$\Pi_{s}$ is a matrix having at least $m^{p-3}$
instances in $\nu$ in $\Pi$}\\}$

where $\nu$ is a level in $\Pi$, form a family. The family $(S_{\nu})_{\nu\in
Lev(\Pi)}$ has at least the non-empty set $S_{\mu}$. Moreover, if
$\nu_{1}<\nu_{2}$ and $S_{\nu_{1}}\neq\emptyset$ then $S_{\nu_{2}}$ contains
all the subtrees of the trees in $S_{\nu_{1}}$ that occurs in level
$\nu_{2}-\nu_{1}$ in the elements (trees) in $S_{\nu_{1}}$. If $T$ is a
subtree of $T^{\prime}$ then we can say that $T^{\prime}$ is a super-tree of
$T$. The same applies to sub-derivations and super-derivations. We define the
set $L$ of levels $\xi$, such that $S_{\xi}$ has no instance in $\Pi$ in level
$\xi$ that is a super-derivation of an instance of $\Pi_{s}\in S_{\mu}$,
$\mu\neq\xi$. The set $\\{\Pi_{\xi}:\mbox{$\xi\in L$}\\}$ is an independent
set of matrices. It is the biggest one, indeed.

Lemma 9 is used to provide the initial list of instances to collapse in the
algorithm 2. This list can be alternatively defined as, given $p>3$, the
lowest sub-derivations of a proof $\Pi$, of size bigger than
$\left|\Pi\right|^{p}$, that occurs at least $\left|\Pi\right|^{p-3}$ times in
their respective lowest level $\mu$. Definition 16 introduces the notation
$LRI(\Pi)$ to denote this set.

$r$$l_{1}$$l_{20}$$l_{30}$$l_{k0}$$l_{50}$$l_{51}$$l_{41}$$l_{31}$$l_{42}$$l_{43}$$l_{21}$$l_{32}$$l_{44}$$l_{33}$$l_{45}$$l_{52}$$l_{60}$$l_{61}$$\ldots$$v_{1}$$v_{20}$$v_{30}$$v_{k0}$$v_{50}$$v_{51}$$v_{41}$$v_{31}$$v_{42}$$v_{43}$$v_{21}$$v_{32}$$v_{44}$$v_{33}$$v_{45}$$v_{52}$$v_{60}$$v_{61}$$\ldots$$u_{1}$$u_{20}$$u_{30}$$u_{k0}$$u_{50}$$u_{51}$$u_{41}$$u_{31}$$u_{42}$$u_{43}$$u_{21}$$u_{32}$$u_{44}$$u_{33}$$u_{45}$$u_{52}$$u_{60}$$u_{61}$
Figure 6: Some instances of the matrix $\mathcal{C}$ in the ambient r-DagProof
$\mathcal{D}$
$r$$l_{1}$$l_{20}$$l_{30}$$l_{k0}$$l_{50}$$l_{51}$$l_{41}$$l_{31}$$l_{42}$$l_{43}$$l_{21}$$l_{32}$$l_{44}$$l_{33}$$l_{45}$$l_{52}$$l_{60}$$l_{61}$$\ldots$$v_{1}$$v_{20}$$v_{30}$$v_{k0}$$v_{50}$$v_{51}$$v_{41}$$v_{31}$$v_{42}$$v_{43}$$v_{21}$$v_{32}$$v_{44}$$v_{33}$$v_{45}$$v_{52}$$v_{60}$$v_{61}$$\ldots$$u_{1}$$u_{20}$$u_{30}$$u_{k0}$$u_{50}$$u_{51}$$u_{41}$$u_{31}$$u_{42}$$u_{43}$$u_{21}$$u_{32}$$u_{44}$$u_{33}$$u_{45}$$u_{52}$$u_{60}$$u_{61}$Polynomial
levelPolynomial
level$b_{3}$$b_{2}$$b_{1}$$b_{2}$$b_{2}$$b_{2}$$b_{1}$$b_{1}$$b_{1}$$b_{3}$$b_{3}$$b_{3}$
Figure 7:  Three DetachLink were applied in the ambient r-DagProof
$\mathcal{D}$ of fig. 6

We remember that $r_{\mathcal{C}}$ is the root of the r-DagProof $\mathcal{C}$
and $Starts(\mathcal{C})$ is the set of initials of $\mathcal{C}$ as stated by
definition 11

We observe that the resulting (pre) r-DagProof yielded from the collapse in
level $\mu$ can be bigger than $m^{p}$ yet. With the collapse of $m^{p-3}$
sub-proofs/derivations, the size of the resulting r-DagProof is at least
$\frac{\left|\mathcal{D}\right|}{\left|\mathcal{C}\right|\times m^{p-3}}$. If
the mentioned size of the resulting r-DagProof is bigger than $m^{p}$, then
there must be two main reasons: (1) The collapsed sub-proof/derivation is
bigger then $m^{p}$ by itself, or; (2) There must be more matrices in level
$\mu$ that we consider. The second alternative dealt proceeds by collapsing
all instances of all matrices occurring at the lowest level. This is addressed
in lines 3 to 11 of algorithm 2. For the first alternative, we only have to
recursively find more redundant parts in the sub-proof/derivation that must
exist by theorem 7 in the matrix that had all instances collapsed in the
ambient r-DagProof. Since theorem 7 works on EmND proofs, as opposed to
derivations with open assumptions, we need lemma 10 below.

######  Lemma 10.

Let $p\in\mathbb{N}$, $p>3$, $\Pi$ be an EmND proof of a
$\mathbf{M}_{\supset}$tautology $\alpha$, such that,
$\left|\mathcal{T}(c(\Pi))\right|=m$ and $\left|\Pi\right|>m^{p}$. According
theorem 7 let $\Pi_{s}$ be a matrix that has at least $m^{p-3}$ instances
occurring in the level $\mu$ in $\Pi$. If $\left|\Pi_{s}\right|>m^{p}$ then
there is a matrix $\Pi_{s}^{\prime}$ that is a sub-derivation of $\Pi_{s}$,
such that it has at least $m^{p-3}$ instances in $\Pi_{s}$ in some, fixed,
level $\nu>\mu$.

###### Proof.

of 10. The main feature of theorem 7 is the fact that it works for EmND proofs
and $\Pi_{s}$ does not need to be a proof, it is instead a derivation with
open assumptions. We can discharge in the correct order, dictated by the
syntax tree of $\alpha$ and the mapping l that defines the EmND $\Pi_{s}$. To
do this, we restrict l to $\Pi_{s}$. This restriction does not yield an EmND
yet, and we have to consider the syntax tree of the conclusion of $\Pi_{s}$,
i.e. the syntax tree $T_{c(\Pi_{s})}$. However, as we have already said, we do
not have a tautology as the conclusion of $\Pi_{s}$. We discharge all open
assumptions in $\Pi_{s}$, obtaining a conclusion $\beta$ that is a tautology.
The result is then an EmND that proves $\beta$. The introduction part of the
main branch does not disrupt the condition o definition 5. Finally, since
$\beta$ is smaller than $\alpha$ we choose a new propositional variable
$q_{new}$ and define a new formula “$q_{new}\supset
q_{new}\supset\ldots\beta$” with as many $q_{new}$ repetitions as it is enough
to have a formula of the same size as $\alpha$. The EmND adjusted to this new
formula is a proof of a tautology, and we can apply Theorem 7 to obtain a
matrix $\Pi_{s}^{\prime}$ that has $m^{p-3}$ instances in $\Pi_{s}$. Note that
$\left|T_{c(\Pi_{s})}\right|=\left|T_{a}\right|$. Since there is only one main
branch, the many instances of $\Pi_{s}^{\prime}$ occur above the original
conclusion of $\Pi_{s}$. Finally, the I-part of the main branch, from
$c(\Pi_{s})$ down to “$q_{new}\supset q_{new}\supset\ldots\beta$” can be
eliminated by merely deleting the introduction rules applied to draw
“$q_{new}\supset q_{new}\supset\ldots\beta$”, including the rules used to
prove $\beta$. In this way we obtain the original matrix $\Pi_{s}$ and the
desired $m^{p-3}$ instances of $\Pi_{s}^{\prime}$ that occurs in it. Finally,
as $\Pi_{s}^{\prime}$ is sub-derivation of $\Pi_{s}$ then the level $\nu$ of
its root is strictly above $\mu$.

By the proof of Lemma 10, we can see that even in the case that $\Pi_{s}$ is
not an EmND proof, if $\left|\Pi_{s}\right|>m^{p}$, with $m=c(\Pi_{s})$, then
there is a sub-derivation of $\Pi_{s}$ that it is repeated at least $m^{p-3}$
many times in $\Pi_{s}$.

######  Corollary 11.

Let $p\in\mathbb{N}$, $p>3$, $\Pi$ be an EmND derivation of $\alpha$, such
that, $\left|\mathcal{T}(c(\Pi))\right|=m$ and $\Pi_{s}$ a sub-derivation of
$\Pi$ that occurs in $\Pi$ in level $\mu$. If $\left|\Pi_{s}\right|>m^{p}$
then there is a sub-derivation $\Pi_{s}^{\prime}$ of $\Pi_{s}$ that has at
least $m^{p-3}$ instances occurring in a level $\nu>\mu$.

The above corollary 11 is used to ensure the termination and correctness of
algorithm 2 in the section 4. Algorithm 1, below, defines the operation of
collapsing a list $\mathcal{Y}$ of instances of the r-DagProof matrix
$\mathcal{C}$333We remember that a matrix that occurs in a level $\mu$ in an
r-DagProof $\mathcal{D}$ is any sub-r-DagProof of $\mathcal{D}$ that has root
in level $\mu$ and may have some other instances in level $\mu$ too occurring
in level $\mu$

######  Definition 15 (Collapse operation inside pre r-DagProofs).

Let

$\mathcal{D}=\langle
V,E_{d},E_{A},r,l,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$

be a pre r-DagProof for a $\mathbf{M}_{\supset}$ formula $\alpha$ and
$\mathcal{C}$ be a pre sub r-DagProof of $\mathcal{D}$ and $\mathcal{Y}$ the
set of roots of the instances of $\mathcal{C}$, occuring in level $\mu$ that
will be collapsed. Algorithm 1 defines and computes the result of collapsing
all instances of $\mathcal{C}$ in only one in $\mathcal{D}$.

Algorithm 1

0: $\mathcal{D}$, $\mathcal{C}$, r-DagProofs, $\mathcal{C}\prec\mathcal{D}$,
and the list $\mathcal{Y}$ containing the roots of the instances of
$\mathcal{C}$

0: a r-DagProof $\mathcal{D}^{\prime}$ having all instances of $\mathcal{C}$
collapsed in a unique r-DagProof

1: Function $Collapse(\mathcal{D},\mathcal{Y},\mathcal{C})$

2: $\mathcal{D}^{\prime}\leftarrow\mathcal{D}$

3: $j\leftarrow l_{\mathcal{C}}(root(\mathcal{C}));$

4: $i\leftarrow 1$;

5: $\mathcal{Y}\leftarrow rest(\mathcal{Y})$

6: for $k\in\mathcal{Y}$ do

7: $\mathcal{D}^{\prime}\leftarrow
DetachLink(\mathcal{C},k,\mathcal{D}^{\prime},j@i);i\leftarrow i+1$

8: end for

9: $Return\;\;\mathcal{D}$

Examining algorithm 1, we have the Lemma 12 that provides an upper-bounded for
the resulting r-DagProof after the collapses of all instances of the matrix in
the ambient r-DagProof $\mathcal{D}$.

######  Lemma 12.

$\left|\mathcal{D}^{\prime}\right|\leq\frac{\left|\mathcal{D}\right|}{length(\mathcal{Y})\times\left|\mathcal{C}\right|}$

##  4 r-Dags as succinct certificates for $\mathbf{M}_{\supset}$ tautologies

In this section, we show how to use the Collapse operation defined in previous
section 3. Algorithm 2 defines the operation of compression that collapses all
redundancies that occur in any huge EmND proof. In line 3 the function
$Lemma\ref{lemma:ListForCollapse}(\mathcal{T}))$ returns the set of
independent matrices in $\mathcal{T}$ that exists by Lemma 9. Since it is an
independent set, by collapsing all of its instances in only one instance to
each matrix, we do not need to collapse the upper levels that are not local
lowest levels, the roots of the matrices’ elements in the independent set.

Algorithm 2 Compress an EmND proof $\mathcal{T}$ using corol.

0: Uses the global variable $m$ with value $\left|c(\mathcal{T})\right|$

0: $3<p\in\mathbb{N}$, $\mathcal{T}$ is a EmND,
$h(T)\leq\left|c(\mathcal{T})\right|$

0: a r-DagProof $\mathcal{D}$ proving $c(\mathcal{T})$ of size smaller than
$\left|c(\mathcal{T})\right|^{p-3}$

1: Function Compress($\mathcal{T},p$)

2: if ($m^{p}<\left|\mathcal{T}\right|)$ then

3: $LocalLowestLevels\leftarrow MinLevel(Lemma\leavevmode\nobreak\
\ref{lemma:ListForCollapse}(\mathcal{T}))$

4: $\mathcal{D}\leftarrow\mathcal{T}$

5: for $lev\in LocalLowestLevels$ upwards $h(\mathcal{T})$ do

6: $L\leftarrow SuperPolySubProofs(\mathcal{T},lev)$

7: for $\langle\mathcal{Y},\mathcal{C}_{\mathcal{Y}}\rangle\in L$ do

8: $\mathcal{D}_{\mathcal{Y}}\leftarrow Compress(\mathcal{C}_{\mathcal{Y}},p)$

9: $\mathcal{D}\leftarrow Collapse(\mathcal{D},\mathcal{Y},D_{\mathcal{Y}})$

10: end for

11: end for

12: $Return\mathcal{D}$

13: else

14: $Return\mathcal{T}$

15: end if

Below we have some lemmas that are proved easily by inspecting the code of
algorithms 1, 2 and definition 13.

######  Lemma 13.

In algorithm 2 above, the number of recursive calls after an initial
invocation of $Compress(\mathcal{T},p)$, with $m=\left|c(\mathcal{T})\right|$,
is at most $\left|\mathcal{T}\right|$.

###### Proof.

Since $m^{p}$ is constant during all the recursive calls, and the size of the
first argument of $Compress$ is strictly smaller than each previous recursive
call. Thus, there must be a call such that $\left|\mathcal{T}\right|<m^{p}$.
When $\mathcal{T}$ is of this size, it is the recursive basis case, anyway.
Taking the (worst) case into account, the number of recursive calls is upper-
bounded by the size of the EmND $\mathcal{T}$ itself. If any recursive call,
on the first argument $\mathcal{T}_{1}$, is such that
$\left|\mathcal{T}_{1}\right|>m^{p}$, then it obtains the sub-derivations that
occurs at least $m^{p-3}$, collapsing $Compress(\mathcal{T}_{1})$ into a
unique compressed version of $\mathcal{T}_{1}$. This is done with lesser than
$\left|\mathcal{T}\right|$ recursive calls. In fact, there is at least
$m^{p-3}$ collapses, so the total amount of recursive calls is at most
$\frac{\left|\mathcal{T}\right|}{\left|\mathcal{T}_{1}\right|\times m^{p}}$.
Lastly, the compression of $\mathcal{T}_{1}$ is obtained in a unique call to
$Compress$.

Below we find a useful Lemma used to prove that after the compression any
linear height bounded EmND super-polynomially bounded proof becomes polynomial
in size.

######  Definition 16.

Given a EmND linearly hight bounded proof $\mathcal{T}$, such that,
$\left|\mathcal{T}\right|>\left|\alpha\right|^{p}$, $p\geq 3$. We denote by
$LRI(\mathcal{T})$444$LRI$ is an acronym to $LowestInstancesRedundant$ the
list of all lowest instances that occur at least $m^{p-3}$ times, for each of
the matrices, as provided by Lemma 9.

######  Definition 17 (EmND proofs difference operation).

Let $\mathcal{T}$ and $\mathcal{T}_{1}$ EmND derivations, such that,
$\mathcal{T}_{1}$ is sub-derivation of $\mathcal{T}$ occuring in level $\nu$.
The difference derivation $\mathcal{T}^{\prime}=\mathcal{T}-\mathcal{T}_{1}$
obtains by removing all nodes of $\mathcal{T}_{1}$ from $\mathcal{T}$, but
$c(\mathcal{T}_{1})$. Morevore, $l_{\mathcal{T}^{\prime}}$ is the restriction
of $l_{\mathcal{T}}$ to this $\mathcal{T}^{\prime}$ new derivation.

######  Definition 18 (EmND proof difference with removal of conclusion).

Let $\mathcal{T}$ and $\mathcal{T}_{1}$ EmND derivations, such that,
$\mathcal{T}_{1}$ is sub-derivation of $\mathcal{T}$ occuring in level $\nu$.
The greedy difference $\mathcal{T}\ominus\mathcal{T}_{1}$ is as in defintion
17 extended with the removal of the conclusion of $\mathcal{T}_{1}$ from the
yielded sub-derivation.

The difference of $\mathcal{T}$ and the set of derivations $S$ is the
iterating the difference of $\mathcal{T}$ to each member of $S$.

The following Lemma 16 shows that for every proof of size bigger than $m^{p}$,
when removing its redundant part, that exists in virtue of Theorem 7, what
remains is a rDagProof of size less than $m^{p}$.

We remember that derivations formally are labeled trees, and the later are
graphs. The differnce between graphs is well-defined as defined by definition
17

We need a preparatory lemma that is, in a certain sense, a generalization of
Lemma 10.

We use $\left(\begin{array}[]{c}\gamma_{1}\\\ \vdots\\\
\gamma_{n}\end{array}\right)\supset\alpha$ to denote the formula
$\gamma_{1}\supset(\gamma_{2}\supset(\ldots\supset\alpha)\ldots)$.

######  Lemma 14 (Redundancy Lemma for Normal derivations).

Let $\Pi$ be a normal and expanded derivation in N.D. for $M_{\supset}$. Let
$\Gamma=\\{\gamma_{1},\ldots,\gamma_{n}\\}$ be the set of all open assumptions
in $\Pi$ and $\alpha$ the conclusion of $\Pi$,
$m=\left|\alpha\right|+\sum_{\gamma\in\Gamma}\left|\gamma\right|$. If
$\left|\Pi\right|>m^{p}$, for some $p>3$, then there is a sub-derivation
$\Pi_{s}$ of $\Pi$ and a level $\mu$ from $\Pi$, such that, there are at least
$m^{p-3}$ instances of $\Pi_{s}$ occurring in level $\mu$.

###### Proof.

From $\Pi$ we obtain an expanded normal proof $\Pi^{\prime}$ of
$\left(\begin{array}[]{c}\gamma_{1}\\\ \vdots\\\
\gamma_{n}\end{array}\right)\supset\alpha$ by applying a series $\supset$-I
rules in the main branch of $\Pi$, discharging all open assumptions in $\Pi$.
From the parsing tree of $\left(\begin{array}[]{c}\gamma_{1}\\\ \vdots\\\
\gamma_{n}\end{array}\right)\supset\alpha$ and an adequate partial map from
formula occurrences in $\Pi^{\prime}$ to this parsing tree we obtain an EmND
proof of $\left(\begin{array}[]{c}\gamma_{1}\\\ \vdots\\\
\gamma_{n}\end{array}\right)\supset\alpha$. Note that any adequate mapping
produces an EmND proof of the later formula. We apply Lemma 7 to
$\Pi^{\prime}$ concluding that there is a level $\mu$ from $\Pi^{\prime}$ and
a sub-derivation $\Pi_{s}$ of $\Pi^{\prime}$, such that, there are at least
$m^{p-3}$ instances of $\Pi_{s}$ occurring in level $\mu$ in $\Pi^{\prime}$.
Finally, we rebuild the orginal derivation $\Pi$ by removing all $\supset$-I
applications used to construct $\Pi^{\prime}$ from $\Pi$. We reach the desire
conclusion, i.e., there is a level $\mu$ from $\Pi$ and a sub-derivation
$\Pi_{s}$ of $\Pi$, such that, there are at least $m^{p-3}$ instances of
$\Pi_{s}$ occurring in level $\mu$ in $\Pi$

Other very useful lemma is the following. It is inspired in the huge proofs,
based on Fibonacci numbers, shown in [SuperExp] in its appendix.

######  Lemma 15.

Let $\beta$ be a $M_{\supset}$ formula. There is a family
$(\Pi^{fib}_{n})_{n\in\mathbb{N}})$ of $M_{\supset}$ N.D. derivations of
$\beta$ from a set of formulas $\Delta_{n}$, of linear size on $n$ and
$\left|\beta\right|$. If
$m=\left|\beta\right|+\sum_{\delta\in\Delta_{n}}\left|\delta\right|$ then, for
each $n\in\mathbb{N}$, $\Pi^{fib}_{n}$ is a Normal and expanded derivation of
height $\mathcal{O}(4\times n\times\left|\beta\right|)$ and size lower-bounded
by $\frac{\phi^{\left|\beta\right|\times n}}{\sqrt{5}}$, where $\phi\approx
1.618$ is the golden ratio.

###### Proof.

In [13], section 4, we show a family of Natural Deduction $M_{\supset}$
derivations of $p_{1}\supset p_{n}$, from $\Delta_{n}=\\{p_{1},p_{1}\supset
p_{2}\\}\cup\\{p_{i}\supset(p_{i+1}\supset p_{i+2}):i\leq n-2\\}$ of height
$n$ and size $\frac{\phi^{n}}{\sqrt{5}}$. We modify this family to have
$p_{n}=\beta$, getting the statement of the lemma.

######  Lemma 16.

For any EmND proof $\mathcal{T}$ of a tautology $\alpha$ and $p>3$, if
$\left|\mathcal{T}\right|\geq\left|\alpha\right|^{p}$ and
$\langle\mathcal{T}_{1},\ldots,\mathcal{T}_{n}\rangle=LRI(\mathcal{T})$, then

$\left|\mathcal{T}\ominus\bigcup_{i=1\ldots n}\mathcal{T}_{i}\right|<m^{p}$

###### Proof.

We can consider $\mathcal{T}$ as shown in figure 8, where $\ell\times
m^{p-3}\leq n$, and $\ell$ is the number of different levels that have sub-
derivations occurring at least $m^{p-3}$ in them. We remember that the
formulas $\beta_{i}$, $i=1\ldots n$ may occur in different levels. For each
$j=1\ldots\ell$ there are at least $m^{p-3}$ occurrences of instances of a
sub-derivation $\mathcal{T}_{j}$ in level $j$ in $\mathcal{T}$. To facilitate
the understanding we re-index the instances with the level $j$, such that,
$\mathcal{T}_{j_{i}}^{j}$ is the $i$-th instance of the matrix
$\mathcal{M}_{j}$ occurring in level $j$ in $\mathcal{T}$. We remember that
there are $\ell$ matrices indicating $\ell$ redundant parts in $\mathcal{T}$.

$\mathcal{T}_{1}^{\mu_{1}}$ $\beta_{1}^{\mu_{1}}$ $\delta_{1}^{\mu_{1}}$
$\Pi_{1}^{\mu_{1}}$ $\beta_{1}^{\mu_{1}}\supset\gamma_{1}^{\mu_{1}}$
$\gamma_{1}^{\mu_{1}}$ $\ldots$ $\mathcal{T}_{1}^{\mu_{\ell}}$
$\beta_{1}^{\mu_{\ell}}$ $\delta_{1}^{\mu_{\ell}}$ $\Pi_{1}^{\mu_{\ell}}$
$\beta_{1}^{\mu_{\ell}}\supset\gamma_{1}^{\mu_{\ell}}$
$\gamma_{1}^{\mu_{\ell}}$ $\Pi$ $q$ $\vdots$ $\alpha$

Figure 8: The proof $\mathcal{T}$ in Lemma 16

We prove by induction on the number of different lowest levels, i.e, on $\ell$
that

$\left|\mathcal{T}_{0}\right|=\left|\mathcal{T}\ominus\bigcup_{i=1\ldots
n}\mathcal{T}_{i}\right|<m^{p}$

Induction on $\ell$:

  1. Basis

There is only one level $\mu$ and one matrix $\mathcal{T}_{\mu}$, hence
$\ell=1$, that is repeated at least $m^{p-3}$ times in level $\mu$ in
$\mathcal{T}$. Let $\mathcal{T}_{0}=\mathcal{T}\ominus\bigcup_{i=1\ldots
n}\mathcal{T}_{i}$, where $\mathcal{T}_{i}^{\mu_{i}}$ are all the instances of
$\mathcal{T}_{\mu}$, for all $i=1\ldots n$. We notice that $\mathcal{T}_{0}$
is not a derivation anymore, it is only a tree, depicted in figure 9.

$\delta_{1}^{\mu_{1}}$ $\Pi_{1}^{\mu_{1}}$
$\beta_{1}^{\mu_{1}}\supset\gamma_{1}^{\mu_{1}}$ $\gamma_{1}^{\mu_{1}}$
$\ldots$ $\delta_{n}^{\mu_{1}}$ $\Pi_{n}^{\mu_{1}}$
$\beta_{n}^{\mu_{1}}\supset\gamma_{n}^{\mu_{1}}$ $\gamma_{n}^{\mu_{1}}$ $\Pi$
$q$ $\vdots$ $\alpha$

Figure 9: The tree $\mathcal{T}_{0}$

Let us suppose that:

$\left|\mathcal{T}_{0}\right|=\left|\mathcal{T}\ominus\bigcup_{i=1\ldots
n}\mathcal{T}_{i}\right|\geq m^{p}$

We observe that by Lemma 14, for each $i$,
$\left|\Pi_{i}^{\mu_{i}}\right|<m^{p}$ and $\left|\Pi\right|<m^{p}$. If any of
these derivations were bigger than $m^{p}$ there would be a matrix occurring
at least $m^{p-3}$ in some level of them. The only instances that occur at
least $m^{p-3}$ in $\mathcal{T}$ are $\mathcal{T}_{i}$, $i=1,\ldots,n$ by
hypotheses. They occur in level $\mu$, contradicting the above assumptions on
the size of the derivations $\Pi_{i}^{\mu_{i}}$ and $\Pi$. We note that
$\left|\mathcal{T}_{0}\right|=\left|\Pi\right|+\sum_{i=1,n}\left|\Pi_{i}^{\mu_{i}}\right|\geq
m^{p}$ and, by previous observation on the size of each of the summands, there
must be a sub-sequence $(\Pi_{r_{i}}^{\mu_{1}})_{i=1,r}$ of the sequence
$(\Pi_{i}^{\mu_{1}})_{i=1,n}$ of derivations, such that,
$\left|\Pi\right|+\sum_{i=1,r}\left|\Pi_{r_{i}}^{\mu_{1}}\right|\geq m^{p}$.
We have to consider two cases:

Proper

We have that $r<m^{p-3}$. So, we build the derivation $\mathcal{T}_{0}^{++}$
in figure 10, by re-introducing in $\mathcal{T}_{0}$ the respective minor
premiss $\beta_{r_{i}}^{\mu_{1}}$ for each $\Pi_{r_{i}}^{\mu_{1}}$ derivation
of the major premiss $\beta_{r_{i}}^{\mu_{1}}\supset\gamma_{r_{i}}^{\mu_{1}}$.
Moreover, the other derivations $\Pi_{i}^{\mu_{1}}$ not in the sub-sequence
$(\Pi_{r_{i}}^{\mu_{1}})_{i=1,r}$ are erased from $\mathcal{T}_{0}$. We re-
inforce the observation that all $\beta_{i}^{\mu_{1}}$ are the same
formula.Moreover, we delete the $I-part$ of the main branch of $\mathcal{T}$
that occurs in $\mathcal{T}_{0}^{++}$. This is the final derivation
$\mathcal{T}_{0}^{++}$ show in the figure 10. $q$ is the minimal formula of
the main branch.

$\gamma_{1}^{\mu_{1}}\;\;\ldots$ $\beta_{r_{1}}^{\mu_{1}}$
$\delta_{r_{1}}^{\mu_{1}}$ $\Pi_{r_{1}}^{\mu_{1}}$
$\beta_{r_{1}}^{\mu_{1}}\supset\gamma_{r_{1}}^{\mu_{1}}$
$\gamma_{r_{1}}^{\mu_{1}}$ $\ldots\;\;\gamma_{i}^{\mu_{1}}\;\;\ldots$
$\beta_{r_{r}}^{\mu_{1}}$ $\delta_{r_{r}}^{\mu_{1}}$ $\Pi_{r_{r}}^{\mu_{1}}$
$\beta_{r_{r}}^{\mu_{1}}\supset\gamma_{r_{r}}^{\mu_{1}}$
$\gamma_{r_{r}}^{\mu_{1}}$ $\ldots\;\;\gamma_{n}^{\mu_{1}}$ $\Pi$ $q$

Figure 10: The derivation $\mathcal{T}_{0}^{++}$

We must observe that $\mathcal{T}_{0}^{++}$ is a valid derivation bigger than
$m^{p}$, thus by Lemma 14 there is a level $\nu$, such that, there are at
least $m^{p-3}$ instances of the matrix $\mathcal{M}$. We have a
contradiction.

     * •

If $\nu>\mu$ then there is at least $m^{p-3}$ instances of a derivation in a
level that exists in all the sub-derivations
$(\Pi_{r_{i}}^{\mu_{1}})_{i=1,r}$. Replacing back all the instances
$\mathcal{T}_{i}$, $i=1,n$, we obtain $\mathcal{T}$ and a proof that it has
another level, besides $\mu$, that has at least $m^{p-3}$ repeated instances
of the same matrix. We have a contradiction.

     * •

If $\nu=\mu$, since $\beta=\beta_{i}^{\mu_{1}}$, for each $i$, occurs less
than $m^{p-3}$ in level $\mu$, then there must be other instances than
$\mathcal{T}_{i}$ occurring at least $m^{p-3}$ in $\mathcal{T}$ in $\mu$. We
have a contradiction, when we replace back the derivations $\mathcal{T}_{i}$,
for there will be more than one matrix with at least $m^{p-3}$ repeated
occurrences in level $\mu=\nu$.

     * •

If $\nu<\mu$ we have a contradiction, by a reasoning analogous to the previous
item.

Improper

We have that $m^{p-3}\leq r$. So, we build the derivation
$\mathcal{T}_{0}^{+++}$ in figure 11, by re-introducing in $\mathcal{T}_{0}$
the respective minor premiss $\beta$ as in $\mathcal{T}_{0}^{++}$, but only
from $r_{1}$ to $r_{m^{p-3}}$. Moreover, for each $i=m^{p-3}+1,\ldots,r$ we
remove $\Pi_{r_{i}}^{\mu}$ from $\mathcal{T}_{0}$ and replace
$\beta_{i-m^{p-3}}^{\mu}$, the derivation of the minor premiss of the
$\supset$-Elim rule by the smallest derivation of the form stated by Lemma 15
that is bigger than $\left|\Pi_{r_{i}}^{\mu}\right|$. We denote by
$\Sigma_{\Pi_{r_{i}}^{\mu}}$ this derivation. Note that the size of
$\Sigma_{\Pi_{r_{i}}^{\mu}}$ compensates the removal of $\Pi_{i}^{\mu_{1}}$,
for every $i=m^{p-3}+1$ to $i=r$. It is important to note that the height of
$\Sigma_{r_{i}}^{\mu}$ is linear on $m$, so it is $\mathcal{T}_{0}^{+++}$.
From $i=r+1$ to $i=n$ there is only a simply removal of
$\Pi_{r_{i}}^{\mu_{1}}$, without any compensation. At the end the size of
$\mathcal{T}_{0}^{+++}$ is bigger than $m^{p}$ and there is less than
$m^{p-3}$ occurrences of $\beta$ in the level $\mu_{1}=\mu$. Thus, by an
analysis similar to the above case, with the application of Lemma 14, we
obtain a contradiction. We observe that we introduced a linear number of
assumptions in the Lemma 15. We notice that we reason in terms of the big-O
notation, thus we have that $\mathcal{T}_{0}^{+++}$ is bigger than $m^{p}$, in
terms of $m$.

$\gamma_{1}^{\mu_{1}}\;\;\ldots$ $\Sigma_{r_{1}}^{\mu_{1}}$
$\beta_{r_{1}}^{\mu_{1}}$ $\delta_{r_{1}}^{\mu_{1}}$ $\Pi_{r_{1}}^{\mu_{1}}$
$\beta_{r_{1}}^{\mu_{1}}\supset\gamma_{r_{1}}^{\mu_{1}}$
$\gamma_{r_{1}}^{\mu_{1}}$ $\ldots\;\;\gamma_{i}^{\mu_{1}}\;\;\ldots$
$\beta_{r_{r}}^{\mu_{1}}$ $\delta_{r_{r}}^{\mu_{1}}$ $\Pi_{r_{r}}^{\mu_{1}}$
$\beta_{r_{r}}^{\mu_{1}}\supset\gamma_{r_{r}}^{\mu_{1}}$
$\gamma_{r_{r}}^{\mu_{1}}$ $\ldots\;\;\gamma_{n}^{\mu_{1}}$ $\Pi$ $q$

Figure 11: The derivation $\mathcal{T}_{0}^{+++}$

  2. Inductive Step

In this case we have $\ell>1$ levels with repetitions of the respective sub-
derivations at least $m^{p-3}$. We analyse the highest level of repetitions in
a similar way that was done in the basis step, with the hypothesis that the
removal of all repetitions in the lowest $\ell-1$ levels result in a tree of
size lesser than $m^{p}$. With this inductive hypothesis and the reasonning on
the repetitions removal in the highest level we reach the desired conclusion.

######  Lemma 17.

For any EmND proof $\mathcal{T}$ of a tautology $\alpha$ and $p>3$, if
$\left|\mathcal{T}\right|\geq\left|\alpha\right|^{p}$ then
$\left|Compress(\mathcal{T},p)\right|<\left|\alpha\right|^{p}$

###### Proof.

We prove by induction on the number of recursive calls that
$\left|Compress(\mathcal{T},p)\right|<\left|\alpha\right|^{p}$, for in lemma
13 we have already proven that the algorithm stops for any valid input pair
$\langle\mathcal{T},p\rangle$.

  * •

Basis No recursive call: In this case we already have
$\left|Compress(\mathcal{T},p)\right|<\left|\alpha\right|^{p}$. The “else” of
the “if” in line 2 of algorithm 2 is used.

  * •

I.H. Suppose $\left|\mathcal{T}\right|\geq\left|\alpha\right|^{p}$ holds.
Thus, a call to $Lemma\leavevmode\nobreak\
\ref{lemma:ListForCollapse}(\mathcal{T})$, in line 3 return the list of all
occurrences of sub-derivations, instances of the independent set of matrices
given by Lemma 9, that occurs more than $m^{p-3}$ in the lowest levels of
$\mathcal{T}$. By inductive hypothesis, there is less one recursive call,
$Compress(\mathcal{T}_{i})$ of each instance $\mathcal{T}_{i}$ of the list
returns a r-Dag of size less than $\left|\alpha\right|^{p}$. By Lemma 16 the
part of $\mathcal{T}$ that it is not collapsed is less than
$\left|\alpha\right|^{p}$ and by Lemma 12 we obtain that
$\left|Compress(\mathcal{T},p)\right|<\left|\alpha\right|^{p}$.

The above upper-bound is not tight. A tighter one obtains by counting the
number of matrices for each level, according to Theorem 7 and corollary 11.
However, in this article, we do not need a tighter upper-bound than what we
state in lemma 13.

##  5 Checking r-DagProofs in Polynomial Time

The following definitions are central in proving that r-DagProofs are
certificates for $\mathbf{M}_{\supset}$ formulas validity. Let $\mathcal{C}$ =
$\langle V,E_{d},E_{A},r,l,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$ be a pre
r-DagProof of $\alpha$ from $\mathbf{M}_{\supset}$. We associate to each $v\in
V$ an entailment relation. The entailment represents the logical consequency
relation carried within $\mathcal{C}$ from the DAG’s leaves downwards until
$v$. Due to the collapse operation, and the many downward detours that the
collapses introduce, we use an environment function that keeps track of the
entailment relation related to each detour. We use the notation $Emt(\alpha)$
to denote the set $\\{\Delta\vdash\beta:\mbox{$\Delta\subseteq Sub(\alpha)$
and $\beta\in Sub(\alpha)$}\\}$ of all possible entailments between sets of
(sub)formulas of $\alpha$, $\Delta$, and (sub)formulas of $\alpha$.

######  Definition 19.

Let $\Delta\vdash\delta\in Emt(\alpha)$, and $\mathcal{O}$ be a total order on
the subformulas of $alpha$. We define
$Ant_{\mathcal{O}}(\Delta\vdash\delta)=b_{\mathcal{O}}(\Delta)$.

In what follows, consider a pre r-DagProof $\mathcal{C}$ = $\langle
V,E_{d},E_{A},r,\ell,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$ of $\alpha$. A
node $v\in V$ is called a deductive leaf, iff, it has no incoming deductive
edge, otherwise we call it as deductive (internal) node. The nodes of
$\mathcal{C}$ that have mode than one different Deductive Edges outcoming from
it are called divergent node.

######  Definition 20 (Local Entailment).

Given a pre r-DagProof $\mathcal{C}$ = $\langle
V,E_{d},E_{A},r,\ell,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$ of $\alpha$,
we define the mapping
$M_{\vdash}^{\mathcal{C}}:V\times\mathbb{N}\longrightarrow
Emt(\alpha)\cup\\{^{\prime}\vdash^{\prime}\\}$, for each $v\in V$ recursively
as follows:

Deductive Leaf, no Ancestrality

If $v\in V$ and, there is no $u\in V$, such that $\langle u,v\rangle\in E_{d}$
and, there is no $w\in V$, such that $\langle w,v\rangle\in E_{A}$ then
$M_{\vdash}^{\mathcal{C}}(v,0)=\\{\ell(v)\\}\vdash\ell(v)$, and
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$, for
$j\in\mathbb{N}$, $j\neq 0$, and;

Deductive Leaf with Ancestrality

If $v\in V$ and, there is no $u\in V$, such that $\langle u,v\rangle\in E_{d}$
and, there is $w\in V$, such that $\langle w,v\rangle\in E_{A}$ then
$M_{\vdash}^{\mathcal{C}}(v,i)=\\{\ell(v)\\}\vdash\ell(v)$, for each $i$, such
that there is $\langle w,v\rangle\in E_{A}$ with $\delta(\langle
w,v\rangle)=i$, and $M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$,
for every $j\in\mathbb{N}$, such that, there is no $\langle w,v\rangle\in
E_{A}$ with $\delta(\langle w,v\rangle)=j$, and;

Deductive Internal Node, no Ancestrality

If $v\in V$ and, there is $u\in V$, such that $\langle u,v\rangle\in E_{d}$
and, there is no $w\in V$, such that $\langle w,v\rangle\in E_{A}$ then we
have two cases:

  1. 1.

There are only two $u_{1},u_{2}\in V$, such that, $\langle u_{i},v\rangle\in
E_{d}$, for $i=1,2$, $\ell(u_{1})=\delta_{1}$,
$\ell(u_{2})=\delta_{1}\supset\delta_{2}$ and, $\ell(v)=\delta_{2}$. Moreover,
let
$I_{i}=\\{j:M_{\vdash}^{\mathcal{C}}(u_{i},j)\neq^{\prime}\vdash^{\prime}\\}$.
Thus, we have that:

If

$I_{1}=I_{2}$ then for every $j\in I_{1}=I_{2}$, we have that:

$M_{\vdash}^{\mathcal{C}}(v,j)=\left\\{\begin{array}[]{ll}\Delta_{1}\cup\Delta_{2}\vdash\delta_{2}&\mbox{if
$M_{\vdash}^{\mathcal{C}}(u_{i},j)=\Delta_{i}\vdash\ell(u_{i})$}\\\
{}^{\prime}\vdash^{\prime}&\mbox{otherwise}\end{array}\right.$

, and every $j\in\mathbb{N}-(I_{1}\cup I_{2})$,
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$. Moreover, if
$L(\langle u_{i},v\rangle)\downarrow$, $i=1,2$, then $L(\langle
u_{i},v\rangle)=Ant_{\mathcal{O}_{\alpha}}(M_{\vdash}^{\mathcal{C}}(u_{i}))$,
and;

If

$I_{1}\neq I_{2}$ then for every $j\in\mathbb{N}$,
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$

  2. 2.

There is only one $u\in V$, such that, $\langle u,v\rangle\in E_{d}$,
$\ell(u)=\delta_{2}$ and $\ell(v)=\delta_{1}\supset\delta_{2}$. Moreover, let
$I=\\{j:M_{\vdash}^{\mathcal{C}}(u,j)\neq^{\prime}\vdash^{\prime}\\}$. If
$I\neq\emptyset$, and hence, for every $j\in I$, we have that:

$M_{\vdash}^{\mathcal{C}}(v,j)=\left\\{\begin{array}[]{ll}\Delta-\\{\delta_{1}\\}\vdash\delta_{1}\supset\delta_{2}&\mbox{if
$M_{\vdash}^{\mathcal{C}}(u,j)=\Delta\vdash\ell(u)$ and
$\ell(u)=\delta_{2}$}\\\
{}^{\prime}\vdash^{\prime}&\mbox{otherwise}\end{array}\right.$

, and every $j\in\mathbb{N}-I$,
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$, and; For every
$j\in\mathbb{N}$, $M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$.
Moreover, if $L(\langle u,v\rangle)\downarrow$ then $L(\langle
u,v\rangle)=Ant_{\mathcal{O}_{\alpha}}^{\mathcal{C}}(M_{\vdash}(u))$. If
$I=\emptyset$ then $M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$,
for every $j\in\mathbb{N}$.

Deductive Internal Node with Ancestrality

If $v\in V$ and, there is $u\in V$, such that $\langle u,v\rangle\in E_{d}$
and, there is $w\in V$, such that $\langle w,v\rangle\in E_{A}$ then we have
two cases:

  1. 1.

There are only two $u_{1},u_{2}\in V$, such that, $\langle u_{i},v\rangle\in
E_{d}$, for $i=1,2$, $\ell(u_{1})=\delta_{1}$,
$\ell(u_{2})=\delta_{1}\supset\delta_{2}$ and, $\ell(v)=\delta_{2}$. Moreover,
let
$I_{i}=\\{j:M_{\vdash}^{\mathcal{C}}(u_{i},j)\neq^{\prime}\vdash^{\prime}\\}$.
Thus, we have that:

If

$I_{1}=I_{2}$ then for every $j\in I_{1}=I_{2}$, we have that:

$M_{\vdash}^{\mathcal{C}}(v,j)=\left\\{\begin{array}[]{ll}\Delta_{1}\cup\Delta_{2}\vdash\delta_{2}&\mbox{if
$M_{\vdash}^{\mathcal{C}}(u_{i},j)=\Delta_{i}\vdash\ell(u_{i})$}\\\
{}^{\prime}\vdash^{\prime}&\mbox{otherwise}\end{array}\right.$

, and every $j\in\mathbb{N}-(I_{1}\cup I_{2})$,
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$, and;

If

$I_{1}\neq I_{2}$ then for every $j\in\mathbb{N}$,
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$

  2. 2.

There is only one $u\in V$, such that, $\langle u,v\rangle\in E_{d}$,
$\ell(u)=\delta_{2}$ and $\ell(v)=\delta_{1}\supset\delta_{2}$. Moreover, let
$I=\\{j:M_{\vdash}^{\mathcal{C}}(u,j)\neq^{\prime}\vdash^{\prime}\\}$. If
$I\neq\emptyset$, and hence, for every $j\in I$, we have that:

$M_{\vdash}^{\mathcal{C}}(v,j)=\left\\{\begin{array}[]{ll}\Delta-\\{\delta_{1}\\}\vdash\delta_{1}\supset\delta_{2}&\mbox{if
$M_{\vdash}^{\mathcal{C}}(u,j)=\Delta\vdash\ell(u)$ and
$\ell(u)=\delta_{2}$}\\\
{}^{\prime}\vdash^{\prime}&\mbox{otherwise}\end{array}\right.$

, and every $j\in\mathbb{N}-I$,
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$, and; For every
$j\in\mathbb{N}$, $M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$. If
$I=\emptyset$ then $M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$,
for every $j\in\mathbb{N}$.

Divergent Deductive Internal Node

In this case $v$ should not be the target of an ancestrality edge, otherwise
$\mathcal{C}$ is not a valid pre rDagProof and
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$, for every
$j\in\mathbb{N}$. Moreover, the set $S=\\{\langle w:\mbox{$\langle
v,w\rangle\in E_{d}$}\\}$ has at least two nodes555This is just the case for
divergent deductive nodes. We have two cases to consider:

  1. 1.

There are only two $u_{1},u_{2}\in V$, such that, $\langle u_{i},v\rangle\in
E_{d}$, for $i=1,2$, $\ell(u_{1})=\delta_{1}$,
$\ell(u_{2})=\delta_{1}\supset\delta_{2}$ and, $\ell(v)=\delta_{2}$. Moreover,
let
$I_{i}=\\{j:M_{\vdash}^{\mathcal{C}}(u_{i},j)\neq^{\prime}\vdash^{\prime}\\}$
and $T=\\{\rho(\langle v,w\rangle):w\in S\\}$. Thus, we have that:

If

$I_{1}=I_{2}=I$ then for every $j\in I_{1}=I_{2}=T$, we have that:

$M_{\vdash}^{\mathcal{C}}(v,j)=\left\\{\begin{array}[]{ll}\Delta_{1}\cup\Delta_{2}\vdash\delta_{2}&\mbox{if
$M_{\vdash}^{\mathcal{C}}(u_{i},j)=\Delta_{i}\vdash\ell(u_{i})$}\\\
{}^{\prime}\vdash^{\prime}&\mbox{otherwise}\end{array}\right.$

, and every $j\in\mathbb{N}-(I_{1}\cup I_{2})$,
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$, and;

If

$I_{1}\neq I_{2}$ or $I_{i}\neq T$, $i=1$ or $i=2$ then for every
$j\in\mathbb{N}$, $M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$

  2. 2.

There is only one $u\in V$, such that, $\langle u,v\rangle\in E_{d}$,
$\ell(u)=\delta_{2}$ and $\ell(v)=\delta_{1}\supset\delta_{2}$. Moreover, let
$I=\\{j:M_{\vdash}^{\mathcal{C}}(u,j)\neq^{\prime}\vdash^{\prime}\\}$,
$T=\\{\rho(\langle v,w\rangle):w\in S\\}$. If $T=I\neq\emptyset$ then for
every $j\in I$, we have that:

$M_{\vdash}^{\mathcal{C}}(v,j)=\left\\{\begin{array}[]{ll}\Delta-\\{\delta_{1}\\}\vdash\delta_{1}\supset\delta_{2}&\mbox{if
$M_{\vdash}^{\mathcal{C}}(u,j)=\Delta\vdash\ell(u)$ and
$\ell(u)=\delta_{2}$}\\\
{}^{\prime}\vdash^{\prime}&\mbox{otherwise}\end{array}\right.$

, and every $j\in\mathbb{N}-I$,
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$, and; For every
$j\in\mathbb{N}$, $M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$.
Moreover, if $L(\langle u,v\rangle)\downarrow$ then $L(\langle
u,v\rangle)=Ant_{\mathcal{O}_{\alpha}}(M_{\vdash}(u))$. If $I=\emptyset$ then
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$, for every
$j\in\mathbb{N}$.

Target of Divergent Deductive Internal Node

In this case $v$ is such that there is a divergent deductive node $u$ with
$\langle u,v\rangle\in E_{d}$ and $\rho(\langle u,v\rangle)$ is defined. Thus,
we have two cases:

$v$ is not target of an ancestrality edge

$M_{\vdash}^{\mathcal{C}}(v,0)=M_{\vdash}^{\mathcal{C}}(u,\rho((\langle
u,v\rangle)$ and $M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$, for
every $j\neq 0$;

$v$ is target of an ancestrality edge

There is $\langle w,v\rangle\in E_{A}$. Hence we set
$M_{\vdash}^{\mathcal{C}}(v,\delta(\langle
w,v\rangle))=M_{\vdash}^{\mathcal{C}}(u,\rho(\langle u,v\rangle)$ and
$M_{\vdash}^{\mathcal{C}}(v,j)=^{\prime}\vdash^{\prime}$, for every
$j\neq\delta(\langle w,v\rangle)$;

Obs: In what follows, sometimes we use the notation $M_{\vdash}(v,i)$ instead
of $M_{\vdash}^{\mathcal{C}}(v,i)$, whenever $\mathcal{C}$ can be easily
infered from the context.

A full subgraph of a graph $A=\langle V_{A},E_{A}\rangle$ is any graph
$B=\langle V_{A},E\rangle$, with $E\subseteq E_{A}$. The labelled version of
full subgraph keeps all labels that label the elements of $V_{A}$ and $E$ with
the same value they have in $A$.

######  Definition 21 (Underlying-deductive-structure of an rDagProof).

Given a pre rDagProof $\mathcal{C}$ = $\langle
V,E_{d},E_{A},r,\ell,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$. The full sub-
graph of $\mathcal{C}$ when we consider all and only all of the edges in
$E_{d}$ is denoted by $\mathcal{C}|_{E_{d}}$. It is called the underlying
deductive strutucture of $\mathcal{C}$.

######  Definition 22 (maximal-path).

Given a pre rDagProof $\mathcal{C}$ = $\langle
V,E_{d},E_{A},r,\ell,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$ and
$v_{k},\ldots,v_{1}$, $v_{i}\in V$, such that, $\langle
v_{i+1},v_{i}\rangle\in E_{d}$, $i=1,\ldots,k-1$. We say that
$v_{1},\ldots,v_{k}$ is a maximal path in $\mathcal{C}|_{E_{d}}$, if and only
if, $v_{k}$ is a top-formula. We say that the maximal-path starts in $v_{1}$.

The lenght of the sequence of nodes $v_{k},\ldots,v_{1}$, is $k$.

######  Definition 23 (reverse-deductive height).

Given pre r-DagProof $\mathcal{C}$ = $\langle
V,E_{d},E_{A},r,\ell,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$ of $\alpha$.
Let $\mathcal{C}|_{E_{d}}$ the sub-graph of $\mathcal{C}$ restricted to
deductive edges only ($E_{d}$). The reverse deductive height of a node $v\in
V$ in $\mathcal{C}|_{E_{d}}$, named $rdh(v)$ is defined as:

$rdh(v)=max\\{k:\mbox{$v_{1},\ldots,v_{k}$ is a maximal-path with
$v_{1}=v$}\\}$

The above definition 20 of $M_{\vdash}^{\mathcal{C}}$ is recursive. Given a
pre rDagProof $\mathcal{C}$, we can assign to each node $v\in V_{\mathcal{C}}$
the value of $rhd(v)$. By the recursion theorem, from set theory, we have that
the function $M_{\vdash}^{\mathcal{C}}$ is well-defined for every node $v$ and
natural number $i$ in any rDagProof $\mathcal{C}$. Acoording to this
assignment of values, we have that the value assigned to the root of
$\mathcal{C}|_{E_{d}}$ is $h(\mathcal{C})$, the value of all of its leaves is
0 (zero) and the value of the children of any node is smaller than the value
of their respective parent. Thus, $M_{\vdash}^{\mathcal{C}}$ is well-defined
and unique for any $\mathcal{C}$.

We note the following well-known facts, regarding usual Kripke semantics for
$\mathbf{M}_{\supset}$[21], denoted by $\models_{\mathbf{M}_{\supset}}$.

######  Fact 1 (Soundness of ND $\mathbf{M}_{\supset}$rules).

Consider $\Delta_{1}$ and $\Delta_{2}$ two sets of
$\mathbf{M}_{\supset}$formulas, and, $\delta_{1}$ and $\delta_{2}$ two
$\mathbf{M}_{\supset}$formulas. We have that:

  1. 1.

If $\Delta_{1}\models_{\mathbf{M}_{\supset}}\delta_{1}$ and
$\Delta_{2}\models_{\mathbf{M}_{\supset}}\delta_{1}\supset\delta_{2}$ then
$\Delta_{1}\cup\Delta_{2}\models_{\mathbf{M}_{\supset}}\delta_{2}$, and;

  2. 2.

If $\Delta_{1}\models_{\mathbf{M}_{\supset}}\delta_{2}$ then
$\Delta_{1}-\\{\delta_{1}\\}\models_{\mathbf{M}_{\supset}}\delta_{1}\supset\delta_{2}$

Note that the above items are just the $\supset$-Intro and $\supset$-Elim
rules. Concerning Item 2, we have both cases $\delta_{1}\in\Delta_{1}$ and
$\delta_{1}\not\in\Delta_{1}$, as it is the case with the $\supset$-Intro
rule.

In what follows we omit the symbol $\mathbf{M}_{\supset}$ in the notation
$\models_{\mathbf{M}_{\supset}}$ whenever its meaning as the minimal
entailment is made clear.

######  Definition 24 (rDagProof correctness).

Let $\mathcal{C}$ = $\langle
V,E_{d},E_{A},r,l,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$ be a pre
r-DagProof. We say that $\mathcal{C}$ is correct iff
$M_{\vdash}(r,0)\neq^{\prime}\vdash^{\prime}$ and, for each $i\neq 0$,
$i\in\mathbb{N}$, $M_{\vdash}(r,i)=^{\prime}\vdash^{\prime}$.

When a pre rDagProof $\mathcal{C}$ is correct we simply call it rDagProof.
Given a correct rDagProof $\mathcal{C}$ , such that,
$M_{\vdash}^{\mathcal{C}}(r_{\mathcal{C}},0)=\Delta\vdash\beta$, we have that
$\mathcal{C}$ is a certificate that $\beta$ as logical consequence of $\Delta$
in $\mathbf{M}_{\supset}$. This is what we state in Lemma 18 below.

######  Lemma 18 (Local entailment sounds).

Let $\mathcal{C}$ = $\langle
V,E_{d},E_{A},r,l,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$ be a correct
rDagProof of $\alpha$. Thus, for every $v\in V$, for every $i\in\mathbb{N}$,
such that $M_{\vdash}^{\mathcal{C}}(v,i)\neq\vdash$, then, if
$M_{\vdash}^{\mathcal{C}}(v,i)=\Delta\vdash\ell(v)$, $\ell(v)=\beta$, then
$\Delta\models_{\mathbf{M}_{\supset}}\beta$.

###### Proof.

By induction on the definition of $M_{\vdash}$ definition and using Lemma 1.

######  Corollary 19.

If in the stating of Lemma 18 above, we consider that:

  * •

There is a formula $\delta$, subformula of $\alpha$, such that, it is top-
formula in $\mathcal{C}$ and, there is no deductive path from this top-formula
to the root $r$ of $\mathcal{C}$ that applies an $\supset$ introduction rule
having $\delta$ as the antecedent of the formula that it is the conclusion of
this application.

Then $M_{\vdash}^{\mathcal{C}}(v,i)=\Delta\vdash\ell(v)$, $\ell(v)=\beta$,
with $\delta\in\Delta$.

###### Proof.

This corollary is a consequence of the proof of Lemma 18. Its proof is an
extension of the induction proof of the lemma, by the inclusion the condition
in the statement and verify that the formula $\delta$ is not removed during
the evaluation of $M_{\vdash}^{\mathcal{C}}(v,i)$. Since it is a top formula,
$\delta$ is included in the local entailment antecedent, in the basic step of
the induction and, we do not remove it anymore.

######  Theorem 20 (Completeness of rDagProofs).

For any $\mathbf{M}_{\supset}$formula $\alpha$ and set of subformulas $\Delta$
of $\alpha$ and subformula $\beta$ of $\alpha$, we have that if
$\Delta\models_{\vdash}\beta$ holds then there is a correct rDagProof
$\mathcal{C}$, such that,
$M_{\vdash}^{\mathcal{C}}(r_{\mathcal{C}},0)=\Delta^{\prime}\vdash\beta$, with
$\Delta^{\prime}\subseteq\Delta$.

###### Proof.

The system of Natural Deduction for $\mathbf{M}_{\supset}$is sound and
complete regarded the usual Kripke semantics for $\mathbf{M}_{\supset}$[21].
Since $ND_{\mathbf{M}_{\supset}}$ proofs are particular cases of rDagProofs we
have completeness of rDagProofs. Thus, if $\Delta\models\beta$ then there is a
derivation $\Pi$ having $\beta$ as conclusion and a set $\Delta^{\prime}$ of
open assumptions, with $\Delta^{\prime}\subseteq\Delta$. Taking $\Pi$ as a
rDagProof and by Corollary 19 we have that
$M_{\vdash}^{\mathcal{C}}(r_{\mathcal{C}},0)=\Delta^{\prime}\vdash\beta$.

######  Theorem 21 (Soundness of rDagProofs).

If $\mathcal{C}$ is a correct rDagProof and
$M_{\vdash}^{\mathcal{C}}(r,0)=\Delta\vdash\beta$ then
$\Delta\models_{\vdash}\beta$.

###### Proof.

This theorem is an immediate consequence of Lemma 18

######  Corollary 22.

If $\mathcal{C}$ is a correct rDagProof of $\alpha$ then $\alpha$ is a
$\mathbf{M}_{\supset}$tautology

We have the following lemmata that help us to show that a correct r-DagProof,
compressed by the technique that algorithm 2 implements, is sound. Moreover,
in the next section, we show an algorithm that checks whether a pre rDagProof
is correct or not. This verification is efficient (linear) on the size of the
pre rDagProof.

In the next section, we show that for any Natural Deduction $\Pi$ that has its
height linearly bounded by the size of its conclusion, $Compress(\Pi)$ is a
correct rDagProof of $\alpha$. From this result, we can conclude that any
$\mathbf{M}_{\supset}$tautology has a succinct (polynomial) and correct
rDagProof. In conclusion, we describe how to use this result to show that
$NP=CoNP$.

##  6 The compression of linearly height-bounded rDagProofs preserves
soundness

This section contains some lemmata that help us to prove that the correctness
of rDagProofs are preserved by the compression of rDagProofs.

######  Definition 25 (A-consistent sub-rDagProof).

Let $\mathcal{D}$ be a pre rDagProof of $\alpha$ and $\mathcal{C}$ a sub-
rDagProof of $\mathcal{D}$. We say that $\mathcal{C}$ is an A-consistent sub-
rDagProof of $\mathcal{D}$, if and only if, $\mathcal{D}\uparrow$ is graph-
isomorphic to $\mathcal{C}$ and for every $\langle u,v\rangle\in E_{A}$, we
have that $v\in V_{\mathcal{C}}$ and $u\not\in V_{\mathcal{C}}$, if and only
if, $v\in V_{\mathcal{D}\uparrow k}$ and $u\not\in V_{\mathcal{D}\uparrow k}$.

######  Lemma 23 (Local Entailment preservation under DetachLink).

Let $\mathcal{D}$ be a pre rDagProof and $k$ a node of $\mathcal{D}$ that is
the root of an instance of a A-consistent sub-rDagProof, cf. definition 25,
$\mathcal{C}$ of $\mathcal{D}$. Let $i\in\mathbb{N}$ be such that $i$ does not
label any of the $E_{d}$ edges going out of $k$. Moreover, consider
$\mathcal{D}^{\prime}=DetachLink(\mathcal{D},k,\mathcal{C},i)$ as defined in
Definition 13. We have that for every $v\in V_{\mathcal{D}^{\prime}}$ and
$j\in\mathbb{N}$, $j\neq i$, the following conditions hold:

  * •

If $v\not\in V(\mathcal{D})\uparrow k$ then
$M_{\vdash}^{\mathcal{D}}(v,j)=M_{\vdash}^{\mathcal{D}^{\prime}}(v,j)$, and;

  * •

If $v\in V(\mathcal{D})\uparrow k$ then
$M_{\vdash}^{\mathcal{C}}(h^{-1}(v),j)=M_{\vdash}^{\mathcal{D}^{\prime}}(v,j)$,
and;

  * •

If $v\in V(\mathcal{D})\uparrow k$ then
$M_{\vdash}^{\mathcal{C}}(h^{-1}(v),0)=M_{\vdash}^{\mathcal{D}^{\prime}}(v,i)$;

Where $h$ is the (full) labeled graph-isomorphism from $\mathcal{C}$ into
$\mathcal{D}\uparrow k$.

###### Proof.

By inspecting Definition 13, we observe that
$\mathcal{D}^{\prime}=(\mathcal{D}-\mathcal{C}^{\prime})\cup\mathcal{C}$,
where $\mathcal{D}\uparrow k=\mathcal{C}^{\prime}=h(\mathcal{C})$. We note
that $M_{\vdash}^{\mathcal{D}^{\prime}}$ definition is then either on the
complement of $\mathcal{D}\uparrow k$, or on $\mathcal{C}$. The former agrees
with $M_{\vdash}^{\mathcal{D}}$ and the later agrees with
$M_{\vdash}^{\mathcal{D}\uparrow k}=M_{\vdash}^{h(\mathcal{C})}$. Finaly, the
third item in the statement of the lemma is related to the new edge that links
the root of $\mathcal{C}$ to the former target of the $E_{d}$ edge that linked
$k$ with this target. The top-formulas that are related to the basis steps of
$M_{\vdash}$ recursion are accordingly accordingly associated to each
respective part of $\mathcal{D}^{\prime}$, the same can be said about the
recursive steps. So we have the desired result.

######  Corollary 24 (Soundness of DetachLink).

Consider the conditions of Lemma 23, above. We have that if $\mathcal{C}$ is
correct and $\mathcal{D}$ is also correct then
$DetachLink(\mathcal{D},k,\mathcal{C},i)$ is correct. Moreover, the local
entailment is preserved, modulo the the isomorphism between
$\mathcal{D}\uparrow k$ and $\mathcal{C}$.

An immediate consequence of Corollary 24 is that it the DetackLink operation
can be repeated many times, without disturbing the soundness of the yielded
rDagProof. Due to this, we have the following lemma.

######  Lemma 25 (Soundness of Collapse).

Let $\mathcal{D}$ and $\mathcal{C}$ be r-DagProofs. Let $\mathcal{C}$ be
A-consistent subgraph of $\mathcal{D}$. Let $\mathcal{Y}$ be a list containing
the roots of the instances of $\mathcal{C}$ in a fixed level $\mu$. We have
that if $\mathcal{D}$ and $\mathcal{C}$ are correct then
$Collapse(\mathcal{D},\mathcal{Y},\mathcal{C})$ is correct too. Moreover the
local entailment is preserved as stated in Lemma 23.

The above Lemma 25 is the correctness proof of algorithm 1.

The following theorem proves the correctness of algorithm 2

######  Theorem 26 (Soundness of Compressed rDagProofs).

Let $\mathcal{D}=\langle
V,E_{d},E_{A},r,l,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$ be a pre
rDagProof for a $\mathbf{M}_{\supset}$formula $\alpha$. If $\mathcal{D}$ is
correct then for every $3<p$ $Compress(\mathcal{D},p)$ is correct. Moreover,
the local entailment is preserved, i.e.,

###### Proof.

This proof proceeds by induction on the number of, recursive, calls to
$Compress$. In the proof of the termination of algorithm 2, we have seen that
it halts for every $\mathcal{D}$ and $p$, $3<p$. The basis step is trivial,
and we use the inductive hypothesis together with Lemma 25 to prove the
inductive (recursive) step.

##  7 On the complexity of verifying that a pre rDagProof is correct or not

The following algorithm performs a top-down sweeping in any pre rDagProof to
check whether it is correct or not. It is an iterative implementation of
$M_{\vdash}^{\mathcal{C}}$ that prints can check whether the pre rDagProof is
correct, and certifies a tautology or not. In the case, it is not a tautology
it prints “DERIVATION”. Finally, it prints “INCORRECT” if the rDagProof is not
correct. The definition of $M_{\vdash}$ points out the correctness of the
algorithm. We analyse its computational complexity in the sequel. We have to
note that the $update-and-check$, inside the iteration structures in lines 17
and 35 is responsible by updating the local entailment data-structure (the
$Reg$ indexed structure) with ${}^{\prime}\vdash^{\prime}$ to indicate that
the checking algorithm detected an incorrect pre rDagProof.

Algorithm 3 Verifies whether a r-DagProof is valid

1: Function Check-rDagProof($\mathcal{C}$)

2: for $k=height(\mathcal{C})downto0$ do

3: $L\leftarrow TopFormulas(k)$

4: for $top\in L$ do

5: $Reg(top)\leftarrow\emptyset$

6: for $edge\in AncestorEdges(top)$ do

7: $Reg(top)\leftarrow
Reg(top)\cup\\{\delta(edge)\mapsto\ell(top)\vdash\ell(top)\\}$

8: end for

9: $Reg(top)\leftarrow Reg(top)\cup\\{0\mapsto\ell(top)\vdash\ell(top)\\}$

10: end for

11: $I\leftarrow InternalNodes(k)$

12: for $v\in I$ do

13: $q\leftarrow Premisses(v)$

14: if $Divergent(v)$ then

15: $Lv\leftarrow\\{\langle v,w\rangle:\langle v,w\rangle\in E_{A}\\}$

16: if $\\{i:Defined(Reg(q,i\\}=\\{\rho(e):e\in Lv\\}$ then

17: for $i\in Reg(q)$ do

18: $Reg(v,i)\leftarrow update-and-check(v,q,i)$

19: end for

20: else

21: $Reg(v,0)\leftarrow\;\;^{\prime}\vdash^{\prime}$

22: end if

23: else

24: if $TargetDivergent(v)$ then

25: $u\leftarrow\;\iota\\{u:\langle u,v\rangle\in E_{d}\\}$

26: if $Defined(\rho(\langle u,v\rangle)\;\land\;\neg\exists\langle
w,v\rangle\in E_{A}$ then

27: $Reg(v,0)\leftarrow Reg(u,\rho(\langle u,v\rangle))$

28: $Reg(v,j)\leftarrow\;\;^{\prime}\vdash^{\prime}\;\;\forall j\neq 0$

29: end if

30: if $Defined(\rho(\langle u,v\rangle)\;\land\;\exists\langle w,v\rangle\in
E_{A}$ then

31: $Reg(v,\delta(\langle w,v\rangle))\leftarrow\;Reg(u,\rho(\langle
u,v\rangle))$

32: $Reg(v,j)\leftarrow\;\;^{\prime}\vdash^{\prime}\;\;\forall
j\neq\delta(\langle w,v\rangle))$

33: end if

34: else

35: for $i\in Reg(q)$ do

36: $Reg(v,i)\leftarrow update-and-check(v,q,i)$

37: end for

38: end if

39: end if

40: end for

41: end for

42: if $Reg(r)\neq\;\;^{\prime}\vdash^{\prime}$ then

43: $CORRECT$

44: if $Reg(r)==\;\;\vdash\ell(r)$ then

45: $TAUTOLOGY$

46: else

47: $DERIVATION$

48: end if

49: else

50: $INCORRECT$

51: end if

Let $\mathcal{C}=\langle
V,E_{d},E_{A},r,l,L,\rho,\delta,\mathcal{O}_{\alpha}\rangle$ be a pre
rDagProof. We set $n_{v}=\left|V\right|$, $n_{A}=\left|E_{A}\right|$,
$m=\left|\mathcal{O}_{\alpha}\right|=\left|T_{\alpha}\right|\leq len(\alpha)$
and $h=height(\mathcal{C})=height(\langle V,E_{d}\rangle)$. In the sequel, all
the line references are in algorithm 3. We proceed to a worst case analysis to
find an upper-bounded for the number of steps to check whether $\mathcal{C}$
is correct or not. The loop that starts in line 2 consumes $h$ steps, for each
of these steps, we have at most $n_{v}$ possible nodes that are top-formulas,
this is what line 4 sweeps using the “for” statement. Inside this “for” there
is other nested iteration on the set of ancestor edges that target the top-
formulas, and a consequent updating in the list of local entailments stored in
the $Reg$ data-structure. Line 9 is responsible by the update of the main
local-entailment (indexed by 0). After that, the loop that starts in line 12
takes care of the internal nodes, and for each internal node, we have two
possible cases, either it is a target of a divergent node and the needed
udpate on the local indexed by the index 0 is made, or, the update of all
indexes, including the 0, of the local entailment structure is made. The
choice is made by the “if” statement in line 24. The cost of with steps that
takes care of the top-formulas is $h\times n_{V}\times n_{A}$. To this we have
to add the cost of processing the internal nodes that is $h\times n_{v}\times
n_{A}$ too, due to the cost of updating the indexes related to each Ancestor
edge in $E_{A}$. However, as top-formulas and internal nodes are disjoint then
we have that algorithm 3 when applied on $\mathcal{C}$ performs the number of
steps upper-bounded by disequality 1:

$\displaystyle Steps(\mathcal{C})\leq h\times n_{v}\times n_{A}$ (1)
$\displaystyle Steps(\mathcal{C})\leq n_{v}\times n_{v}^{3}=n_{v}^{4}$ (2)

Observing that $n_{A}\leq n_{v}^{2}$ and $h\leq n_{v}$ we have the upper-bound
in disequality 2 Since we are counting steps, we can say that the time
complexity to check whether a pre rDagProof $\mathcal{C}$ is correct or not is
polynomial, 4th power indeed, on the size of $\mathcal{C}$.

##  8 A brief argument towards $CoNP=NP$

We have already discussed in the introduction of this text that when
considering the complexity class $CoNP$, we are naturally limited to linearly
height-bounded proofs. The proofs, in $\mathbf{M}_{\supset}$, of the non-
hamiltonianicity of graphs, are linearly height bounded. See the appendix in
[13] or [9] for a detailed explanation on this. If $NP\neq CoNP$ then the set
of non-hamiltonian graphs there is no polynomially sized and verifiable in
polynomial time certificate for each of its elements. Thus, the set $S$ of all
formulas that have Normal Natural Deduction proofs linear height-bounded
contains the valid for the non-hamiltonian graphs. Hence, by assuming that
$NP\neq CoNP$, we have to conclude that $S$ is a family of normal super-
polynomial proofs with linear height. If we consider any proof in $S$, either
it is polynomially sized, and we have nothing to prove, or it is bigger than
$m^{p}$, for some $p>3$, where $m$ is the size of the proof’s conclusion. We
observe that the case $p\leq 3$ is subsumed by $p>3$, anyway. Thus, we can
apply Theorem 7 to show that this big proof is redundant, so we can apply the
compression algorithm 2 to obtain a correct rDagProof of size smaller than
$m^{p}$, according to Lemma 17. Finally, the algorithm 3 can check the
correctness of this polynomially sized rDagProof in time upper-bounded by
$m^{4p}$.

The last paragraph provided a precise argumentation showing polynomial
certificates for each non-hamiltonicity of each non-hamiltonian graph. We can
check each of them is a (correct) certificate in polynomial time too. We can
conclude that $CoNP\subseteq NP$, since non-hamiltonicity of graphs is a
$CoNP$-complete problem. Having proved that $CoNP\subseteq NP$ we have proof
that $NP=CoNP$, as the following reasoning shows, where $\overline{L}$ is the
set-theoretical complement of $L$. We have used the logically simplest
definition of the class $CoNP$ class as $\\{\overline{L}:L\in NP\\}$.

$\begin{array}[]{c}\Rightarrow CoNP\subset NP\\\ \Downarrow\\\ \mbox{$L\in
NP$, iff, $\overline{L}\in CoNP$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}CoNP\subseteq
NP}$ so $\overline{L}\in NP$, iff, $L\in CoNP$}\\\ \Downarrow\\\
CoNP=NP\end{array}$

More details and mathematical precision on this argument contain an
alternative proof to the conjecture $CoNP=NP$ and are a matter for a further
article.

##  9 Conclusion

This article shows that for any huge proof of a tautology in
$\mathbf{M}_{\supset}$we obtain a succinct certificate for its validity.
Moreover, we offer an algorithm able to check this validity in polynomial time
on the certificate’s size. We can use this result to provide a compression
method to propositional proofs. Moreover, we can efficiently check the
compressed proof without uncompressing it. Thus, we have many advantages over
traditional compression methods based on strings. The compression ratio of
techniques based on collapsing redundancies seems to be bigger, as shown in
[22] that reports some experiments with a variation of the Horizontal
Compression method compared with Huffman compression. The second and more
important advantage is the possibility to check for the validity of the
compressed proof without having to uncompress it. In general, the original
proof is huge, super-polynomial and hard check computationally.

Another application of the results in this article is to provide an
alternative proof of $NP=CoNP$. In [8] we have a proof that $NP=NPSPACE$. An
immediate consequence of this equality is that $NP=CoNP$. The approach that
arises from the results we have shown here does not need Hudelmaier [15]
linearly bounded sequent calculus for $\mathbf{M}_{\supset}$logic. The proof
reported in [8], on the other hand, needs Hudelmaier Sequent Calculus and a
translation to Natural Deduction proofs that preserves the linear upper-bound.
However, the resulted translation is not normal, and it is well-known that
normalization does not preserve upper-bounds in general. Thus, we cannot apply
our approach to the whole class of $\mathbf{M}_{\supset}$tautologies to prove
that $NPSPACE\subseteq NP$, for the use of normal proofs is essential to
obtain the redundancy lemma, i.e., Lemma 7. However, the compression method
reported in this article, due to the redundancy lemma, provides knowledge to
prove $\mathbf{M}_{\supset}$short tautologies automatically. It seems easier
than the use of the double certificate approach in [8].

##  10 Acknowledgement

We would like very much to thank professor Lew Gordeev for the work we have
done together and the inspiration to follow this alternative approach. Thank
Professor Luiz Carlos Pereira for his support, lessons and ideas on Proof
Theory since the first course I have taken with him as a student. Thank the
proof-theory group at Tuebingen-University, led by prof. Peter Schroeder-
Heister. Many thanks to profs Gilles Dowek (INRIA) and Jean-Baptiste Joinet
(univ. Lyon) for the intense interaction during this work’s elaboration.
Finally, we want to thank all students, former students, and colleagues who
discussed with us in many stages during this work. We must have forgotten to
mention someone, and we hope we can mend this memory failure in a nearer
future.

## References

  * [1] A.Church.  A set of postulates for the foundations of logic.  Annals of Mathematics, 33(2):346–366, 1932.  Corrections in [2].
  * [2] A.Church.  A set of postulates for the foundations of logic (second paper).  Annals of Mathematics, 34(4):839–864, 1933.
  * [3] Bovet, D. and Crescenzi, P.  Introduction to the Theory of Complexity,  Prentice-Hall, 1994.
  * [4] S. Arora and B. Barak.  Computational Complexity: A Modern Approach.  Cambridge University Press, 2009.
  * [5] G.Gentzen.  Untersuchungen über das logische schließsen I.  Mathematische Zeitschrift, 39:176–210, 1935.  English translation in [6].
  * [6] G.Gentzen.  Investigations into logical deduction I.  American Philosophical Quarterly, 1(4):288–306, 1964.  English translation by M. E. Szabo.
  * [7] L.Gordeev and E. H. Haeusler. _Proof Compression and NP versus PSPACE_. Studia Logica 107, 53-83 (2019).
  * [8] L.Gordeev and E. H. Haeusler. _Proof Compression and NP versus PSPACE II_. Bulletin of the Section of Logic, 2020, 18 pages, https://doi.org/10.18778/0138-0680.2020.16.
  * [9] L. Gordeev and E. H. Haeusler. _Proof Compression and NP Versus PSPACE II: Addendum_ , CoRR, abs/2011.09262, 2020, in https://arxiv.org/abs/2011.09262v2.
  * [10] E. H. Haeusler. _Propositional Logics Complexity and the Sub-Formula Property_ , in Proceedings Tenth International Workshop on Developments in Computational Models, DCM 2014, Vienna, Austria, 13th July 2014.
  * [11] Edward Hermann Haeusler. _Every super-polynomial proof in purely implicational minimal logic has a polynomially sized proof in classical implicational propositional logic_ , CoRR, abs/1505.06506, 2015, in http://arxiv.org/abs/1505.06506.
  * [12] E. H. Haeusler. _On the Intrinsic Redundancy in Huge Natural Deduction proofs II: Analysing $M_{\supset}$ Super-Polynomial Proofs_, CoRR, submmited to Arxiv in August.
  * [13] E. H. Haeusler. _Exponentially Huge Natural Deduction proofs are Redundant: Preliminary results on $M_{\supset}$_, CoRR, abs/2004.10659, 2020, in https://arxiv.org/abs/2004.10659.
  * [14] E. H. Haeusler,  _How Many Times do We Need an Assumption to Prove a Tautology in Minimal Logic? Examples on the Compression Power of Classical Reasoning_.  Electronic Notes in Theoretical Computer Science, v.315, 2015, pp 31-46.
  * [15] Hudelmaier, Jörg. _An $\mathcal{O}(n\log n)-Space$ Decision Procedure for Intuitionistic Propositional Logic_, Journal of Logic and Computation, volume 3, number 1, pp. 63-75, 1993.
  * [16] D. Hilbert und W. Ackermann, Grundzüge der theoretischen Logik. Julius Springer, Berlin 1928. English version Principles of Mathematical Logic, Chelsea, New York 1950, ed. by R. E. Luce is based on 2nd German edition, 1938.
  * [17] Ladner, Richard E.  _The Computational Complexity of Provability in Systems of Modal Propositional Logic_.  SIAM J. Comput., n.3, v.6, 1977.
  * [18] D. Prawitz, Natural deduction: a proof-theoretical study. Almqvist & Wiksell, 1965
  * [19] J. Rothe, Complexity Theory and Cryptology, Texts in Theoretical Computer Science, An EATCS Series, Springer, 2005.
  * [20] W. Savitch, _Relationships between nondeterministic and deterministic tape complexities_ , J. of Computer and System Sciences (4): 177–192 (1970)
  * [21] Segerberg, Krister. _Propositional Logics Related to Heyting’s amd Johansson’s_ , Theoria, 34:26-61.
  * [22] José Flávio Cavalcante Barros Jr and Edward Hermann Haeusler. _A comparative study on proof compression techniques_ , Brazilian Meeting on Logic, 2019, Proceedindgs, pages 85-86, in https://ebl2019.ci.ufpb.br/assets/Book_of_Abstracts_EBL_2019.pdf. In portuguese.
  * [23] R. Statman, _Intuitionistic propositional logic is polynomial-space complete_ , Theor. Comp. Sci. (9): 67–72 (1979)
  * [24] V. Ŝvejdar, _On the polynomial-space completeness of intuitionistic propositional logic_ , Archive for Math. Logic (42): 711–716 (2003)