Proof Complexity of Monotone Branching Programs

Abstract

We investigate the proof complexity of systems based on positive branching programs, i.e. non-deterministic branching programs (NBPs) where, for any 0-transition between two nodes, there is also a 1-transition. Positive NBPs compute monotone Boolean functions, like negation-free circuits or formulas, but constitute a positive version of (non-uniform) $\mathbf {N}\mathbf {L}$, rather than $\mathbf {P}$ or $\mathbf {NC}^{1}$, respectively.

The proof complexity of NBPs was investigated in previous work by Buss, Das and Knop, using extension variables to represent the dag-structure, over a language of (non-deterministic) decision trees, yielding the system $\mathsf {e}\mathsf {LNDT}$. Our system $\mathsf {e}\mathsf {LNDT}^{+}$ is obtained by restricting their systems to a positive syntax, similarly to how the ‘monotone sequent calculus’ $\mathsf {MLK}$ is obtained from the usual sequent calculus $\mathsf {LK}$ by restricting to negation-free formulas.

Our main result is that $\mathsf {e}\mathsf {LNDT}^{+}$ polynomially simulates $\mathsf {e}\mathsf {LNDT}$ over positive sequents. Our proof method is inspired by a similar result for $\mathsf {MLK}$ by Atserias, Galesi and Pudlák, that was recently improved to a bona fide polynomial simulation via works of Jeřábek and Buss, Kabanets, Kolokolova and Koucký. Along the way we formalise several properties of counting functions within $\mathsf {e}\mathsf {LNDT}^{+}$ by polynomial-size proofs and, as a case study, give explicit polynomial-size poofs of the propositional pigeonhole principle.

1 Introduction

Proof complexity is the study of the size of formal proofs. This pursuit is fundamentally tied to open problems in computational complexity, in particular due the Cook-Rechow theorem [8]: $co \mathbf {NP}= \mathbf {NP}$ iff there is a ‘formal’ proof system that has polynomial-size proofs of each propositional tautology. This has led to what is known as ‘Cook’s program’ for separating $\mathbf {P}$ and $\mathbf {NP}$ (see, e.g., [7, 17]).

Systems of interest in proof complexity are typically motivated by analogous results from circuit complexity. For instance ‘bounded depth’ systems restrict proofs to formulas with a limit on the number of alternations between $\vee$ and $\wedge$ in its formula tree, i.e. $\mathbf {AC}^{0}$ concepts. Indeed, Håstad’s famous lower bound technique for $\mathbf {AC}^{0}$ [13] was lifted to the setting of proof complexity in [4], yielding lower bounds for a propositional formulation of the pigeonhole principle.

Monotone proof complexity is motivated by another famous lower bound result, namely Razborov’s lower bounds on the size of negation-free circuits [22, 23] (and similar ones for formulas [16]). In this regard, there has been much investigation into the negation-free fragment of Gentzen’s sequent calculus, called $\mathsf {MLK}$ [2, 3, 6, 14]. [3] showed a quasipolynomial simulation of $\mathsf {LK}$ by $\mathsf {MLK}$ on negation-free sequents by formalising an elegant counting argument using quasipolynomial-size negation-free counting formulae. This has recently been improved to a polynomial simulation by an intricate series of results [3, 6, 14], solving a question first posed in [21]. However, note the contrast with bounded depth systems: restricting negation has a different effect on computational complexity and on proof complexity.

In this work we address a similar question for the setting of branching programs. These are (presumably) more expressive than Boolean formulas, in that they are the non-uniform counterpart of log-space ($\mathbf {L}$), as opposed to $\mathbf {NC}^{1}$. They have recently been given a proof theoretic treatment in [5]. We work within that framework, only restricting to formulas representing positive branching programs.

Positive (or ‘monotone’) branching programs have been considered several times in the literature, e.g. [12, 15], and are identical to Markov’s ‘relay-diode bipoles’ from [20]. [11, 12] give a general way of making a non-deterministic model of computation ‘positive’; in particular, a non-deterministic branching program is positive if, whenever there is a 0-transition from a node u to a node v, there is also a 1-transition from u to v. As in the earlier work [5] we implement such a criterion by using disjunction to model nondeterminism.

Contribution. We present a formal calculus $\mathsf {e}\mathsf {LNDT}^{+}$, reasoning with formula-based representations of positive branching programs, by restricting the calculus $\mathsf {e}\mathsf {LNDT}$ from [5] appropriately. We consider the ‘positive closures’ of well-known polynomial-size ‘ordered’ BPs (OBDDs) for counting functions, and show that their characteristic properties admit polynomial-size proofs in $\mathsf {e}\mathsf {LNDT}^{+}$.

