A Closer Look at Some Recent Proof Compression-Related Claims^††thanks: Supported in part by NSF grant CCF-2006496 .

Natural deduction is a way of formalizing languages of logic that involves creating proofs (also referred to as deductions) of logical sentences by application of a set of inference rules. These inference rules represent the very natural notion of deductive reasoning, where if some set of premises are known to be true, we can infer some conclusion. The rules are defined using what can be thought of as templates of logical sentences. Instead of using individual propositional variables, the templates use variables that represent entire sentences of their own. For example, the template $A\lor B$ could represent infinitely many sentences including $p\lor q$, $(p\land q)\lor(r\rightarrow q)$, etc. The inference rules are defined with the following notation

where $\beta$ can be immediately derived from the $\alpha_{i}$s, i.e., if every $\alpha_{i}$ is known to be true, then $\beta$ is also known to be true. Application of these rules to derive some sentence $\rho$ results in a tree for which $\rho$ is the root, and each parent is related to its children by a particular inference rule. Each leaf of the tree is an assumption. Anything can be assumed, but the derived sentence only holds under the assumptions (unless they are discharged—see below).

For example, suppose we have a system of natural deduction that has the rules $\frac{A\ B}{A\land B}$ and $\frac{A\land B}{A}$. If we wanted to derive $(p\land q)\land r$ from the assumptions $p$, $q$, and $r\land s$, we could do so with the following derivation:

With the system as is, sentences can only be derived under a nonempty set of assumptions, so there are no tautologies (sentences that are always true; they can be derived without assumptions). This is where the notion of discharging assumptions comes in. Inference rules can be defined so that their application discharges specific assumptions, meaning that those assumptions are accounted for and are no longer assumed. This is indicated in the inference rule by writing the assumption being discharged in parentheses above the $\alpha$ for which it applies. We can expand the formalization of the notation for inference rules to

where, for each $i\in\{1,\ldots,k\}$, whenever $\gamma_{i}$ is an assumption of the subderivation leading to $\alpha_{i}$, $\gamma_{i}$ is discharged. In the derivation, every rule application that discharges an assumption is labeled with a number, and that number is written above every instance of the assumption it discharges.

Returning to the earlier example, suppose we add this new inference rule that allows us to discharge any assumption:

We can now prove the tautology $(r\land s)\rightarrow(q\rightarrow(p\rightarrow((p\land q)\land r)))$ by extending the derivation from above and discharging all the assumptions.

We can clearly see that this is a tautology because every leaf in the tree has a number above it, so every assumption is discharged.

For a more detailed exposition of natural deduction, we refer readers to Prawitz’s monograph on the topic [Pra06].

Sequent calculus is another approach to logical derivation. Compared to natural deduction, it has a similar notation for inference rules and a similar tree-like proof structure, but differs greatly in how it handles assumptions. Rather than single logical sentences, each node in the deduction (an $\alpha$ or $\beta$ in the notation specified in Section 2.1) is a sequent—a conditional tautology expressed as $\Gamma\Rightarrow\Delta$ where $\Gamma$ is a set of antecedents and $\Delta$ is a single consequent.¹¹1 In some systems, $\Delta$ could be set of consequents rather than a singe consequent, but we will not consider such systems here. The consequent is what can be proved given that all of the antecedents are true. The sequent essentially bundles the assumptions together with the consequent, making each sequent in some sense self-contained: while the full derivation is needed to establish validity of the sequent, each individual sequent in the derivation is true on its own; there are no separate assumptions in other parts of the derivation that must be accounted for. This removes the need to discharge assumptions, and instead we can simply remove antecedents. An unconditional tautology would be any consequent for which there are no antecedents. In other words, any $\Delta$ for which $\Gamma$ is the empty set. Sequent calculi include axioms in addition to their inference rules. Rather than each leaf of the deduction tree being an assumption, each leaf must be an axiom. In both axioms and inference rules, a subset of the antecedents can be specified while the rest of the antecedents are left free using the notation $\Gamma,\alpha_{1}\ldots\alpha_{n}$.

As an example, consider a sequent calculus with just the axiom $\Gamma,p\Rightarrow p$ and the inference rule $\frac{\Gamma,A\Rightarrow B}{\Gamma\Rightarrow A\rightarrow B}$.²²2This inference rule is essentially the sequent calculus analogue of the last natural deduction rule from the example in Section 2.1 that was for discharging assumptions. We could use this system to prove the unconditional tautology $p\rightarrow(q\rightarrow p)$ as follows:

For a more detailed exposition of sequent calculus, we refer readers to Appendix A of Prawitz [Pra06].