As a case study, we show that these properties can be used to obtain polynomial-size proofs of the propositional pigeonhole principle, by adapting an approach of [2] for $\mathsf {MLK}$. Our main result is that $\mathsf {e}\mathsf {LNDT}^{+}$ in fact polynomially simulates $\mathsf {e}\mathsf {LNDT}$ over positive sequents. For this we again use representations of positive NBPs for counting and small proofs of their characteristic properties. At a high level we adapt the approach of [3], but there are several additional technicalities specific to our setting. In particular, we require bespoke treatments of negative literals in $\mathsf {e}\mathsf {LNDT}$ and of substitutions of (representations of) positive NBPs into (representations of) other positive NBPs.

Terminology. Throughout this work, we shall reserve the words ‘monotone’, ‘monotonicity’ etc. for semantic notions, i.e. as a property of Boolean functions. For (non-uniform) models of computation such as formulas, branching programs, circuits etc., we shall say ‘positive’ for the associated syntactic constraints, e.g. negation-freeness for the case of formulas or circuits. While many works simply say ‘monotone’ always, in particular [11, 12], let us note that the distinction we make is employed by several other authors too, e.g. [1, 10, 18, 19].

Proofs and Full Version. Proofs of all results stated in this work can be found in a preprint available at [9].

2 Preliminaries

We will use a countable set of propositional variables, written p, q etc., and Boolean constants 0 and 1, with their usual interpretations. An assignment, written $\alpha , \beta$ etc., is just a map from propositional variables to $\{0,1\}$, and a Boolean function, f, g etc., is just a map from assignments to $\{0,1\}$. We write $\alpha \le \beta$ if, for all propositional variables p, we have $\alpha (p) \le \beta (p)$. We say that a Boolean function f is monotone if $\alpha \le \beta \implies f(\alpha ) \le f(\beta )$.

In proof complexity, formally, a propositional proof system is just a polynomial-time function P from $\varSigma ^*$ to the set of propositional tautologies, for $\varSigma$ some finite alphabet. The idea is that P checks (efficiently) that an element $\sigma \in \varSigma ^*$ correctly codes a proof in the system in which case the output $P(\sigma )$ is the tautology $\sigma$ proves. Otherwise P outputs the tautology 1 by convention. We say that a propositional proof system P polynomially simulates a system Q if we can construct in polynomial-time, for each Q proof $\pi$ of A, a P-proof of A. In practice (and throughout this work) we shall avoid specifying proof systems at such a low level, leaving such formalisation implicit.

2.1 Positive Branching Programs and Their Representations

A (non-deterministic) branching program (NBP) is a (rooted) directed acyclic graph G with two distinguished sink nodes, 0 and 1, such that:

• G has a unique root node, i.e. a unique node with in-degree 0.

• Each non-sink node v of G is labelled by a propositional variable.

• Each edge e of G is labelled by a constant 0 or 1.

Definition 1

(Positive NBPs, e.g. [12]). An NBP is positive if, for every 0-edge from a node u to a node v, there is also a 1-edge from u to v.

A run of a NBP G on an assignment $\alpha$ is a maximal path beginning at the root of G consistent with $\alpha$. I.e., at a node labelled by p the run must follow an edge labelled by $\alpha (p) \in \{0,1\}$. G accepts $\alpha$ if there is a run on $\alpha$ reaching the sink 1. We extend $\alpha$ to a map from all NBPs to $\{0,1\}$ by setting $\alpha (G) = 1$ if G accepts $\alpha$. Thus each NBP computes a unique Boolean function $\alpha \mapsto \alpha (G)$.

Fact 2

A positive NBP computes a monotone Boolean function.

Example 3

(2-out-of-4 Threshold). The 2-out-of-4 Threshold function, returning 1 if at least two of its four inputs are 1, is computed by the positive NBP on the left of Fig. 1. Here 0-edges are dotted, and 1-edges are solid; the multiple 0-leaves correspond to the same sink.

Fig. 1.

Pos. NBP for 2-out-of-4 Threshold and representation by extension axioms.

Like in [5], we shall represent (positive) NBPs in proofs by means of extension variables, $e_0, e_1,\dots$ (distinguished from propositional variables). An extended non-deterministic decision tree formula (eNDT formula), written A, B etc., is generated from constants, propositional variables and extension variables by:

• If A and B are eNDT formulas then so is $(A \vee B)$.

• If A and B are eNDT formulas then so is $(ApB)$.

Disjunction, $\vee$, has its usual semantic interpretation, while $ApB$ should be interpreted as “if p then B else A”. The role of extension variables is to ‘abbreviate’ complex formulas, intuitively ‘naming’ nodes in branching programs. Their interpretation is thus determined by additional data:

Definition 4

A set of extension axioms $\mathcal A$ is a set of the form , where each $A_i$ may only contain extension variables among $e_0, \dots , e_{i-1}$.

Thanks to the subscripting condition for $\mathcal A$ above we inherit a natural induction principle (‘$\mathcal A$-induction’) for formulas over $e_0, \dots , e_{n-1}$. For instance, this means that formulas over $e_0, \dots , e_{n-1}$ indeed compute unique Boolean functions with respect to $\mathcal A$:

Definition 5

(Semantics of eNDT formulas).Satisfaction with respect to a set of extension axioms , written $\vDash _{\mathcal A}$, is a (infix) binary relation between assignments and formulas over $e_0, \dots , e_{n-1}$ defined as follows:

• $\alpha \nvDash _{\mathcal A} 0$, $\alpha \vDash _{\mathcal A} 1$ and $\alpha \vDash _{\mathcal A} p$ if $\alpha (p) = 1$.

• $\alpha \vDash _{\mathcal A} A \vee B$ if $\alpha \vDash _{\mathcal A} A$ or $\alpha \vDash _{\mathcal A} B$.

• $\alpha \vDash _{\mathcal A} ApB$ if either $\alpha (p)=0$ and $\alpha \vDash _{\mathcal A} A$, or $\alpha (p)=1$ and $\alpha \vDash _{\mathcal A} B$.

• $\alpha \vDash _{\mathcal A} e_i$ if $\alpha \vDash _{\mathcal A} A_i$.

Remark 6

(Distinguishing extension variables). Note that we do not allow decisions on extension variables, i.e. formulas may not have the form $Ae_iB$. Otherwise we would be able to represent all Boolean circuits succinctly, cf. [5].

Definition 7

(Positive formulas). An eNDT formula is positive if, for each subformula of the form $ApB$, we have $B = A \vee C$ for some C.

A set of extension axioms is positive if each $A_i$ is positive.

As expected, positive formulas over positive extension axioms represent positive NBPs, and so compute monotone Boolean functions.

Example 8

(2-out-of-4 Threshold, revisited). Returning to Example 3 earlier, the positive NBP on the left of Fig. 1 is represented by the extension variable $e_{11}$ under the extension axioms on the right of Fig. 1. Each $e_{ij}$ represents the j^th node (left to right) on the i^th row (top to bottom) for $1\le i\le 4$ and $1 \le j\le i$; for well-foundedness of the extension axioms (i.e. the subscripting condition of Definition 4), note that we may identify each $e_{ij}$ with $e_{4(4-i) + j}$.

2.2 The System $\mathsf {e}\mathsf {LNDT}$ and its Positive Fragment

We now recall the system for NBPs introduced in [5]. The language of the system $\mathsf {e}\mathsf {LNDT}$ comprises of just the eNDT formulas. A sequent is an expression $\varGamma \, \rightarrow \, \varDelta$, where $\varGamma$ and $\varDelta$ are multisets of eNDT formulas (‘$\, \rightarrow \,$’ is just a syntactic delimiter). Semantically, such a sequent is interpreted as a judgement “some formula of $\varGamma$ is false or some formula of $\varDelta$ is true”.

Definition 9

(Systems). The system $\mathsf {LNDT}$ is given by the rules in Fig. 2. An $\mathsf {LNDT}$ derivation of $\varGamma \, \rightarrow \, \varDelta$ from hypotheses $\mathcal H = \{\varGamma _i \, \rightarrow \, \varDelta _i\}_{i\in I}$ is defined as expected: it is a finite list of sequents, each being either some $\varGamma _i \, \rightarrow \, \varDelta _i$ from $\mathcal H$ or following from previous ones by rules of $\mathsf {LNDT}$, ending with $\varGamma \, \rightarrow \, \varDelta$.

An $\mathsf {e}\mathsf {LNDT}$ proof is just an $\mathsf {LNDT}$ derivation from hypotheses that are a set of extension axioms , with construed as an abbreviation for the pair of sequents $A \, \rightarrow \, B$ and $B \, \rightarrow \, A$. Furthermore, we (typically) require that the conclusion of an $\mathsf {e}\mathsf {LNDT}$ proof has no extension variables.

The size of a proof/derivation P or a formula A, written |P| or |A| respectively, is just the number of symbols occurring in it.