Intuitionistic logic is a logic which rejects both the law of excluded middle ($\vdash p\lor\lnot p$) and double negation elimination ($\lnot\lnot p\vdash p$). Minimal logic, originally introduced by Johansson [Joh37], is an intuitionistic logic that additionally rejects the principle of explosion ($\bot\vdash p$).

The notions of intuitionistic and minimal logic can be applied to different syntaxes of logic. They are traditionally formalized in the context of predicate logic [Joh37, Pra06] but may also be applied in the context of propositional logic (as in [Hud93]) or even purely implicational logic (discussed in [Pog94]). Regardless of the syntactic context, the restrictions relative to classical logic remain the same, and the differences between, for example, intuitionistic propositional logic and intuitionistic predicate logic are the same as the differences between classical propositional logic and classical predicate logic (namely the inclusion of quantifiers, quantified variables, and relations).

It is worth noting that negation ($\lnot$) is generally not included as a propositional connective in intuitionistic or minimal logic. Rather, absurdity ($\bot$) is added as a nullary connective, where $\lnot p$ is interpreted as a shorthand for $p\rightarrow\bot$.

Prawitz formalizes systems of natural deduction for minimal, intuitionistic, and classical logic [Pra06]. The system for minimal logic uses the following inference rules:

These rules consist of one introduction rule and one elimination rule for each standard (binary) propositional connective. Prawitz also included introduction and elimination rules for $\forall$ and $\exists$ because the system was formulated in predicate logic, but we can simply take the propositional fragment (i.e., remove the rules for quantifiers) to get a system for minimal propositional logic.

Prawitz’s system for intuitionistic logic includes all of the above inference rules along with a rule for the principle of explosion, formalized as:

Hudelmaier presents a ${\rm PSPACE}$ algorithm for intuitionistic propositional logic [Hud93]. The procedure uses backward application of the rules of a sequent calculus (referred to as LG). The ${\rm PSPACE}$ classification is achieved because LG was constructed to have the critical property that every deduction of a sequent $s$ is linearly bounded in length with respect to the length of $s$. This is not a linear (or even polynomial) bound on the overall size of the deduction, only the length (as some of the rules produce multiple branches).

The calculus LG includes the axioms $\Gamma,p\Rightarrow p$ and $\Gamma,\bot\Rightarrow p$. The latter axiom is the principle of explosion, and thus can be excluded to create a minimal propositional logic version of the calculus. LG uses 12 inference rules labeled: $GI1\land$, $GI2\land$, $GI1\lor$, $GI2\lor$, $GI1\mathord{\rightarrow}$, $GI2\mathord{\rightarrow}$, $GE\land$, $GE\lor$, $GE\mathord{\rightarrow}P$, $GE\mathord{\rightarrow}\land$, $GE\mathord{\rightarrow}\lor$, $GE\mathord{\rightarrow}\mathord{\rightarrow}$. For brevity, these will not be listed here in their full form, but they use the following naming conventions: Rules in the form $GIXC$, where $X\in\{1,2\}$ and $C$ is a propositional connective, are introduction rules that introduce $C$ in the consequent. Rules in the form $GEC$ are elimination rules that introduce $C$ in the antecedent. The four $GE\mathord{\rightarrow}$ rules introduce an implication in the antecedent, in which the antecedent of said implication includes the specified connective or, in the case of $GE\mathord{\rightarrow}P$ is just a propositional variable.

In this paper, we assume familiarity with basic concepts of complexity theory. Readers may wish to consult any standard text on the subject, e.g., [Pap94, Sip13].

The complexity class ${\rm NP}$ is the class of languages that can be decided by a nondeterministic Turing machine in polynomial time. The class ${\rm PSPACE}$ is the class of languages that can be decided by a deterministic Turing machine using polynomial space. The class ${\rm FP}$ is the set of polynomial-time computable functions. It is well-known that ${\rm NP}\subseteq{\rm PSPACE}$, and whether ${\rm NP}={\rm PSPACE}$ is a central open issue in theoretical computer science.

Formally, given two sets (i.e., decision problems) $A$ and $B$, we say that $A\leq_{m}^{p}B\iff(\exists f\in{\rm FP})(\forall x)[x\in A\iff f(x)\in B]$, i.e., $A$ (polynomial-time) many-one reduces to $B$. Many-one reductions are tremendously important in complexity theory, as they allow one to relate the hardness of one problem to that of another. One such way is via “complete problems.”