Our formulation of $\mathsf {e}\mathsf {LNDT}$ differs slightly from the original one in [5] in that (a) we admit Boolean constants in our language; and (b) we admit decisions only on propositional variables, not their negations. Both of these are only cosmetic, and in particular do not affect proof complexity, as observed in [5].

Fig. 2.

Rules for system $(\mathsf e)\mathsf {LNDT}$.

To define our ‘positive fragment’ of $\mathsf {e}\mathsf {LNDT}$ notice that $Ap(A\vee B)$ is semantically equivalent to $A \vee (p \wedge B)$, which motivates the following analytic ‘positive decision’ rules:

(1)

Definition 10

(System $\mathsf {e}\mathsf {LNDT}^{+}$). The system $\mathsf {e}\mathsf {LNDT}^{+}$ is defined just like $\mathsf {e}\mathsf {LNDT}$, except replacing the $p\text {-}l$ and $p\text {-}r$ rules by the positive ones above in (1). Moreover, all extension axioms and formulas occurring in a proof (in particular $\mathsf {cut}$-formulas) must be positive.

2.3 Some Basic (Meta) theorems for $\mathsf {e}\mathsf {LNDT}^{+}$

Let us first note that the set of valid positive sequents (without extension variables) is actually sufficiently expressive to be meaningful for proof complexity:

Proposition 11

Validity of extension-free positive sequents is $co \mathbf {NP}$-complete.

This follows by a basic reduction from DNF validity, expressing positive terms (i.e. conjunctions of propositional variables) by recursively using the equivalence $p \wedge A \iff 0p(0\vee A)$.

Note that our logical rules, in particular $p^{+}\text {-}l$ and $p^{+}\text {-}r$, are not only sound but also invertible: the validity of the conclusion implies the validity of each premiss. A basic bottom-up proof search argument thus gives:

Proposition 12

(Soundness and completeness).$\mathsf {e}\mathsf {LNDT}^{+}$ proves a positive sequent $\varGamma \, \rightarrow \, \varDelta$ (without extension variables) iff $\bigwedge \varGamma \supset \bigvee \varDelta$ is valid.

As an example of explicit proofs in $\mathsf {e}\mathsf {LNDT}^{+}$ (and for later use) we have:

Proposition 13

(General identity). Let be a set of positive extension axioms. There are polynomial-size $\mathsf {e}\mathsf {LNDT}^{+}$ proofs of $A \, \rightarrow \, A$, for positive formulas A containing only extension variables among $e_0, \dots , e_{n-1}$.

Proof

We construct proofs inductively according to the extension axiom set $\mathcal A$. When A is a propositional variable or Boolean constant, the required derivation is immediate by initial rule $\mathsf {id}$ or by the initial rules 0, 1 along with $\mathsf {w}\text {-}l, \mathsf {w}\text {-}r$ resp.

If $A = e_i$ for some $i<n$ or $A=B \vee C$, then we have proofs,¹

where sequents marked $IH$ are obtained by inductive hypothesis; other premisses are extension axioms from $\mathcal A$. If $A = Bp(B\vee C)$ then we have the proof:

Note that we do not formally ‘duplicate’ the subproof corresponding to $B \, \rightarrow \, B$, we simply use it twice. Similarly, the proofs of $B\, \rightarrow \, B$ and $C \, \rightarrow \, C$ may have common subproofs corresponding to, say, the same extension variable.

To evaluate proof size note that, at each step of the argument above, we add a constant number of lines of polynomial size in A and $\mathcal A$. Since the total number of steps is bounded by $|A| + \sum _{i<n} |A_i|$, we obtain polynomial-size proofs overall.

Note that the result above, together with completeness, means that we can sometimes obtain polynomial-size proofs ‘for free’: for each valid (extension-free) sequent there is a constant-size proof by completeness, Proposition 12, and by the above result, we have polynomial-size proofs for all its ‘instances’ under substitution. E.g., by simply observing semantic validity, we immediately have:

Proposition 14

(Truth conditions). Let be a set of positive extension axioms and let A and B be formulas over $e_0, \dots , e_{n-1}$. There are polynomial-size $\mathsf {e}\mathsf {LNDT}^{+}$ proofs of the following sequents with respect to $\mathcal A$:

$$ Ap(A\vee B) \, \rightarrow \, A,p \quad Ap(A\vee B) \, \rightarrow \, A,B \quad A \, \rightarrow \, Ap(A\vee B) \quad p,B \, \rightarrow \, Ap(A\vee B) $$

3 Formalising Counting Arguments in $\mathsf {e}\mathsf {LNDT}^{+}$