Formally, a ${\rm PSPACE}$-complete problem $B$ is a ${\rm PSPACE}$ problem such that $(\forall A\in{\rm PSPACE})[A\leq_{m}^{p}B]$. Informally, ${\rm PSPACE}$-complete problems are the “hardest” problems in ${\rm PSPACE}$. It is well-known that polynomial-time many-one reductions are transitive and that ${\rm NP}$ is closed downwards under polynomial-time many-one reductions (i.e., if $A\leq_{m}^{p}B$ and $B\in{\rm NP}$, then $A\in{\rm NP}$). It follows that if some ${\rm PSPACE}$-complete problem is shown to be in ${\rm NP}$, then ${\rm NP}={\rm PSPACE}$.

The two calculi introduced in the paper, $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$, are not novel systems—they are modifications to existing systems proposed by Hudelmaier [Hud93] and Prawitz [Pra06], respectively. Thus, proofs of their soundness and completeness with respect to minimal propositional logic are delegated to the papers from which the systems originated [GH19, Claim 1, Claim 3]. However, the modifications are substantial and equivalence is not proved, so delegating the proofs is not a valid strategy. Thus, $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$ are not established to be sound and complete for minimal propositional logic.

In both cases, all rules that are not purely implicational are left out, as well as all rules including $\bot$. In converting from LG [Hud93] to $\text{LM}_{\mathord{\rightarrow}}$, this includes the second axiom ($\Gamma,\bot\Rightarrow p$), which is correctly omitted to modify the intuitionistic logic to a minimal logic, along with $GI1\land$, $GI2\land$, $GI1\lor$, $GI2\lor$, $GE\land$, $GE\lor$, $GE\mathord{\rightarrow}\land$, and $GE\mathord{\rightarrow}\lor$, which are incorrectly omitted, resulting in a modification from minimal propositional logic to minimal implicational logic. In converting from Prawitz’s minimal logic [Pra06] to $\text{NM}_{\mathord{\rightarrow}}$, rules $\land I$, $\land E$, $\lor I$, and $\lor E$ are incorrectly omitted, again resulting in a modification from minimal propositional logic to minimal implicational logic. These inference rules are needed to prove many things in minimal propositional logic, so omitting them weakens the system.

As a counterexample to the completeness of $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$ with respect to minimal propositional logic, consider

This is clearly provable in minimal propositional logic, as demonstrated by the following natural deduction proof:

Pure implication is not functionally complete and thus cannot express all the standard propositional connectives. $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$, being purely implicational systems, cannot directly express, for example, $\land$. This alone could be considered sufficient evidence against the completeness of $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$; if they cannot even express certain tautologies of minimal propositional logic they have no hope of proving the tautologies. However, one might argue that a system that is able to prove the same notions in a different notation could still be considered complete for minimal propositional logic. At the very least, the overall results of the paper would hold if minimal propositional logic could be polynomial-time many-one reduced to minimal implicational logic.

The functional incompleteness of implication can be resolved with the addition of $\bot$. For example, $p\land q$ could be expressed as $(p\rightarrow(q\rightarrow\bot))\rightarrow\bot$. Since each standard propositional connective could be replaced with an equivalent expression using only $\rightarrow$ and $\bot$ in polynomial time, we can permit this transformation with regards to time complexity results. The paper does establish that the language of minimal logic being used does not include $\bot$ [GH19, Section 1], but since allowing $\bot$ to take the place of any predicate in an existing axiom or rule does not impact any of their proofs, we will permit it in an attempt to recover the results of the paper.

Using only implication and $\bot$, $(p\land q)\rightarrow p$ can be expressed as:

There are other ways it could be expressed, but this is the simplest and most standard. The below argument will work in exactly the same way for any alternative choice of how to represent $\land$.³³3It is worth noting that the representation must treat the $(p\land q)$ clause as atomic, and thus cannot restructure the entire sentence to something like $p\rightarrow(q\rightarrow p)$. While $p\rightarrow(q\rightarrow p)$ also expresses a similar idea, it cannot be used for a transformation from minimal propositional logic to minimal implicational logic because it depends on the $\rightarrow$ following the $\land$ clause, and thus cannot be generalized.

Because the proof systems $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$ have no axioms or inference rules specifically including $\bot$, formulas including $\bot$ can only be derived by treating $\bot$ as an ordinary subformula, no different from some arbitrary $A$. In other words, the special meaning we have assigned to $\bot$ as a nullary connective cannot be leveraged in derivations. Any derivation involving $\bot$ could be modified by replacing every occurrence of $\bot$ with some new propositional variable, and each rule application would remain valid, as $p$ could take the place of a variable in an inference rule just as easily as $\bot$ could. For the same reason, any propositional variable could be replaced with $\bot$, as the variable cannot be broken down into smaller components to take advantage of some rule that $\bot$ cannot. Essentially, $\bot$ and $p$ are both atomic and indistinguishable from the perspective of the inference rules in $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$, so they are interchangeable. For example, $\bot\rightarrow(p\rightarrow\bot)$ is a theorem in $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$ precisely because $q\rightarrow(p\rightarrow q)$ is also a theorem in $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$.