In this work we shall make use of monotone Boolean counting functions, namely the Threshold functions $\mathrm {Th}^{n}_{k} : \{0,1\}^n \rightarrow \{0,1\}$ by $\mathrm {Th}^{n}_{k} (b_1, \dots , b_n)=1$ if at least k of $b_1, \dots , b_n$ are 1. For a list of propositional variables $\mathbf {p} = p_1, \dots , p_n$, we can compute the function $\mathrm {Th}^{n}_{k} (\mathbf {p})$ with polynomial-size positive NBPs as follows:

Definition 15

(Thresholds). For each list $\mathbf {p}$ of propositional variables, and each integer k, we introduce an extension variable $t^{\mathbf {p}}_{k}$ and write $\mathcal {T}^{}_{}$ for the set of all extension axioms of the form (i.e. for all choices of p, $\mathbf {p}$ and k):

(2)

Example 16

Revisiting Fig. 1, note that we may visualise $t^{p_1p_2p_3p_4}_{2}$ by the program on the left. Referencing the extension axioms on the right, we may simply identify each $e_{ij}$ with $t^{p_i\cdots p_4}_{2-j+1}$ (for $1\le i \le 4)$. It is not hard to see that, in general, $t^{\mathbf {p}}_{k}$ represents a positive NBP with number of nodes and edges quadratic in $|\mathbf {p}|$.

It turns out that $\mathsf {e}\mathsf {LNDT}^{+}$ admits small proofs of several characteristic properties of the Threshold functions, which we now survey. The following result is shown by induction on $|\mathbf {p}|$, appealing to Lemma 14 for all the inductive steps.

Proposition 17

($t^{\mathbf {p}}_{k}$ is decreasing in k). There are polynomial-size $\mathsf {e}\mathsf {LNDT}^{+}$ proofs of the following sequents over extension axioms $\mathcal {T}^{}_{}$:

$$ \, \rightarrow \, t^{\mathbf {p}}_{0}, \qquad t^{\mathbf {p}}_{k+1} \, \rightarrow \, t^{\mathbf {p}}_{k}, \qquad t^{\mathbf {p}}_{k} \, \rightarrow \, \ \text {(if }k>|\mathbf {p}|\text {)} $$

The next result simplifies many of our later arguments, admitting a ‘direct’ proof peculiar to the structure of our particular threshold programs (cf., e.g., [2, 3]).

Lemma 18

There are polynomial-size $\mathsf {e}\mathsf {LNDT}^{+}$ proofs over $\mathcal {T}^{}_{}$ of $t^{\mathbf {p} q \mathbf {q}}_{k} \ \, \leftrightarrow \, \ t^{q \mathbf {p} \mathbf {q}}_{k}$.

The proof is, again, by induction on $|\mathbf {p}|$, this time using small proofs of the following ‘medial’ property for the inductive step:

$$ \begin{array}{rl} &{} (Aq(A\vee B))p((Aq(A\vee B))\vee (Cq(C\vee D))) \\ \, \leftrightarrow \, &{} (Ap(A\vee C))q((Ap(A\vee C))\vee (Bp(B\vee D) )) \end{array} $$

By repeatedly applying the above lemma, we obtain the following crucial result:

Theorem 19

(Symmetry). Let $\pi$ be a permutation of $\mathbf {p}$. Then there are polynomial-size $\mathsf {e}\mathsf {LNDT}^{+}$ proofs over $\mathcal {T}^{}_{}$ of $t^{\mathbf {p}}_{k} \ \, \leftrightarrow \, \ t^{\pi (\mathbf {p})}_{k}$.

4 Case Study: The Pigeonhole Principle

As a warm up to our main result in the next section, we will show here how we may use the previous results to obtain polynomial-size proofs of the propositional pigeonhole principle in $\mathsf {e}\mathsf {LNDT}^{+}$. In our setting, this principle is encoded as:

$$\begin{aligned} \mathsf {PHP}_{n} \ := \quad \left\{ \bigvee \limits _{j=1}^n p_{i j } \right\} _{i=1}^{n+1} \, \rightarrow \, \bigvee \limits _{j=1}^n \bigvee \limits _{i = 1}^{n} \bigvee \limits _{ i' = i+1}^{n+1} 0p_{i j }(0\vee p_{i' j }) \end{aligned}$$

(3)

It is helpful to think of the propositional variables $p_{i j }$ as expressing “pigeon i sits in hole j”. In the RHS the formulas $0p_{i j }(0\vee p_{i' j })$ are usually written as $p_{i j } \wedge p_{i' j }$ but, in the absence of conjunction, we adopt the current encoding.

We show that $\mathsf {PHP}_{n}$ admits small proofs in $\mathsf {e}\mathsf {LNDT}^{+}$ with a ‘standard’ high-level argument. We fix n throughout this section and write:

• $\mathbf {p}_{i}$ for the list $p_{i 1 } , \dots , p_{i n }$, and just $\mathbf {p}_{}$ for the list $\mathbf {p}_{1} , \dots , \mathbf {p}_{n+1}$.

• $\mathbf {p}^\intercal _{j}$ for the list $p_{1 j }, \dots , p_{n+1 j }$ and just $\mathbf {p}^\intercal _{}$ for the list $\mathbf {p}^\intercal _{1} , \dots , \mathbf {p}^\intercal _{n}$.

The notation $\mathbf {p}^\intercal _{}$ is suggestive since, construing $\mathbf {p}_{}$ as an $(n+1) \times n$ matrix of propositional variables, $\mathbf {p}^\intercal _{}$ is just the transpose $n\times (n+1)$ matrix.

Our approach towards proving $\mathsf {PHP}_{n}$ in $\mathsf {e}\mathsf {LNDT}^{+}$ (with small proofs) will be broken up into the three smaller steps. Writing $\mathsf L \mathsf {PHP}_{n}$ and $\mathsf R \mathsf {PHP}_{n}$ for the LHS and RHS, respectively, of $\mathsf {PHP}_{n}$ in (3), we will prove the following sequents:

Notice that, since $\mathbf {p}^\intercal _{}$ is just a permutation of $\mathbf {p}_{}$, we already have small proofs of (5) from Theorem 19, so we focus on the other two sequents. We will need:

Lemma 20

(Merging and splitting). There are polynomial-size $\mathsf {e}\mathsf {LNDT}^{+}$ proofs, over extension axioms $\mathcal {T}^{}_{}$, of the following sequents:

This is again proved by induction on $|\mathbf {p}|$, appealing several times to Proposition 14. (7) yields small proofs of (4), and (8) yields small proofs of (6). Finally, (4), (5) and (6) are combined by cuts to obtain:

Theorem 21

There are polynomial-size $\mathsf {e}\mathsf {LNDT}^{+}$ proofs of $\mathsf {PHP}_{n}$.

5 Positive Simulation of Non-positive Proofs

We have shown that $\mathsf {e}\mathsf {LNDT}^{+}$ can formalise basic counting arguments by giving small proofs of the pigeonhole principle. We now go further and show:

Theorem 22

$\mathsf {e}\mathsf {LNDT}^{+}$ polynomially simulates $\mathsf {e}\mathsf {LNDT}$ over positive sequents.

This section is devoted to demonstrating this result, in particular defining various intermediate systems to this end. The high-level structure of the argument is similar to that of [3], but we must make several specialisations to the current setting due to the peculiarities of eNDT formulas and extension.

5.1 Positive Normal Form of $\mathsf {e}\mathsf {LNDT}$ proofs

We first deal with non-positive formulas occurring in an $\mathsf {e}\mathsf {LNDT}$ proof. The intuition is similar to that in [3] where negations are reduced to the variables using De Morgan duality. In our setting formulas are no longer closed under duality but, nonetheless, we are able to devise a bespoke ‘positive normal form’.

First, we shall temporarily work with a presentation of $\mathsf {e}\mathsf {LNDT}$ within $\mathsf {e}\mathsf {LNDT}^{+}$ by allowing negative literals, in order to facilitate our later translations.

Definition 23

($\mathsf {e}\mathsf {LNDT}^{+}_{-}$). For each propositional variable p we introduce a distinguished propositional variable $\overline{p}$. The system $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ is defined just like $\mathsf {e}\mathsf {LNDT}^{+}$ but also allows positive decisions on variables $\overline{p}$. All syntactic positivity constraints remain. Furthermore, $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ has additional initial sequents of the forms $\ p, \overline{p} \, \rightarrow \, \,$ and $\, \, \rightarrow \, p, \overline{p}$.

Definition 24

(Positive normal form). We define a (polynomial-time) translation from an $\mathsf {e}\mathsf {LNDT}$ formula A to an $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ formula $A^{-}$ as follows:

For a multiset of formulas $\varGamma = A_1, \dots , A_n$ we write $\varGamma ^{-}:= A^{-}_1, \dots , A^{-}_n$. For a set of extension axioms , we write $\mathcal A^{-}$ for .

By induction on the length of an $\mathsf {e}\mathsf {LNDT}$ proof, we obtain:

Theorem 25

Let P be an $\mathsf {e}\mathsf {LNDT}$ proof of $\varGamma \, \rightarrow \, \varDelta$ over extension axioms $\mathcal A$. There is an $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ proof $P^{-}$ of $\varGamma ^{-}\, \rightarrow \, \varDelta ^{-}$ over extension axioms $\mathcal A^{-}$ of size polynomial in |P|.

The critical cases for the above theorem are the decision steps, since $\cdot ^{-}$ commutes with everything else. For this we appeal to another ‘truth lemma’:

Lemma 26

(Truth for $\cdot ^{-}$-translation). Let be a set of positive extension axioms and let A and B be formulas over $e_0, \dots , e_{n-1}$. There are polynomial-size $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ proofs of the following sequents over $\mathcal A^{-}$:

$$ (ApB)^{-} \, \rightarrow \, A^{-},p \quad (ApB)^{-} , p \, \rightarrow \, B^{-} \quad A^{-} \, \rightarrow \, (ApB)^{-} , p \quad p,B^{-} \, \rightarrow \, ( ApB)^{-} $$

Combining the above lemma with the original truth conditions, Proposition 14, we can show, for positive extension-free formulas A, that there are polynomial-size $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ proofs of $A^{-} \, \leftrightarrow \, A$. This is established by direct structural induction on A (which has no extension variables), and thus yields:

Corollary 27

$\mathsf {e}\mathsf {LNDT}^{+}_{-}$ polynomially simulates $\mathsf {e}\mathsf {LNDT}$, over positive sequents.

5.2 Generalised Counting Formulas

[3] relies heavily on substitution of formulas for variables in proofs of $\mathsf {LK}$. Being based on usual Boolean formulae, this is entirely unproblematic in that setting, but for us causes low-level difficulties due to the restrictions of our syntax.

Our aim is to ‘replace’ negative literals in an $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ proof by certain threshold formulas from Definition 15. However, if a literal occurs as a decision variable, then we cannot directly substitute an extension variable for it, since the syntax of $\mathsf {e}\mathsf {LNDT}$ (crucially) does not allow this. To handle this, we introduce a generalisation of our previous threshold extension variables and axioms below that accounts for all such substitution situations. To maintain well-foundedness of sets of extension axioms, cf. Definition 4, these extension variables should be considered defined mutually inductively with eNDT formulas themselves. We shall gloss over the details of this technicality in what follows.

Definition 28

(Threshold decisions). We introduce extension variables $[ {\scriptstyle A} { t^{\mathbf {p}}_{k}} {\scriptstyle ( A \vee B )} ]$ for each list $\mathbf {p}$ of propositional variables, integer k, and formulas A, B. We extend $\mathcal {T}^{}_{}$ to include all extension axioms of the following form:

(9)

Despite the notation, $[ {\scriptstyle A} { t^{\mathbf {p}}_{k}} {\scriptstyle ( A \vee B )} ]$ is, formally speaking, a single extension variable, not a decision on the extension variable $t^{\mathbf {p}}_{k}$ which, recall, our syntax does not permit. However the notation is suggestive, justified by the following counterpart of the truth conditions from Proposition 14 (proved by induction on $|\mathbf {p}|$):

Proposition 29

(Truth). There are polynomial size $\mathsf {e}\mathsf {LNDT}^{+}$ proofs over $\mathcal {T}^{}_{}$ of:

$$ [ {\scriptstyle A} { t^{\mathbf {p}}_{k}} {\scriptstyle ( A \vee B )} ] \, \rightarrow \, A , t^{\mathbf {p}}_{k} \quad [ {\scriptstyle A} { t^{\mathbf {p}}_{k}} {\scriptstyle ( A \vee B )} ] \, \rightarrow \, A , B \quad A \, \rightarrow \, [ {\scriptstyle A} { t^{\mathbf {p}}_{k}} {\scriptstyle ( A \vee B )} ] \quad t^{\mathbf {p}}_{k} , B \, \rightarrow \, [ {\scriptstyle A} { t^{\mathbf {p}}_{k}} {\scriptstyle ( A \vee B )} ] $$

5.3 ‘Substituting’ Thresholds for Negative Literals

For the remainder of this section we work with a fixed $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ proof P, over extension axioms , of a positive sequent $\varGamma \, \rightarrow \, \varDelta$, with propositional variables among $\mathbf {p} = p_0, \dots , p_{m-1}$ and extension variables among $\mathbf {e} = e_0, \dots , e_{n-1}$. Recall we are only concerned with the provable positive sequents of $\mathsf {e}\mathsf {LNDT}$, so our consideration of $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ here suffices by Corollary 27.

Throughout this section, we write $\mathbf {p}_{i}$ for $p_0, \dots , p_{i-1} , p_{i+1}, \dots , p_{m-1}$, i.e. just $\mathbf {p}$ with $p_i$ removed. We will need to define a family of intermediary systems $\mathsf {e}\mathsf {LNDT}^{+}_{k}(P)$, for each $k\ge 0$. Before that, we introduce the following translation:

Definition 30

(‘Substituting’ thresholds). We define a (polynomial-time) translation from an $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ formula A (over $\mathbf {p}$, $\overline{\mathbf {p}}$ and $\mathbf {e}$) to an $\mathsf {e}\mathsf {LNDT}^{+}$ formula $A^{k}$ (over $\mathbf {p}$, some extension variables $\mathbf {e}^k$ and extension variables from $\mathcal {T}^{}_{}$) by:

Also , and $\{B_1, \dots , B_l \}^{k}:=B_1^{k}, \dots , B_l^{k}$.

While this translation, and the threshold decisions themselves, may seem syntactically heavy, at the level of branching programs the idea is simple: the NBP represented by $A^{k}$ is obtained by substituting the NBP represented by $t^{\mathbf {p}_{i}}_{k}$ for each node labelled by $\overline{p}_i$ in the NBP represented by A. This may be visualised:

Our systems $\mathsf {e}\mathsf {LNDT}^{+}_{k}(P)$ are parametrised by the choice of $k\ge 0$, and are peculiar to $\mathcal A$, $\mathbf {p}$ and P we fixed at the beginning of this subsection:

Definition 31

$\mathsf {e}\mathsf {LNDT}^{+}_{k}(P)$ is defined just like $\mathsf {e}\mathsf {LNDT}^{+}$, but has extra initial sequents $p_i, t^{\mathbf {p}_{i}}_{k} \, \rightarrow \, \,$ and $\, \, \rightarrow \, p_i, t^{\mathbf {p}_{i}}_{k}$, and only uses extension axioms $\mathcal {T}^{}_{} \cup \mathcal A^{k}$.

By replacing every formula A in P by $A^{k}$ and locally repairing the proof:

Lemma 32

There is a $\mathsf {e}\mathsf {LNDT}^{+}_{k}(P)$ proof $P^{k}$ of $\varGamma \, \rightarrow \, \varDelta$ of size polynomial in |P|.

The critical cases for this result are positive decisions on negative literals, for which we appeal to the previously given truth conditions, Proposition 29.

5.4 Putting It All Together

In this section we stitch together the proofs obtained in each ${\mathsf {e}\mathsf {LNDT}^{+}_{k}(P)}$ for $0\le k \le m+1$ to obtain our main simulation result. Before this we will need the following result, proved by directly applying Lemmas 18 and 20.

Proposition 33

For $k\ge 0$, there are polynomial size $\mathsf {e}\mathsf {LNDT}^{+}$ proofs over $\mathcal {T}^{}_{}$ of:

By adding $t^{\mathbf {p}}_{k}$ to the LHS and $t^{\mathbf {p}}_{k+1}$ to the RHS of each sequent in $P^{k}$ from Lemma 32, replacing the additional initial sequents of $\mathsf {e}\mathsf {LNDT}^{+}_{k}(P)$ from Definition 31 by (10) and (11) resp., we obtain:

Lemma 34

For $k\ge 0$, there are polynomial size $\mathsf {e}\mathsf {LNDT}^{+}$ proofs over extension axioms $\mathcal {T}^{}_{} \cup \mathcal A^{k}$ of $t^{\mathbf {p}}_{k} , \varGamma \, \rightarrow \, \varDelta , t^{\mathbf {p}}_{k+1}$

We may now assemble the proof of our main result:

Proof (of Theorem 22)

[of Theorem 22] By Corollary 27, without loss of generality let P be an $\mathsf {e}\mathsf {LNDT}^{+}_{-}$ proof of a positive sequent $\varGamma \, \rightarrow \, \varDelta$ over extension axioms $\mathcal A$. By Lemma 34 we construct, for each $k\le n+1$, polynomial-size proofs of $t^{\mathbf {p}}_{k}, \varGamma \, \rightarrow \, \varDelta , t^{\mathbf {p}}_{k+1}$, over $\mathcal {T}^{}_{} \cup \mathcal A^{k}$, and we simply cut them all together as follows:

 

The resulting proof is indeed an $\mathsf {e}\mathsf {LNDT}^{+}$ proof of the required sequent, in particular over extension axioms $\mathcal {T}^{}_{} \cup \mathcal A^{0} \cup \mathcal A^{1} \cup \cdots \cup \mathcal A^{m+1}$.