Thus, $((p\rightarrow(q\rightarrow\bot))\rightarrow\bot)\rightarrow p$ is a theorem in $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$ if and only if $((p\rightarrow(q\rightarrow r))\rightarrow r)\rightarrow p$ is a theorem. The latter is obviously not a tautology in minimal propositional logic (or even in the more permissive classical logic—consider the case where $p$ is false and $r$ is true), and therefore is not a theorem either since $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$ are both sound.

We can thus conclude that $(p\land q)\rightarrow p$ is a tautology in minimal propositional logic but is not a theorem of $\text{LM}_{\mathord{\rightarrow}}$ or $\text{NM}_{\mathord{\rightarrow}}$, and cannot be transformed into an equivalent implicational theorem of $\text{LM}_{\mathord{\rightarrow}}$ or $\text{NM}_{\mathord{\rightarrow}}$. Therefore, $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$ are not complete with respect to minimal propositional logic.

The paper claims that tree-like provability in $\text{NM}_{\mathord{\rightarrow}}{}$ is sound and complete with respect to minimal propositional logic [GH19, Lemma 5]. We have established this to be false. It makes the same claim for DAG-like provability in $\text{NM}_{\mathord{\rightarrow}}{}$ [GH19, Corollary 20], but depends on the soundness and completeness of tree-like provability [GH19, Lemma 5] to do so, so it does not hold. Corollary 1 [GH19, Corollary 21], the central result of the paper, depends on soundness and completeness of DAG-like provability [GH19, Corollary 20], and thus it also does not hold. Therefore, the paper has not proven that all (and only) tautologies of minimal propositional logic have a proof whose size is polynomial in the size of the tautology.

One might try to recover the results of the paper by extending $\text{LM}_{\mathord{\rightarrow}}$ and $\text{NM}_{\mathord{\rightarrow}}$ to include the omitted rules and updating the transformation and compression algorithms to account for $\land$ and $\lor$. This would require adding at least eight additional cases to the recursive function that converts from $\text{LM}_{\mathord{\rightarrow}}$ to $\text{NM}_{\mathord{\rightarrow}}$ to handle the eight missing rules of LG, and would disrupt many of the assumptions and proofs throughout the paper.

Notably, the inclusion of the rest of the rules from LG would invalidate the semi-subformula property [GH19, Lemma 2.1]. For a counterexample, consider inference rule $GE\mathord{\rightarrow}\lor$:⁴⁴4 The notation has been slightly modified from the original paper to maintain consistency of notation within this paper; the semantics remain identical. Note that $p$ is a propositional variable not occurring in $A$, $B$, $C$, or $D$.

This involves multiple formulas that cannot appear in the resulting formula that they are being used to prove. Thus, even a weaker notion of the semi-subformula property (one that allows more nonproper subformulas beyond just $\beta\rightarrow\gamma$ as a semi-subformula of $(\alpha\rightarrow\beta)\rightarrow\gamma$) could not hold, as arbitrary propositional variables can appear in a deduction in LG that are not anywhere in the formula being proved.

The semi-subformula property is crucial for proving the polynomial bound on foundation in $\text{LM}_{\mathord{\rightarrow}}$ [GH19, Lemma 2.4]. The bound on foundation depends on a polynomial bound on the number of distinct semi-subformulas of any given formula, but if the semi-subformula property is lost and arbitrary formulas can appear in the deduction that are not semi-subformulas, the bound on foundation is lost as well. Without a polynomial bound on foundation in $\text{LM}_{\mathord{\rightarrow}}$, the polynomial bound on foundation for deductions in $\text{NM}_{\mathord{\rightarrow}}$ [GH19, Theorem 4] would also fail to hold, as it relies on property carryover from LG. The bound on foundation for $\text{NM}_{\mathord{\rightarrow}}$ is what allows the compression algorithm to get a polynomial bound in size. Only identical formulas can be merged in the DAG, so if there is no polynomial bound on foundation then the compression cannot get a polynomial bound on size [GH19, Corollary 15]. Without the polynomial bound on size, Corollary 1 [GH19, Corollary 21] is similarly lost. Thus even the substantial additions that would be required to cover the rest of minimal propositional logic are not sufficient to recover the central results of the paper.