# Proof complexity of positive branching programs

Anupam Das∗ and Avgerinos Delkos∗ ∗University of Birmingham, UK

###### 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, just 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 [10]: $\mathit{co}\mathbf{NP}=\mathbf{NP}$ if and
only if there is a propositional proof system (suitably defined) 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}$:
find superpolynomial lower bounds for stronger and stronger systems until we
have found a general method (see, e.g., [7, 20]).

Systems of interest in proof complexity are typically motivated by analogous
results from circuit complexity and other non-uniform models of computation.
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
techniques for $\mathbf{AC}^{0}$ [14] have been lifted to the setting of proof
complexity, yielding lower bounds for a propositional formulation of the
pigeonhole principle [4] via a refined version of the switching lemma.

_Monotone_ proof complexity is motivated by another famous lower bound result,
namely Razborov’s lower bounds on the size of $\neg$-free circuits [27, 28]
(and similar ones for formulas [18]). In this regard, there has been much
investigation into the negation-free fragment of Gentzen’s sequent calculus,
called $\mathsf{MLK}$ [2, 3, 16, 6]. [3] showed a quasipolynomial simulation
of $\mathsf{LK}$ by $\mathsf{MLK}$ on $\neg$-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, 16, 6], solving a question first posed in
[26]. However, note the contrast with bounded depth systems: restricting
negation has different effects on computational complexity and 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], in particular addressing proof complexity. We work within
that framework, only restricting ourselves to formulas (with extension)
representing _positive_ branching programs.

Positive (or ‘monotone’) branching programs have been considered several times
in the literature, e.g. [13, 17]. They are identical to Markov’s ‘relay-diode
bipoles’ from [25]. [13, 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. As far as we are aware, there is no other work investigating
the proof complexity of systems based on positive/monotone branching programs.

###  1.1. Contribution

We present a formal proof 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 (iterated) substitutions of representations of
positive NBPs into other positive NBPs.

###  1.2. A terminological convention

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 [12, 13], let us
note that the distinction we make is employed by several other authors too,
e.g. [1, 23, 22, 11].

##  2\. Preliminaries on proof complexity and branching programs

In this section we will recall some of the content from [5]. The reader
familiar with that work can safely omit this section, though they should take
note of our conventions in the definition of the system
$\mathsf{e}\mathsf{LNDT}$, cf. Remark 2.10.

Throughout this work we will use a countable set of _propositional variables_
, written $p,q$ etc., and _Boolean constants_ $0$ and $1$.

An _assignment_ is just a map $\alpha$ from propositional variables to
$\\{0,1\\}$. For all intents and purposes we may assume that they have finite
support, e.g. nonzero only on variables occurring in a formula or proof. We
extend an assignment $\alpha$ to the constants in the natural way, setting
$\alpha(0)=0$ and $\alpha(1)=1$.

A _Boolean function_ is just a map from (finitely supported) assignments to
$\\{0,1\\}$.

###  2.1. Proof complexity

In proof complexity, a (formal) _propositional proof system_ is just a
polynomial-time function $P$ from $\Sigma^{*}$ to the set of propositional
tautologies, where $\Sigma$ is some finite alphabet. Intuitively, the elements
$\sigma\in\Sigma^{*}$ code proofs in the system, while $P$ itself is a
(efficient) ‘proof-checking’ algorithm that verifies that $\sigma$ is indeed a
correctly written proof, and if so returns its conclusion, i.e. the theorem it
proves. If not, it just returns $1$, by convention.

The significance of this definition is due to the following result from [10]:

######  Theorem 2.1 (Cook-Reckhow).

There is a propositional proof system with polynomial-size proofs of each
tautology if and only if $\mathit{co}\mathbf{NP}=\mathbf{NP}$.

In practice, this ‘Cook-Reckhow definition’ of a propositional proof system
covers all well-studied proof systems for propositional logic, under suitable
codings. We shall refrain from giving any of these codings explicitly in this
work, as is standard for proof complexity. However, let us point out that the
systems we consider routinely admit polynomial-time proof checking in the way
described above, and so indeed constitute formal propositional proof systems.

See [19, 8, 21] for more comprehensive introductions to proof complexity.

###  2.2. Non-deterministic branching programs

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$.

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 a
propositional variable $p$ the run must follow an edge labelled by
$\alpha(p)\in\\{0,1\\}$.

We say that $G$ _accepts_ $\alpha$ if there is a run on $\alpha$ reaching the
sink $1$. We may extend $\alpha$ to a map from all NBPs to $\\{0,1\\}$ by
setting $\alpha(G)=1$ just if $G$ accepts $\alpha$. In this way, each NBP
_computes_ a unique Boolean function $\alpha\mapsto\alpha(G)$.

A comprehensive introduction to (variants of) branching programs and their
underlying theory can be found in, e.g., [30].

######  Example 2.2 (OBDD for 2-out-of-4 Exact).

The 2-out-of-4 Exact function, which returns 1 just if precisely two of its
four arguments are 1, is computed by the branching program in Fig. 1.
$0$-edges are indicated dotted and $1$-edges are indicated solid, a convention
that we adopt throughout this work. Formally, each $0$-leaf corresponds to the
same sink.

Note that this program is deterministic: there is exactly one 0-edge and one
1-edge outgoing from each non-sink node. It is also _ordered_ : all the
variables appear in the same order in each path. Thus its semantics may be
verified by checking that every path leading to the 1-sink has exactly two
1-edges and vice versa.

$p_{1}$$p_{2}$$p_{2}$$p_{3}$$p_{3}$$p_{3}$$p_{4}$$p_{4}$$p_{4}$$p_{4}$$0$$0$$1$$0$$0$
Figure 1. An OBDD computing the 2-out-of-4 Exact function. $0$-edges are
indicated dotted, and $1$ edges are indicated solid.

###  2.3. Representation of NBPs by extended formulas

Since we will be working in formal proof systems, we shall use a natural
representation of NBPs by ‘formulas with extension’, just like in [5]. For
this, we shall make use of _extension variables_ $e_{0},e_{1},e_{2},\dots$ in
our language.

An _extended non-deterministic decision tree_ formula, or _eNDT_ formula,
written $A,B$ etc., is generated from propositional variables, extension
variables and constants by disjunction, $\vee$, and _decisions_ : for formulas
$A,B$ and $p$ a propositional variable, $(ApB)$ is a formula. Intuitively,
$(ApB)$ expresses “if $p$ then $B$ else $A$”.

As usual, we often omit external brackets of formulas and write long
disjunctions without internal brackets, under associativity. The _size_ of a
formula $A$, written $|A|$, is the number of symbols occurring in $A$.

######  Remark 2.3 (Distinguishing extension variables).

Note that we formally distinguish extension variables from propositional
variables. This is for the same technical reasons as in [5] we must not allow
extension variables to be decision variables, i.e. we forbid formulas of the
form $Ae_{i}B$. If we did allow this then we would be able to express all
Boolean circuits succinctly, whereas the current convention ensures that we
only express NBPs.

The semantics of (non-extended) NDT formulas under an assignment will be
standard. With extension variables, however, the interpretation is
parametrised by a set of _extension axioms_ , allowing extension variables to
‘abbreviate’ more complex formulas.

######  Definition 2.4 (Extension axioms).

A _set of extension axioms_ $\mathcal{A}$ is a set of the form
$\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$, where each $A_{i}$
may only contain extension variables among $e_{0},\dots,e_{i-1}$.

######  Definition 2.5 (Semantics of eNDT formulas).

_Satisfaction_ with respect to a set of extension axioms
$\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}\mathcal{A}_{i}\\}_{i<n}$,
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$ and $\alpha\vDash_{\mathcal{A}}1$.

  * •

$\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}$.

######  Example 2.6 (2-out-of-4 Exact, revisited).

Recall Example 2.2 and the branching program from Fig. 1. Under the semantics
above, we may represent this branching program as $e_{11}$ under the following
extension axioms:

$\begin{array}[]{r@{\ \extiff\ }l}e_{11}\
\mbox{\Large$\,\leftrightarrow\,$}&e_{21}p_{1}e_{22}\\\ e_{21}\
\mbox{\Large$\,\leftrightarrow\,$}&e_{31}p_{2}e_{32}\\\ e_{22}\
\mbox{\Large$\,\leftrightarrow\,$}&e_{32}p_{2}e_{33}\end{array}\qquad\begin{array}[]{r@{\
\extiff\ }l}e_{31}\ \mbox{\Large$\,\leftrightarrow\,$}&e_{41}p_{3}e_{42}\\\
e_{32}\ \mbox{\Large$\,\leftrightarrow\,$}&e_{42}p_{3}e_{43}\\\ e_{33}\
\mbox{\Large$\,\leftrightarrow\,$}&e_{43}p_{3}e_{44}\end{array}\qquad\begin{array}[]{r@{\
\extiff\ }l}e_{41}\ \mbox{\Large$\,\leftrightarrow\,$}&0p_{4}0\\\ e_{42}\
\mbox{\Large$\,\leftrightarrow\,$}&0p_{4}1\\\ e_{43}\
\mbox{\Large$\,\leftrightarrow\,$}&1p_{4}0\\\ e_{44}\
\mbox{\Large$\,\leftrightarrow\,$}&0p_{4}0\end{array}$

Each $e_{ij}$ represents the $j$th node (left to right) on the $i$th row (top
to bottom). Note that, in order to strictly comply with the subscripting
condition on extension axioms, we may identify $e_{ij}$ with $e_{4i-j}$.

Note that the notion $\vDash_{\mathcal{A}}$ is indeed well-defined, thanks to
the subscripting conditions on sets of extension axioms: intuitively, each
$e_{i}$ abbreviates a formula containing only extension variables among
$e_{0},\dots,e_{i-1}$, and so on. More generally:

######  Remark 2.7 ($\mathcal{A}$-induction).

Given a set of extension axioms
$\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$ we may
define a strict partial order $<_{\mathcal{A}}$ on formulas over
$e_{0},\dots,e_{n-1}$ by:

  * •

$p<_{\mathcal{A}}ApB$ and $A<_{\mathcal{A}}ApB$ and $B<_{\mathcal{A}}ApB$.

  * •

$A<_{\mathcal{A}}A\vee B$ and $B<_{\mathcal{A}}A\vee B$.

  * •

$A_{i}<_{\mathcal{A}}e_{i}$, for each $i<n$.

Notice that $<_{\mathcal{A}}$ is indeed well-founded by the condition that
each $A_{i}$ must contain only extension variables among
$e_{0},\dots,e_{i-1}$. Thus we may carry out arguments and make definitions by
induction on $<_{\mathcal{A}}$, which we shall simply refer to as
‘$\mathcal{A}$-induction’.

We can now see Definition 2.5 above of $\vDash_{\mathcal{A}}$ as just a
definition by $\mathcal{A}$-induction. In this way, fixing some set of
extension axioms
$\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$, each
eNDT formula $A$ over $e_{0},\dots,e_{n-1}$ computes a unique Boolean function
$f:\alpha\mapsto 1$ just if $\alpha\vDash_{\mathcal{A}}A$. In this case, we
may say that $A$ _computes_ $f$ _with respect to_ $\mathcal{A}$.

Since many of our arguments will be based on $\mathcal{A}$-induction, let us
make the following observation for complexity matters:

######  Observation 2.8 (Complexity of $\mathcal{A}$-induction).

Let $\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$ be
a set of extension axioms and $A$ contain only extension variables among
$e_{0},\dots,e_{n-1}$. Then
$|\\{B<_{\mathcal{A}}A\\}|\leq|A|+\sum\limits_{i<n}|A_{i}|$ and, if
$B<_{\mathcal{A}}A$, then $|B|\leq\max(|A|,|A_{0}|,\dots,|A_{n-1}|)$.

###  2.4. The system $\mathsf{e}\mathsf{LNDT}$

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 $\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$, where
$\Gamma$ and $\Delta$ are multisets of eNDT formulas (‘$\,\rightarrow\,$’ is
just a syntactic delimiter). Semantically, such a sequent is interpreted as a
judgement “some formula of $\Gamma$ is false or some formula of $\Delta$ is
true”.

Notice that the semantic interpretation of eNDT formulas we gave in Definition
2.5 means that $ApB$ is logically equivalent to both $(\overline{p}\wedge
A)\vee(p\wedge B)$ and $(\overline{p}\supset A)\wedge(p\supset B)$. It is this
observation which naturally yields the following system for eNDT sequents from
[5]:

######  Definition 2.9 (Systems $\mathsf{LNDT}$ and
$\mathsf{e}\mathsf{LNDT}$).

The system $\mathsf{LNDT}$ is given by the rules in Fig. 2. An $\mathsf{LNDT}$
_derivation_ of $\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$ from _hypotheses_
$\mathcal{H}=\\{\Gamma_{i}\mbox{\Large$\,\rightarrow\,$}\Delta_{i}\\}_{i\in
I}$ is defined as expected: it is a finite list of sequents, each either some
$\Gamma_{i}\mbox{\Large$\,\rightarrow\,$}\Delta_{i}$ from $\mathcal{H}$ or
following from previous ones by rules of $\mathsf{LNDT}$, ending with
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$.

An $\mathsf{e}\mathsf{LNDT}$ _proof_ is just an $\mathsf{LNDT}$ derivation
from hypotheses that are a set of extension axioms
$\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}(e_{j})_{j<i}\\}_{i<n}$;
here we construe $A\mbox{\Large$\,\leftrightarrow\,$}B$ as an abbreviation for
the pair of sequents $A\mbox{\Large$\,\rightarrow\,$}B$ and
$B\mbox{\Large$\,\rightarrow\,$}A$. We require that the conclusion of an
$\mathsf{e}\mathsf{LNDT}$ proof is free of extension variables.

The _size_ of a proof or derivation $P$, written $|P|$, is just the number of
symbols occurring in it.

Note that, despite the final condition that conclusions of
$\mathsf{e}\mathsf{LNDT}$ proofs are free of extension variables, we may
sometimes consider intermediate ‘proofs’ with extension variables in the
conclusions. In these cases we will always make explicit the underlying set of
extension axioms.

Initial sequents and cut:

$\scriptstyle 0\;$ $0\mbox{\Large$\,\rightarrow\,$}$ $\scriptstyle 1\;$
$\mbox{\Large$\,\rightarrow\,$}1$ $\scriptstyle\mathsf{id}\;$
$p\mbox{\Large$\,\rightarrow\,$}p$
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A$$\Gamma,A\mbox{\Large$\,\rightarrow\,$}\Delta$
$\scriptstyle\mathsf{cut}\;$ $\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$

Structural rules:

$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$
$\scriptstyle\mathsf{w}\text{-}l\;$
$\Gamma,A\mbox{\Large$\,\rightarrow\,$}\Delta$
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$
$\scriptstyle\mathsf{w}\text{-}r\;$
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A$
$\Gamma,A,A\mbox{\Large$\,\rightarrow\,$}\Delta$
$\scriptstyle\mathsf{c}\text{-}l\;$
$\Gamma,A\mbox{\Large$\,\rightarrow\,$}\Delta$
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A,A$
$\scriptstyle\mathsf{c}\text{-}r\;$
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A$

Logical rules:

$\Gamma,A\mbox{\Large$\,\rightarrow\,$}\Delta,p$$\Gamma,p,B\mbox{\Large$\,\rightarrow\,$}\Delta$
$\scriptstyle p\text{-}l\;$ $\Gamma,ApB\mbox{\Large$\,\rightarrow\,$}\Delta$
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A,p$$\Gamma,p\mbox{\Large$\,\rightarrow\,$}\Delta,B$
$\scriptstyle p\text{-}r\;$ $\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,ApB$

$\Gamma,A\mbox{\Large$\,\rightarrow\,$}\Delta$$\Gamma,B\mbox{\Large$\,\rightarrow\,$}\Delta$
$\scriptstyle\vee\text{-}l\;$ $\Gamma,A\vee
B\mbox{\Large$\,\rightarrow\,$}\Delta$
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A,B$ $\scriptstyle\vee\text{-}r\;$
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A\vee B$

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

######  Remark 2.10 (Differences from original $\mathsf{e}\mathsf{LNDT}$).

In order to ease the exposition, we have slightly adjusted the definition of
$\mathsf{e}\mathsf{LNDT}$. The variations are minor and, in particular, the
current presentation is polynomially equivalent to that of [5]. Nonetheless,
let us survey these differences here:

  * •

We admit constants $0$ and $1$ within the language. As mentioned in [5], this
does not significantly affect proof size, since $0$ can be encoded as
$pp\overline{p}$ and $1$ as $\overline{p}pp$, for an arbitrary propositional
variable $p$.

  * •

We do not have symbols for negative literals, to facilitate our later
definition of ‘positivity’. Note, however, that $\overline{p}$ is equivalent
to the formula $1p0$ in our language.

  * •

More generally, we admit decisions on only positive literals, not negative
ones, for the same reason. Again, a formula $A\overline{p}B$ may be replaced
by the equivalent one $BpA$.

As shown in [5], the system $\mathsf{e}\mathsf{LNDT}$ is adequate for
reasoning about non-deterministic decision trees.

######  Proposition 2.11 (Soundness and completeness, [5]).

$\mathsf{e}\mathsf{LNDT}$ proves a sequent
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$ (without extension variables) if
and only if $\bigwedge\Gamma\supset\bigvee\Delta$ is valid.

One sanity check here is that the set of valid extension-free sequents is
indeed $\mathit{co}\mathbf{NP}$-complete, and so comprises an adequate logic
for proof complexity. This is shown explicitly in [5], but is also subsumed by
the analogous statement for the ‘positive’ fragment of this language that we
consider in the next section, namely Proposition 3.13.

##  3\. Monotone functions and positive proofs

In this section we shall recall monotone Boolean functions and positive NBPs
that compute them, and introduce a restriction of the system
$\mathsf{e}\mathsf{LNDT}$ that reasons only with such positive NBPs.

###  3.1. Monotone Boolean functions and positive programs

A Boolean function $f:\\{0,1\\}^{n}\to\\{0,1\\}$ is usually called ‘monotone’
if, whenever $\mathbf{c}\in\\{0,1\\}^{n}$ is obtained from
$\mathbf{b}\in\\{0,1\\}^{n}$ by flipping $0$s to $1$s, we have
$f(\mathbf{b})\leq f(\mathbf{c})$. Rephrasing this into our setting we have:

######  Definition 3.1 (Monotonicity).

Given assignments $\alpha,\beta$, we write $\alpha\leq\beta$ if, for all
propositional variables $p$, we have $\alpha(p)\leq\beta(p)$, i.e. if
$\alpha(p)=1$ then also $\beta(p)=1$. A Boolean function $f$ is _monotone_ if
$\alpha\leq\beta\implies f(\alpha)\leq f(\beta)$.

There are several known non-uniform ‘positive’ models for computing monotone
functions, e.g. $\neg$-free circuits or formulas, monotone span programs [17],
and, in our setting, positive NBPs:

######  Definition 3.2 (Positive NBPs, e.g. [13]).

A 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$.

######  Fact 3.3.

A positive NBP computes a monotone Boolean function.

###### Proof sketch.

Suppose $\alpha\leq\beta$ and $\alpha(G)=1$. Let
$\mathbf{v}=(v_{0},\dots,v_{n})$ be an accepting run, where $v_{n}=1$ and, for
$i<n$, each $v_{i}$ is labelled by some propositional variable $p_{i}$. We
argue that $\mathbf{v}$ is also an accepting run of $\beta$. The critical case
is when $\alpha(p_{i})=0$ but $\beta(p_{i})=1$; in which case the positivity
condition on $G$ ensures that there is nonetheless a $1$-edge from $v_{i}$ to
$v_{i+1}$. ∎

###  3.2. A digression on monotone complexity and closures

NBPs are a non-uniform version of non-deterministic logspace
($\mathbf{N}\mathbf{L}$): each $\mathbf{N}\mathbf{L}$ language is accepted by
a polynomial-size family of NBPs and, conversely, the evaluation problem for
NBPs is complete for $\mathbf{N}\mathbf{L}$. In particular,
$\mathbf{N}\mathbf{L}$ is precisely the class of languages accepted by, say,
$\mathbf{L}$-uniform families of NBPs.

Naturally, our positive NBPs correspond to a positive version of
$\mathbf{N}\mathbf{L}$ too, called $\mathbf{m}\mathbf{N}\mathbf{L}$ by Grigni
and Sipser in [13, 12]. Those works present a comprehensive development of
positive models of computation and their underlying theory. In particular
there is a well-behaved notion of positive non-deterministic Turing machine
based on a similar idea to that of positive NBPs: roughly speaking, whenever a
transition is available when reading a $0$, the same transition is available
when reading a $1$. It turns out that the class
$\mathbf{m}\mathbf{N}\mathbf{L}$, induced by this machine model restricted to
logarithmic size work tapes, is equivalent to the class of languages
recognised by $\mathbf{L}$-uniform families of positive NBPs.

One natural construction that is available in the NBP setting (as opposed to,
say, Boolean formulas or circuits) is the notion of a ‘positive closure’,
which we shall work with later.

######  Definition 3.4 (Positive closure of a NBP).

For a NBP $G$ with $0$-edges $E_{0}$ and $1$-edges $E_{1}$, we write $G^{+}$
for the NBP with the same vertex set and $0$-edges $E_{0}$ and $1$-edges
$E_{0}\cup E_{1}$. I.e., $G^{+}$ is obtained from $G$ by adding, for every
$0$-edge from a node $u$ to a node $v$, a $1$-edge from $u$ to $v$ (if there
is not already one).

######  Example 3.5.

The positive closure of the OBDD for 2-out-of-4 Exact from Fig. 1 is given in
Fig. 3.

$p_{1}$$p_{2}$$p_{2}$$p_{3}$$p_{3}$$p_{3}$$p_{4}$$p_{4}$$p_{4}$$p_{4}$$0$$0$$1$$0$$0$
Figure 3. Positive closure of the OBDD for 2-out-of-4 Exact from Fig. 1.

Note that $G^{+}$ is always a positive NBP. Thus this construction gives us a
‘canonical’ positive version of a NBP. In many (but not all) cases, we can
precisely characterise the semantic effect of taking positive closures, thanks
to the following notion:

######  Definition 3.6 (Monotone closure).

For a Boolean function $f$, we define its _monotone closure_ $m(f)$, by
$m(f)(\alpha)=1$ just if $\exists\beta\leq\alpha.f(\beta)=1$.

The point of the monotone closure of a function $f$ is that it is the ‘least’
monotone function that dominates $f$, i.e. such that $f\leq m(f)$. There is
also a dual notion of the ‘greatest’ monotone function dominated by $f$ which
is similarly related to ‘positive co-NBPs’, but we shall not make use of it in
this work.

In certain cases, the positive closure of a NBP $G$ computes _precisely_ the
monotone closure of (the function computed by) $G$. Call a NBP _read-once_ if,
on each path, each propositional variable appears at most once. We have:

######  Proposition 3.7 ([13]).

Let $G$ be a read-once NBP computing a Boolean function $f$. Then $G^{+}$
computes $m(f)$.

###### Proof sketch.

Suppose $m(f)(\alpha)=1$, and let $\mathbf{v}$ be an accepting run of $G$ on
some $\beta\leq\alpha$. Notice that $\mathbf{v}$ is also accepting for $G^{+}$
on $\alpha$: at any node $v_{i}$ labelled by some $p$ on which $\alpha$ and
$\beta$ differ, i.e. $\beta(p)=0$ and $\alpha(p)=1$, by positivity we also
have a $1$-edge $v_{i}$ to $v_{i+1}$.

Now suppose that $G^{+}$ accepts $\alpha$ by a run $\mathbf{v}$ of nodes
labelled by $\mathbf{p}$ respectively. Define $\beta\leq\alpha$ by
$\beta(p_{i})=1$ if there is no $0$-edge from $v_{i}$ to $v_{i+1}$ in $G$,
otherwise $\beta(p_{i})=0$. Note that $\beta$ is indeed well-defined, by the
read-once property, and indeed $\beta\leq\alpha$ by definition of $G^{+}$. ∎

In particular, the above result holds when $G$ is ‘ordered’ (an ‘OBDD’), i.e.
propositional variables occur in the same relative order in each path through
$G$. We will see an example of this with counting functions later in Section
4.

######  Example 3.8 (Monotone closure of Exact).

The monotone closure of the 2-out-of-4 Exact function is the 2-out-of-4
Threshold function, returning 1 if _at least_ two of its four inputs are 1.
Since the branching programs from Fig. 1 were read-once, we have by
Proposition 3.7 above that the branching programs from Fig. 3 compute the
2-out-of-4 Threshold function.

Note, however, that the result does not hold for arbitrary NBPs. In fact,
there is no feasible notion of ‘positive closure’ on NBPs that always computes
the monotone closure, due to the following result:

######  Theorem 3.9 ([13]).

There are monotone functions computed by polynomial-size families of NBPs, but
no polynomial-size family of positive NBPs.

Note that this result is the analogue for the NBP model to Razborov’s seminal
results for the circuit model [27, 28]. This result follows by establishing a
non-uniform version of
‘$\mathbf{m}\mathbf{N}\mathbf{L}\neq\mathit{co}\mathbf{m}\mathbf{N}\mathbf{L}$’;
in particular there is a monotone $\mathit{co}\mathbf{N}\mathbf{L}$ language
(namely non-reachability in a graph) computed by no polynomial-size family of
positive NBPs. The result above now follows by the Immerman-Szelepcsényi
theorem that $\mathbf{N}\mathbf{L}=\mathit{co}\mathbf{N}\mathbf{L}$ [15, 29]
and $\mathbf{N}\mathbf{L}$-completeness of NBP evaluation.

###  3.3. Representations of positive branching programs

Let us now return to our representation of NBPs by extended formulas. Recall
that we implement non-determinism using disjunction, so we may duly define the
corresponding notion of positivity at the level of eNDT formulas themselves:

######  Definition 3.10 (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
$\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$ is
_positive_ if each $A_{i}$ is positive.

Positive eNDT formulas, under positive extension axioms, are just
representations of positive NBPs. Notice in particular that a positive
decision $Ap(A\vee B)$ is semantically equivalent to $A\vee(p\wedge B)$, which
is monotone in $A$, $p$ and $B$. Since every other symbol/connective also
computes a monotone function we may thus directly obtain the analogue of Fact
3.3:

######  Proposition 3.11.

Suppose $\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$
is a set of positive extension axioms. Each positive eNDT formula $A$ over
$e_{0},\dots,e_{n-1}$ computes a monotone Boolean function with respect to
$\mathcal{A}$.

This argument proceeds by $\mathcal{A}$-induction on $A$ and is routine. Other
than the fact that all connectives are monotone, we also rely on the fact that
we have no negative literals in our language.

###  3.4. A system for positive branching programs

The semantic equivalence of $Ap(A\vee B)$ and $A\vee(p\wedge B)$ motivates the
following ‘positive decision’ rules:

(1)
$\Gamma,A\mbox{\Large$\,\rightarrow\,$}\Delta$$\Gamma,p,B\mbox{\Large$\,\rightarrow\,$}\Delta$
$\scriptstyle p^{+}\text{-}l\;$ $\Gamma,Ap(A\vee
B)\mbox{\Large$\,\rightarrow\,$}\Delta$
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A,p$$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A,B$
$\scriptstyle p^{+}\text{-}r\;$
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,Ap(A\vee B)$

Naturally, these rules satisfy the subformula property and, moreover, are
derivable in $\mathsf{e}\mathsf{LNDT}$ by small proofs. As expected, none of
the arguments $A$, $p$ or $B$ above ‘change sides’ by the rules above. This is
due to the fact that positive decisions are, indeed, monotone, unlike general
decisions, for which the $x$ may change sides. Note, however, that the two
rules above are not ‘dual’, in the logical sense, unlike general decisions.
This is because positive decisions are no longer self-dual.

######  Definition 3.12 (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 Equation (1). Moreover, all extension
axioms and formulas occurring in a proof (in particular cut-formulas) must be
positive.

As for $\mathsf{e}\mathsf{LNDT}$, we should verify that the set of valid
positive sequents (without extension variables) is actually sufficiently
expressive to be meaningful for proof complexity, i.e. that they are
$\mathit{co}\mathbf{NP}$-complete. While this is fairly immediate for other
positive systems, such as $\mathsf{MLK}$, it is not so clear here so we give a
self-contained argument.

######  Proposition 3.13.

The set of valid positive sequents (without extension variables) is
$\mathit{co}\mathbf{NP}$-complete.

###### Proof.

By the Cook-Levin theorem [9, 24], we know that the validity problem for DNFs
is $\mathit{co}\mathbf{NP}$-complete, so we will show how to encode a DNF as
an equi-valid positive sequent.

First, note that we may express positive terms (i.e. conjunctions of
propositional variables) as positive NDT formulas by exploiting the
equivalence $0x(0\vee B)\iff 0\lor(x\land B)\iff x\land B$. Recursively
applying this equivalence we obtain:

(2) $\bigwedge_{i=1}^{m}p_{i}\iff 0p_{1}(0\vee 0p_{2}(0\vee(\cdots
0p_{m-1}(0\vee p_{m})\cdots)))$

Let us write $\mathrm{Conj}(p_{1},\dots,p_{m})$ for the positive NDT formula
on the right above.

Now, fix a DNF instance $A$ over propositional variables $p_{1},\dots,p_{k}$
and let $A^{\prime}$ be obtained by replacing each negative literal
$\overline{p}_{i}$ by a fresh (positive) propositional variable
$p_{i}^{\prime}$. Write
$A^{\prime}=\bigvee\limits_{i=1}^{n}\bigwedge\mathbf{p}_{i}$, where each
$\mathbf{p}_{i}$ is a sequence of propositional variables (among
$p_{1},\dots,p_{k},p_{1}^{\prime},\dots,p_{k}^{\prime}$). Now we have that the
following positive NDT sequent is equi-valid with $A$, as required:

$p_{1}\lor p_{1}^{\prime},\dots,p_{k}\lor
p_{k}^{\prime}\mbox{\Large$\,\rightarrow\,$}\mathrm{Conj}(\mathbf{p}_{1}),\dots,\mathrm{Conj}(\mathbf{p}_{n})\qed$

Finally, our calculus $\mathsf{e}\mathsf{LNDT}^{+}$ is indeed adequate for
reasoning about positive sequents:

######  Proposition 3.14 (Soundness and completeness).

$\mathsf{e}\mathsf{LNDT}^{+}$ proves a positive sequent
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$ (without extension variables) if
and only if $\bigwedge\Gamma\supset\bigvee\Delta$.

###### Proof sketch.

Similarly to the argument in [BDK20] for $\mathsf{e}\mathsf{LNDT}$, we may
proceed by cut-free proof search, and will not make use of any extension
variables. Notice that each logical rule is _invertible_ , i.e. the validity
of the conclusion implies the validity of each premiss. Moreover, each premiss
(of a logical rule) has fewer connectives than the conclusion. Thus, bottom-
up, we may simply repeatedly apply the logical steps until we reach sequents
of only atomic formulae. Such a sequent is valid if and only if there is a $0$
on the LHS, a $1$ on the RHS, or some propositional variable $p$ on both
sides. Each of these cases may be derived from initial sequents using the
weakening rules, $\mathsf{w}\text{-}l$ and $\mathsf{w}\text{-}r$. ∎

######  Remark 3.15 (Completeness with respect to extension axioms).

While it is standard to only consider extended proofs over extension-free
theorems, let us point out that we also have a stronger version of
completeness with respect to sets of (positive) extension axioms.

Given a set of (positive) extension axioms
$\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$, a
(positive) formula $A$ over $e_{0},\dots,e_{n-1}$ is _$\mathcal{A}$ -valid_
if, for every assignment $\alpha$, we have $\alpha\vDash_{\mathcal{A}}A$ (cf.
Definition 2.5). The same argument as in Proposition 3.14 can now be applied
to show completeness for $\mathcal{A}$-valid positive sequents by proofs using
the extension axioms $\mathcal{A}$. The only difference is that, when we reach
a connective-free sequent (bottom-up), extension variables may also occur, not
just propositional variables and constants. In this case we must use the
extension axioms to unwind the extension variables and continue the proof
search algorithm. Termination of this process now follows by appealing to
$\mathcal{A}$-induction (cf. Remark 2.7).

###  3.5. Some basic theorems

Let us now present some basic theorems of $\mathsf{e}\mathsf{LNDT}^{+}$, which
will all have polynomial-size proofs. These will be useful for our later
arguments and, at the same time, exemplify how we will conduct proof
complexity theoretic reasoning in what follows.

Let us first point out an expected property, that we can polynomially derive a
general identity rule from the atomic version included in the definition of
$\mathsf{e}\mathsf{LNDT}^{+}$. Albeit a simple observation, it has the
consequence that applying substitutions of formulas for variables in proofs
has only polynomial overhead in proof size.

######  Proposition 3.16 (General identity).

Let $\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$ be
a set of positive extension axioms. There are polynomial-size
$\mathsf{e}\mathsf{LNDT}^{+}$ proofs of $A\mbox{\Large$\,\rightarrow\,$}A$,
for positive formulas $A$ containing only extension variables among
$e_{0},\dots,e_{n-1}$.

###### Proof.

We construct a (dag-like) proof of the required sequent by
$\mathcal{A}$-induction. More precisely, for each such $A$, we construct a
polynomial-size proof containing sequents $B\mbox{\Large$\,\rightarrow\,$}B$
for each $B\leq_{\mathcal{A}}A$ by $\mathcal{A}$-induction on $A$.

  * •

If $A$ is a propositional variable then we are done by the rule $\mathsf{id}$.

  * •

If $A=0$ then we have:

$\scriptstyle 0\;$ $0\mbox{\Large$\,\rightarrow\,$}$
$\scriptstyle\mathsf{w}\text{-}r\;$ $0\mbox{\Large$\,\rightarrow\,$}0$

  * •

If $A=1$ then we have:

$\scriptstyle 1\;$ $\mbox{\Large$\,\rightarrow\,$}1$
$\scriptstyle\mathsf{w}\text{-}l\;$ $1\mbox{\Large$\,\rightarrow\,$}1$

  * •

If $A=e_{i}$ for some $i<n$, then we extend the proof obtained by the
inductive hypothesis as follows,

$e_{i}\mbox{\Large$\,\rightarrow\,$}A_{i}$ $\scriptstyle\mathit{IH}\;$
$A_{i}\mbox{\Large$\,\rightarrow\,$}A_{i}$
$A_{i}\mbox{\Large$\,\rightarrow\,$}e_{i}$ $\scriptstyle 2\mathsf{cut}\;$
$e_{i}\mbox{\Large$\,\rightarrow\,$}e_{i}$

where the sequent marked $\mathit{IH}$ is obtained by the inductive
hypothesis, and the other premisses are extension axioms from $\mathcal{A}$.

  * •

If $A=B\vee C$ then we extend the proof obtained by the inductive hypothesis
as follows,

$\scriptstyle\mathit{IH}\;$ $B\mbox{\Large$\,\rightarrow\,$}B$
$\scriptstyle\mathsf{w}\text{-}r\;$ $B\mbox{\Large$\,\rightarrow\,$}B,C$
$\scriptstyle\mathit{IH}\;$ $C\mbox{\Large$\,\rightarrow\,$}C$
$\scriptstyle\mathsf{w}\text{-}r\;$ $C\mbox{\Large$\,\rightarrow\,$}B,C$
$\scriptstyle\vee\text{-}l\;$ $B\vee C\mbox{\Large$\,\rightarrow\,$}B,C$
$\scriptstyle\vee\text{-}r\;$ $B\vee C\mbox{\Large$\,\rightarrow\,$}B\vee C$

where sequents marked $\mathit{IH}$ are obtained by the inductive hypothesis.

  * •

If $A=Bx(B\vee C)$ then we extend the proof obtained by the inductive
hypothesis as follows:

$\scriptstyle\mathit{IH}\;$ $B\mbox{\Large$\,\rightarrow\,$}B$
$\scriptstyle\mathsf{w}\text{-}r\;$ $B\mbox{\Large$\,\rightarrow\,$}B$
$\scriptstyle\mathit{IH}\;$ $B\mbox{\Large$\,\rightarrow\,$}B$
$\scriptstyle\mathsf{w}\text{-}r\;$ $B\mbox{\Large$\,\rightarrow\,$}B,C$
$\scriptstyle p^{+}\text{-}r\;$ $B\mbox{\Large$\,\rightarrow\,$}Bp(B\vee C)$
$\scriptstyle\mathsf{id}\;$ $p\mbox{\Large$\,\rightarrow\,$}p$
$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$
$p,C\mbox{\Large$\,\rightarrow\,$}B,p$ $\scriptstyle\mathit{IH}\;$
$C\mbox{\Large$\,\rightarrow\,$}C$
$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$
$p,C\mbox{\Large$\,\rightarrow\,$}B,C$ $\scriptstyle p^{+}\text{-}r\;$
$p,C\mbox{\Large$\,\rightarrow\,$}Bp(B\vee C)$ $\scriptstyle p^{+}\text{-}l\;$
$Bp(B\vee C)\mbox{\Large$\,\rightarrow\,$}Bp(B\vee C)$

where sequents marked $\mathit{IH}$ are obtained by the inductive hypothesis.

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}$. Thus a
polynomial bound follows by 2.8. ∎

Notice, in the final step above, that we do not formally ‘duplicate’ the
subproof for $B\mbox{\Large$\,\rightarrow\,$}B$ as this, recursively applied,
could cause an exponential blowup. This is why the construction by
$\mathcal{A}$-induction is phrased as constructing a _single_ proof that
contains all ‘smaller’ instances of identity already, with inductive steps
just extending that proof. In what follows we shall be less rigorous when
constructing formal proofs in this way, simply saying that we ‘construct them
by $\mathcal{A}$-induction’. We shall also typically leave proof complexity
analysis like the one above implicit.

For our later simulations, the following ‘truth conditions’ for positive
decisions will prove useful:

######  Proposition 3.17 (Truth conditions).

Let $\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$ 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}$:

  1. (1)

$Ap(A\vee B)\mbox{\Large$\,\rightarrow\,$}A,p$

  2. (2)

$Ap(A\vee B)\mbox{\Large$\,\rightarrow\,$}A,B$

  3. (3)

$A\mbox{\Large$\,\rightarrow\,$}Ap(A\vee B)$

  4. (4)

$p,B\mbox{\Large$\,\rightarrow\,$}Ap(A\vee B)$

###### Proof.

We give the proofs explicitly:

$\lx@cref{creftype~refnum}{item:truth-posdec-implies-0case}:\
{{}{}\vbox{\hbox{\kern
0.45128pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
9.64592pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
15.54436pt\hbox{\hbox{\hbox{$$}}}\kern 15.54436pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to31.08873pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}A$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 4.73782pt}\kern 1.43518pt\hbox{\kern 3.87323pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to40.56439pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern
3.87323pt\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}A,p$}\kern 0.0pt$}}}}}\kern
0.0pt}\kern 10.00002pt}\hbox{\kern
25.07887pt\hbox{\vbox{\offinterlineskip\hbox{\kern 3.62677pt\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
13.07559pt\hbox{\hbox{\hbox{$$}}}\kern 13.07559pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to26.1512pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$p\mbox{\Large$\,\rightarrow\,$}p$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 12.23782pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to50.62685pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$p,B\mbox{\Large$\,\rightarrow\,$}A,p$}\kern 0.0pt$}}}}}\kern
0.0pt}}}}\kern 1.43518pt\hbox{\kern 13.51915pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
p^{+}\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to126.27013pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
36.61856pt\hbox{\hbox{$Ap(A\vee B)\mbox{\Large$\,\rightarrow\,$}A,p$}}\kern
23.09941pt}}}\kern 0.0pt}}}\qquad\lx@cref{creftype~refnum}{item:truth-posdec-
implies-1case}:\ {{}{}\vbox{\hbox{\kern
0.45128pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
11.1737pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
15.54436pt\hbox{\hbox{\hbox{$$}}}\kern 15.54436pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to31.08873pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}A$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 6.26561pt}\kern 1.43518pt\hbox{\kern 2.34544pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to43.61995pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern
2.34544pt\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}A,B$}\kern 0.0pt$}}}}}\kern
0.0pt}\kern 10.00002pt}\hbox{\kern
25.07887pt\hbox{\vbox{\offinterlineskip\hbox{\kern 2.09898pt\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
16.13115pt\hbox{\hbox{\hbox{$$}}}\kern 16.13115pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to32.26231pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$B\mbox{\Large$\,\rightarrow\,$}B$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 10.71004pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to53.6824pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$p,B\mbox{\Large$\,\rightarrow\,$}A,B$}\kern 0.0pt$}}}}}\kern
0.0pt}}}}\kern 1.43518pt\hbox{\kern 13.51915pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
p^{+}\text{-}l\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to132.38124pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
38.14635pt\hbox{\hbox{$Ap(A\vee B)\mbox{\Large$\,\rightarrow\,$}A,B$}}\kern
24.6272pt}}}\kern 0.0pt}}}$ $\lx@cref{creftype~refnum}{item:truth-0case-
implies-posdec}:\ {{}{}\vbox{\hbox{\kern
1.57744pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
9.64592pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
15.54436pt\hbox{\hbox{\hbox{$$}}}\kern 15.54436pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to31.08873pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}A$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 4.73782pt}\kern 1.43518pt\hbox{\kern 3.87323pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to40.56439pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern
3.87323pt\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}A,p$}\kern 0.0pt$}}}}}\kern
0.0pt}\kern 10.00002pt}\hbox{\kern
11.1737pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
15.54436pt\hbox{\hbox{\hbox{$$}}}\kern 15.54436pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to31.08873pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}A$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 6.26561pt}\kern 1.43518pt\hbox{\kern 2.34544pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to43.61995pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern
2.34544pt\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}A,B$}\kern 0.0pt$}}}}}\kern
0.0pt}}}}\kern 1.43518pt\hbox{\kern 13.51915pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
p^{+}\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to107.7035pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
32.07309pt\hbox{\hbox{$A\mbox{\Large$\,\rightarrow\,$}Ap(A\vee B)$}}\kern
18.55394pt}}}\kern 0.0pt}}}\qquad\lx@cref{creftype~refnum}{item:truth-1case-
implies-posdec}:\ {{}{}\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
25.07887pt\hbox{\vbox{\offinterlineskip\hbox{\kern 3.62677pt\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
13.07559pt\hbox{\hbox{\hbox{$$}}}\kern 13.07559pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to26.1512pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$p\mbox{\Large$\,\rightarrow\,$}p$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 12.23782pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to50.62685pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$p,B\mbox{\Large$\,\rightarrow\,$}A,p$}\kern 0.0pt$}}}}}\kern
0.0pt}\kern 10.00002pt}\hbox{\kern
25.07887pt\hbox{\vbox{\offinterlineskip\hbox{\kern 2.09898pt\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
16.13115pt\hbox{\hbox{\hbox{$$}}}\kern 16.13115pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to32.26231pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$B\mbox{\Large$\,\rightarrow\,$}B$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 10.71004pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to53.6824pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$p,B\mbox{\Large$\,\rightarrow\,$}A,B$}\kern 0.0pt$}}}}}\kern
0.0pt}}}}\kern 1.43518pt\hbox{\kern 25.07887pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
p^{+}\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to139.38814pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
54.4439pt\hbox{\hbox{$p,B\mbox{\Large$\,\rightarrow\,$}Ap(A\vee B)$}}\kern
29.36502pt}}}\kern 0.0pt}}}$

where the steps marked $\mathsf{id}$ are derivable by Proposition 3.16. ∎

Notice that, given that we have polynomial-size proofs for general identity,
Proposition 3.16, the result above also just follows immediately from semantic
validity of the sequents Item 1-Item 4 and completeness of
$\mathsf{e}\mathsf{LNDT}^{+}$, Proposition 3.14, by simply substituting the
formulas $A$ and $B$ for appropriate constant-size instances of Item 1-Item 4.
We gave the argument explicitly to exemplify formal proofs of the system
$\mathsf{e}\mathsf{LNDT}^{+}$. We shall, however, make use of the
aforementioned observation in the remainder of this work.

######  Example 3.18 (A positive ‘medial’).

Branching programs enjoy elegant symmetries. For instance, in our eNDT
notation, we have validity of the following pair of sequents,

$(AqB)p(CqD)\ \mbox{\Large$\,\leftrightarrow\,$}\ (ApC)q(BpD)$

corresponding to a certain permutations of nodes in NBPs.

We also have a _positive_ version of the law above, namely:

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

The validity of this equivalence can be seen by noticing that each side is
equivalent to $A\vee(p\wedge C)\vee(q\wedge B)\vee(p\wedge q\wedge D)$. By
completeness and substitution, we thus have polynomial-size proofs of (3).

Finally, we will make use of the following consequence of the truth
conditions:

######  Corollary 3.19.

There are polynomial size $\mathsf{e}\mathsf{LNDT}^{+}$ derivations of

$\Gamma,Ap(A\vee
B)\mbox{\Large$\,\rightarrow\,$}\Delta,A^{\prime}p(A^{\prime}\vee B^{\prime})$

from hypotheses $\Gamma,A\mbox{\Large$\,\rightarrow\,$}\Delta,A^{\prime}$ and
$\Gamma,B\mbox{\Large$\,\rightarrow\,$}\Delta,B^{\prime}$, over any positive
extension axioms including all extension variables occurring in $A$ and $B$.

###### Proof.

We give the derivation below:

$\Gamma,A\mbox{\Large$\,\rightarrow\,$}\Delta,A^{\prime}$ Proposition
3.17.Item 3
$A^{\prime}\mbox{\Large$\,\rightarrow\,$}A^{\prime}p(A^{\prime}\vee
B^{\prime})$ $\scriptstyle\mathsf{cut}\;$
$\Gamma,A\mbox{\Large$\,\rightarrow\,$}\Delta,A^{\prime}p(A^{\prime}\vee
B^{\prime})$ $\Gamma,B\mbox{\Large$\,\rightarrow\,$}\Delta,B^{\prime}$
Proposition 3.17.Item 4
$p,B^{\prime}\mbox{\Large$\,\rightarrow\,$}A^{\prime}p(A^{\prime}\vee
B^{\prime})$ $\scriptstyle\mathsf{cut}\;$
$\Gamma,p,B\mbox{\Large$\,\rightarrow\,$}\Delta,A^{\prime}p(A^{\prime}\vee
B^{\prime})$ $\scriptstyle p^{+}\text{-}l\;$ $\Gamma,Ap(A\vee
B)\mbox{\Large$\,\rightarrow\,$}\Delta,A^{\prime}p(A^{\prime}\vee B^{\prime})$

Note that we have omitted several structural steps, namely
$\mathsf{w}\text{-}l,\mathsf{w}\text{-}r$ above $\mathsf{cut}$-steps, to match
contexts. We will typically continue to omit these, freely using ‘context
splitting’ and ‘context sharing’ behaviour, under structural rules. ∎

##  4\. Programs for counting and their basic properties

Let us now consider some of the Boolean counting functions that appeared in
our earlier examples more formally. The _Exact_ functions
$\mathrm{Ex}^{n}_{k}:\\{0,1\\}^{n}\to\\{0,1\\}$ are defined by:

$\mathrm{Ex}^{n}_{k}(b_{1},\dots,b_{n})=1\quad\iff\quad\sum\limits_{i=1}^{n}b_{i}\,=\,k$

I.e. $\mathrm{Ex}^{n}_{k}(b_{1},\dots,b_{n})=1$ just if _exactly_ $k$ of
$b_{1},\dots,b_{n}$ are $1$.

Taking the monotone closures of these functions (cf. Definition 3.6), we
obtain the _Threshold_ functions
$\mathrm{Th}^{n}_{k}:\\{0,1\\}^{n}\to\\{0,1\\}$ by:

$\mathrm{Th}^{n}_{k}(b_{1},\dots,b_{n})=1\quad\iff\quad\sum\limits_{i=1}^{n}b_{i}\,\geq\,k$

I.e. $\mathrm{Th}^{n}_{k}(b_{1},\dots,b_{n})=1$ just if _at least_ $k$ of
$b_{1},\dots,b_{n}$ are $1$.

For consistency with the exposition so far, given a list
$\mathbf{p}=p_{0},\dots,p_{n-1}$ of propositional variables, we construe
$\mathrm{Ex}^{n}_{k}(\mathbf{p})$ as a Boolean function from assignments to
Booleans, writing, say, $\mathrm{Ex}^{n}_{k}(\mathbf{p})(\alpha)$ for its
(Boolean) output. Similarly for $\mathrm{Th}^{n}_{k}(\mathbf{p})$.

###  4.1. OBDDs for Exact and their representations as eDTs

It is well-known that counting functions like those above are computable by
‘ordered’ branching programs, or ‘OBDDs’ (see, e.g., [30]). These are
deterministic branching programs where variables occur in the same relative
order on each path. For instance we give an OBDD for
$\mathrm{Ex}^{n}_{k}(p_{1},\dots,p_{n})$ in Figure 4.

$p_{1}$$p_{2}$$p_{2}$$p_{3}$$p_{3}$$p_{3}$$\vdots$⋮⋮$p_{n}$$p_{n}$$p_{n}$$0$$0$$1$$0$$0$$0$
Figure 4. An ‘ordered’ branching program (OBDD) for
$\mathrm{Ex}^{n}_{k}(p_{1},\dots,p_{n})$, where there are $k$ $0$s to the left
of the $1$, and $n-k$ to the right.

Thanks to determinism, we can formalise these programs as ($\vee$-free) eDT
formulas as follows:

######  Definition 4.1 (eDTs for Exact).

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

(4)
$\begin{array}[]{c@{\quad\extiff\quad}ll}e^{\varepsilon}_{0}\hfil\quad\mbox{\Large$\,\leftrightarrow\,$}&1&\\\
e^{\varepsilon}_{k}\hfil\quad\mbox{\Large$\,\leftrightarrow\,$}&0&\text{if
$k\neq 0$}\\\
e^{p\mathbf{p}}_{k}\hfil\quad\mbox{\Large$\,\leftrightarrow\,$}&e^{\mathbf{p}}_{k}pe^{\mathbf{p}}_{k-1}\end{array}$

where we write $\varepsilon$ for the empty list.

Note that, even though $\mathcal{E}$ is an infinite set, we may use it as the
underlying set of extension axioms for proofs, with the understanding that
only finitely many will actually ever be used in a particular proof. We will
typically not explicitly compute this set, but such a consideration will be
subsumed by our analysis of proof complexity.

While the extension variables above (and their axioms) do not strictly follow
the subscripting conditions from Definition 2.4, we may understand them to be
‘names’ for the appropriate subscripting. It suffices to establish the well-
foundedness of the extension axiom set in (4), which is clear by induction on
the length of the superscript. We implicitly assume here, and for other well-
founded extension axioms, that appropriately small subscripts are assigned to
extension variables to satisfy the subscripting condition and to not
contribute significantly to proof complexity.

######  Proposition 4.2.

Let $\mathbf{p}=(p_{1},\dots,p_{n})$. $e^{\mathbf{p}}_{k}$ computes
$\mathrm{Ex}^{n}_{k}(\mathbf{p})$, with respect to $\mathcal{E}$.

###### Proof.

We show that
$\alpha\vDash_{\mathcal{E}}e^{\mathbf{p}}_{k}\iff\mathrm{Ex}^{n}_{k}(\mathbf{p})(\alpha)=1$
by induction on the length $n$ of the list $\mathbf{p}$. If $n=0$ then
$\mathrm{Ex}^{0}_{k}(\,)$ attains the value $1$ just if $k=0$, so the result
is immediate from the first two axioms of (4). For the inductive step we have:

$\begin{array}[]{rc@{\ \iff\ \
}ll}\alpha\vDash_{\mathcal{E}}e^{p\mathbf{p}}_{k}&&\alpha\vDash_{\mathcal{E}}e^{\mathbf{p}}_{k}pe^{\mathbf{p}}_{k-1}&\text{by
\eqref{eq:exact-ext-axs} and \lx@cref{creftype~refnum}{dfn:sat-endt-wrt-
extax}}\\\ \vskip 3.0pt plus 1.0pt minus
1.0pt\cr&&\begin{cases}\alpha\vDash_{\mathcal{E}}e^{\mathbf{p}}_{k}&\alpha(p)=0\\\
\alpha\vDash_{\mathcal{E}}e^{\mathbf{p}}_{k-1}&\alpha(p)=1\end{cases}&\\\
\vskip 3.0pt plus 1.0pt minus
1.0pt\cr&&\begin{cases}\mathrm{Ex}^{n}_{k}(\mathbf{p})(\alpha)=1&\alpha(p)=0\\\
\mathrm{Ex}^{n}_{k-1}(\mathbf{p})(\alpha)=1&\alpha(p)=1\end{cases}&\text{by
inductive hypothesis}\\\ \vskip 3.0pt plus 1.0pt minus
1.0pt\cr&&\mathrm{Ex}^{n+1}_{k}(p,\mathbf{p})(\alpha)=1&\qed\end{array}$

###  4.2. Programs for Threshold via positive closure

Notice that, since the Exact programs we considered were OBDDs which are, in
particular, read-once, the semantic characterisation of positive closure by
monotone closure from Proposition 3.7 from applies. Looking back to Figure 4,
the positive closures we are after (as NBPs) are given in Figure 5. Realising
this directly as eNDT formulas and extension axioms we obtain the following:

$p_{1}$$p_{2}$$p_{2}$$p_{3}$$p_{3}$$p_{3}$$\vdots$⋮⋮$p_{n}$$p_{n}$$p_{n}$$0$$0$$1$$0$$0$$0$$\ldots$$\ldots$
Figure 5. The positive closure of the OBDD for Exact from Figure 4, computing
$\mathrm{Th}^{n}_{k}(p_{1},\dots,p_{n})$. Again, there are $k$ $0$s to the
left of the $1$, and $n-k$ to the right.

######  Definition 4.3 (Positive eNDTs for Threshold).

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$):

(5)
$\begin{array}[]{c@{\quad\extiff\quad}ll}t^{\varepsilon}_{0}\hfil\quad\mbox{\Large$\,\leftrightarrow\,$}&1&\\\
t^{\varepsilon}_{k}\hfil\quad\mbox{\Large$\,\leftrightarrow\,$}&0&\text{if
$k\neq 0$}\\\
t^{p\mathbf{p}}_{k}\hfil\quad\mbox{\Large$\,\leftrightarrow\,$}&t^{\mathbf{p}}_{k}p(t^{\mathbf{p}}_{k}\vee
t^{\mathbf{p}}_{k-1})\end{array}$

Again, even though $\mathcal{T}$ is an infinite set, we shall typically write
$\mathsf{e}\mathsf{LNDT}^{+}$ proofs with respect to this set of extension
axioms, with the understanding that only finitely many are ever used in any
particular proof. Again, we will typically not explicitly compute this set,
but such a consideration will be subsumed by our analysis of proof complexity.

Note that the extension variables $t^{\mathbf{p}}_{k}$ and extension axioms
$\mathcal{T}$ above are just the positive closures of $e^{\mathbf{p}}_{k}$ and
$\mathcal{E}$ earlier, within the eNDT setting. Thus, as a consequence of
Proposition 3.7 we have that, for each non-negative $k$, $t^{\mathbf{p}}_{k}$
computes exactly the threshold function $\mathrm{Th}^{n}_{k}(\mathbf{p})$ with
respect to $\mathcal{T}$.

######  Corollary 4.4.

If $k\geq 0$, then $t^{\mathbf{p}}_{k}$ computes
$\mathrm{Th}^{n}_{k}(\mathbf{p})$, with respect to $\mathcal{T}$.

Note that, for $k$ negative, we could have alternatively set
$t^{\varepsilon}_{k}$ to be $1$. We could have also simply set
$t^{\mathbf{p}}_{0}$ to be $1$ for arbitrary $\mathbf{p}$. Instead, we have
chosen to systematically take the positive closure of the aforementioned Exact
programs, to make our exposition more uniform.

###  4.3. Small proofs of basic counting properties

Our main results rely on having small proofs of characteristic properties of
counting formulae, which we duly give in this section.

First we need to establish a basic monotonicity property:

######  Proposition 4.5 ($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}$:

  1. (1)

$\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}}_{0}$

  2. (2)

$t^{\mathbf{p}}_{k+1}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}}_{k}$

  3. (3)

$t^{\mathbf{p}}_{k}\mbox{\Large$\,\rightarrow\,$}$ whenever $k>|\mathbf{p}|$

###### Proof.

We proceed by induction on the length of $\mathbf{p}$. In the base case, when
$\mathbf{p}=\varepsilon$, all three properties follow easily from
$\mathcal{T}$ initial sequents, weakening and cuts.

For the inductive steps, we construct polynomial-size proofs as follows:

$\begin{array}[]{rl}\text{\lx@cref{creftype~refnum}{item:thr-0-true}}\ :&\
\begin{array}[]{r@{\ \seqar\ }ll}\
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}}_{0}&\text{by the inductive
hypothesis}\\\ \
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}}_{0}p(t^{\mathbf{p}}_{0}\vee
t^{\mathbf{p}}_{-1})&\text{by
\lx@cref{creftype~refnum}{Truth}.\lx@cref{creftype~refnum}{item:truth-0case-
implies-posdec} }\\\ \
\mbox{\Large$\,\rightarrow\,$}&t^{p\mathbf{p}}_{0}&\text{by extension axioms
$\mathcal{T}$}\end{array}\\\ \vskip 6.0pt plus 2.0pt minus
2.0pt\cr\text{\lx@cref{creftype~refnum}{item:thr-k+1-implies-thr-k}}\ :&\
\begin{array}[]{r@{\ \seqar\ }ll}t^{p\mathbf{p}}_{k+1}\
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}}_{k+1}x(t^{\mathbf{p}}_{k+1}\vee
t^{\mathbf{p}}_{k})&\text{by extension axioms $\mathcal{T}$}\\\ \
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}}_{k}p(t^{\mathbf{p}}_{k}\vee
t^{\mathbf{p}}_{k-1})&\text{by inductive hypotheses and
\lx@cref{creftype~refnum}{mon-replacing-result}}\\\ \
\mbox{\Large$\,\rightarrow\,$}&t^{p\mathbf{p}}_{k}&\text{by extension axioms
$\mathcal{T}$ again}\end{array}\\\ \vskip 6.0pt plus 2.0pt minus
2.0pt\cr\text{\lx@cref{creftype~refnum}{item:thr-big-false}}\ :&\
\begin{array}[]{r@{\ \seqar\ }ll}t^{p\mathbf{p}}_{k}\
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}}_{k}p(t^{\mathbf{p}}_{k}\vee
t^{\mathbf{p}}_{k-1})&\text{by extension axioms $\mathcal{T}$ }\\\ \
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}}_{k},t^{\mathbf{p}}_{k-1}&\text{by
\lx@cref{creftype~refnum}{Truth}.\lx@cref{creftype~refnum}{item:truth-posdec-
implies-1case} }\\\ \
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}}_{k-1}&\text{by
\lx@cref{creftype~refnum}{item:thr-k+1-implies-thr-k} and contraction}\\\ \
\mbox{\Large$\,\rightarrow\,$}&&\text{by inductive
hypothesis}\qed\end{array}\end{array}$

The arguments above should be read by obtaining each sequent by the
justification given on the right, possibly with some cuts and structural
rules.

Note that Corollary 3.19 allows us to apply previously proven implications or
equivalences ‘deeply’ within a formula. We will use such reasoning throughout
this work, but shall typically omit further mentioning such uses of Corollary
3.19 to lighten the exposition.

For the complexity bound, note that only polynomially many lines occur: we
only require $k+1$ instantiations of the all the sequents above, one for each
choice of threshold $i\leq k$. This sort of complexity analysis will usually
suffice for later arguments, in which case we shall suppress them unless
further justification is required.

One of the key points we shall exploit in what follows is the provable
_symmetry_ of $t^{\mathbf{p}}_{k}$, in terms of the the ordering of
$\mathbf{p}$. We shall establish this through a series of results, beginning
by showing a form of ‘case analysis’ on a propositional variable occurring in
a list:

######  Lemma 4.6 (Case analysis).

There are polynomial-size $\mathsf{e}\mathsf{LNDT}^{+}$ proofs of,

$t^{\mathbf{p}q\mathbf{q}}_{k}\ \mbox{\Large$\,\leftrightarrow\,$}\
t^{q\mathbf{p}\mathbf{q}}_{k}$

over the extension axioms $\mathcal{T}$.

###### Proof.

We proceed by induction on the length of $\mathbf{p}$. The base case, when
$\mathbf{p}$ is empty, follows immediately by general identity, Proposition
3.16.

For the inductive step we construct polynomial-size proofs as follows:

$\begin{array}[]{rll}&t^{p\mathbf{p}q\mathbf{q}}_{k}&\\\
\mbox{\Large$\,\leftrightarrow\,$}&t^{\mathbf{p}q\mathbf{q}}_{k}p(t^{\mathbf{p}q\mathbf{q}}_{k}\vee
t^{\mathbf{p}q\mathbf{q}}_{k-1})&\text{by $\mathcal{T}$}\\\
\mbox{\Large$\,\leftrightarrow\,$}&t^{q\mathbf{p}\mathbf{q}}_{k}p(t^{q\mathbf{p}\mathbf{q}}_{k}\vee
t^{q\mathbf{p}\mathbf{q}}_{k-1})&\text{by $\mathit{IH}$ and
\lx@cref{creftype~refnum}{mon-replacing-result}}\\\
\mbox{\Large$\,\leftrightarrow\,$}&t^{\mathbf{p}\mathbf{q}}_{k}q(t^{\mathbf{p}\mathbf{q}}_{k}\vee
t^{\mathbf{p}\mathbf{q}}_{k-1})p(t^{\mathbf{p}\mathbf{q}}_{k}q(t^{\mathbf{p}\mathbf{q}}_{k}\vee
t^{\mathbf{p}\mathbf{q}}_{k-1})\vee
t^{\mathbf{p}\mathbf{q}}_{k-1}q(t^{\mathbf{p}\mathbf{q}}_{k-1}\vee
t^{\mathbf{p}\mathbf{q}}_{k-2}))&\text{by $\mathcal{T}$}\\\
\mbox{\Large$\,\leftrightarrow\,$}&t^{\mathbf{p}\mathbf{q}}_{k}p(t^{\mathbf{p}\mathbf{q}}_{k}\vee
t^{\mathbf{p}\mathbf{q}}_{k-1})q(t^{\mathbf{p}\mathbf{q}}_{k}p(t^{\mathbf{p}\mathbf{q}}_{k}\vee
t^{\mathbf{p}\mathbf{q}}_{k-1})\vee
t^{\mathbf{p}\mathbf{q}}_{k-1}p(t^{\mathbf{p}\mathbf{q}}_{k-1}\vee
t^{\mathbf{p}\mathbf{q}}_{k-2}))&\text{by \lx@cref{creftype~refnum}{pos-
medial}}\\\
\mbox{\Large$\,\leftrightarrow\,$}&t^{p\mathbf{p}\mathbf{q}}_{k}q(t^{p\mathbf{p}\mathbf{q}}_{k}\vee
t^{p\mathbf{p}\mathbf{q}}_{k-1})&\text{by $\mathcal{T}$ }\\\
\mbox{\Large$\,\leftrightarrow\,$}&t^{qp\mathbf{p}\mathbf{q}}_{k}&\text{by
$\mathcal{T}$}\qed\end{array}$

Similarly to the proof of Proposition 4.5, the above argument should be read
as providing polynomial-size proofs ‘in both directions’, by the
justifications given on the right. Note that, we restrict cedents to
singletons when using $\,\leftrightarrow\,$ in this way, to avoid ambiguity of
the comma delimiter. Polynomial proof size is, again, immediate by inspection
on the number of lines.

######  Theorem 4.7 (Symmetry).

Let $\pi$ be a permutation of $\mathbf{p}$. Then there are polynomial-size
$\mathsf{e}\mathsf{LNDT}^{+}$ proofs over the extension axioms $\mathcal{T}$
of:

$t^{\mathbf{p}}_{k}\ \mbox{\Large$\,\leftrightarrow\,$}\
t^{\pi(\mathbf{p})}_{k}$

###### Proof.

Write $\mathbf{p}=p_{1}\cdots p_{n}$ and write $\pi(\mathbf{p})=q_{1}\cdots
q_{n}$. We construct polynomial-size proofs by repeatedly applying Lemma 4.6
as follows:

$\begin{array}[]{rcll}t^{\mathbf{p}}_{k}&\mbox{\Large$\,\leftrightarrow\,$}&t^{q_{n}\mathbf{p}^{n}}_{k}&\text{by
\lx@cref{creftype~refnum}{thresh-case-analysis}}\\\
&\mbox{\Large$\,\leftrightarrow\,$}&t^{q_{n-1}q_{n}\mathbf{p}^{n-1,n}}_{k}&\text{by
\lx@cref{creftype~refnum}{thresh-case-analysis}}\\\ &\vdots&&\\\
&\mbox{\Large$\,\leftrightarrow\,$}&t^{q_{1}\cdots q_{n}}_{k}&\text{by
\lx@cref{creftype~refnum}{thresh-case-analysis}}\\\
&\mbox{\Large$\,\leftrightarrow\,$}&t^{\pi(\mathbf{p})}_{k}&\text{by
definition of $\mathbf{q}$ }\end{array}$

where $\mathbf{p}^{i,\dots,n}$ is just $\mathbf{p}$ with the elements
$q_{i},\dots,q_{n}$ removed, otherwise preserving relative order of the
propositional variables. ∎

##  5\. Case study: the pigeonhole principle

The _pigeonhole principle_ is usually encoded in propositional logic by a
family of $\neg$-free sequents of the following form:

$\bigwedge\limits_{i=1}^{n+1}\bigvee\limits_{j=1}^{n}p_{ij}\mbox{\Large$\,\rightarrow\,$}\bigvee\limits_{j=1}^{n}\bigvee\limits_{i=1}^{n}\bigvee\limits_{i^{\prime}=i+1}^{n+1}(p_{ij}\land
p_{i^{\prime}j})$

Here it is useful to think of the propositional variables $p_{ij}$ as
expressing “pigeon $i$ sits in hole $j$”. In this way the left-hand side (LHS)
above expresses that each pigeon $1,\dots,n+1$ sits in some hole $1,\dots,n$,
and the right-hand side (RHS) expresses that there is some hole occupied by
two (distinct) pigeons. Note that this encoding allows the mapping from
pigeons to holes to be ‘multi-functional’, i.e. the LHS is allows for a pigeon
to sit in multiple holes.

In the setting of $\mathsf{e}\mathsf{LNDT}^{+}$ we may not natively express
conjunctions, so we adopt a slightly different encoding. Being a sequent, the
outermost conjunctions on the LHS above can simply be replaced by commas; the
subformulas $p_{ij}\wedge p_{i^{\prime}j}$ may be encoded as $0p_{ij}(0\vee
p_{i^{\prime}j})$.

Thus we shall work with the following encoding of the pigeonhole principle
throughout this section:

######  Definition 5.1 (Pigeonhole principle).

$\mathsf{PHP}_{n}$ is the following positive sequent:

$\left\\{\bigvee\limits_{j=1}^{n}p_{ij}\right\\}_{i=1}^{n+1}\mbox{\Large$\,\rightarrow\,$}\bigvee\limits_{j=1}^{n}\bigvee\limits_{i=1}^{n}\bigvee\limits_{i^{\prime}=i+1}^{n+1}0p_{ij}(0\vee
p_{i^{\prime}j})$

We write $\mathsf{L}\mathsf{PHP}_{n}$ and $\mathsf{R}\mathsf{PHP}_{n}$ for the
LHS and RHS, respectively, of $\mathsf{PHP}_{n}$.

###  5.1. Summary of proof structure

The main result of this section is:

######  Theorem 5.2.

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

At a high level, we shall employ a traditional proof structure for proving
$\mathsf{PHP}_{n}$, specialising somewhat to our setting for certain
intermediate results. Before surveying this, let us introduce some notation.

######  Notation 5.3.

We fix $n\in\mathbb{N}$ throughout this section and write:

  * •

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

  * •

$\mathbf{p}^{\intercal}_{j}$ for the list $p_{1j},\dots,p_{n+1j}$ 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, proving the following sequents respectively:

  1. (1)

$\mathsf{L}\mathsf{PHP}_{n}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}}_{n+1}$

  2. (2)

$t^{\mathbf{p}}_{n+1}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}^{\intercal}}_{n+1}$

  3. (3)

$t^{\mathbf{p}^{\intercal}}_{n+1}\mbox{\Large$\,\rightarrow\,$}\mathsf{R}\mathsf{PHP}_{n}$

Notice that, since $\mathbf{p}^{\intercal}$ is just a permutation of
$\mathbf{p}$, we already have small proofs of Item 2 from Theorem 4.7. In the
next two subsections we shall focus on the other two implications, for which
the following lemma will be quite useful:

######  Lemma 5.4 (Merging and splitting threshold arguments).

There are polynomial-size $\mathsf{e}\mathsf{LNDT}^{+}$ proofs, over extension
axioms $\mathcal{T}$ of the following sequents:

  1. (1)

$t^{\mathbf{p}}_{k},t^{\mathbf{q}}_{l}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}\mathbf{q}}_{k+l}$

  2. (2)

$t^{\mathbf{p}\mathbf{q}}_{k+l}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}}_{k+1},t^{\mathbf{q}}_{l}$

###### Proof.

We proceed by induction on the length of $\mathbf{p}$. In the base case, when
$\mathbf{p}=\varepsilon$, we have two cases for Item 1:

  * •

if $k=0$ then
$t^{\varepsilon}_{0},t^{\mathbf{q}}_{l}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{q}}_{l}$
follows by $\mathsf{id}$ and $\mathsf{w}\text{-}l$.

  * •

if $k\neq 0$ then we have an axiom
$t^{\varepsilon}_{k}\mbox{\Large$\,\rightarrow\,$}0$ from $\mathcal{T}$,
whence
$t^{\varepsilon}_{k},t^{\mathbf{q}}_{l}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{q}}_{k+l}$
follows by $0$, $\mathsf{cut}$ and weakenings.

For Item 2, we have polynomial-size proofs of
$t^{\mathbf{q}}_{k+l}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{q}}_{l}$ already
from Proposition 4.5, whence we obtain
$t^{\mathbf{q}}_{k+l}\mbox{\Large$\,\rightarrow\,$}t^{\varepsilon}_{k+1},t^{\mathbf{q}}_{l}$
by $\mathsf{w}\text{-}r$.

For the inductive step we shall appeal to Corollary 3.19. First, for Item 1,
by the inductive hypothesis we already have a polynomial-size proof of:

$\begin{array}[]{r@{ \ \seqar\ }l}t^{\mathbf{p}}_{k},t^{\mathbf{q}}_{l}\
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}\mathbf{q}}_{k+l}\\\
t^{\mathbf{p}}_{k-1},t^{\mathbf{q}}_{l}\
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}\mathbf{q}}_{k+l-1}\end{array}$

Thus, by Corollary 3.19 we can derive,

$t^{\mathbf{p}}_{k}p(t^{\mathbf{p}}_{k}\vee
t^{\mathbf{p}}_{k-1}),t^{\mathbf{q}}_{l}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}\mathbf{q}}_{k+l}p(t^{\mathbf{p}\mathbf{q}}_{k+l}\vee
t^{\mathbf{p}\mathbf{q}}_{k+l-1})$

whence the required sequent
$t^{p\mathbf{p}}_{k},t^{\mathbf{q}}_{l}\mbox{\Large$\,\rightarrow\,$}t^{p\mathbf{p}\mathbf{q}}_{k+l}$
follows by the extension axioms $\mathcal{T}$.

For Item 2, by the inductive hypothesis we have a polynomial-size proof of:

$\begin{array}[]{r@{ \ \seqar\ }l}t^{\mathbf{p}\mathbf{q}}_{k+l}\
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}}_{k+1},t^{\mathbf{q}}_{l}\\\
t^{\mathbf{p}\mathbf{q}}_{k+l-1}\
\mbox{\Large$\,\rightarrow\,$}&t^{\mathbf{p}}_{k},t^{\mathbf{q}}_{l}\end{array}$

Thus, by Corollary 3.19, we can derive,

$t^{\mathbf{p}\mathbf{q}}_{k+l}p(t^{\mathbf{p}\mathbf{q}}_{k+l}\vee
t^{\mathbf{p}\mathbf{q}}_{k+l-1})\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}}_{k+1}p(t^{\mathbf{p}}_{k+1}\vee
t^{\mathbf{p}}_{k}),t^{\mathbf{q}}_{l}$

whence the required sequent
$t^{p\mathbf{p}\mathbf{q}}_{k+l}\mbox{\Large$\,\rightarrow\,$}t^{p\mathbf{p}}_{k+1},t^{\mathbf{q}}_{l}$
follows by the extension axioms $\mathcal{T}$. ∎

###  5.2. From $\mathsf{L}\mathsf{PHP}_{n}$ to $(n+1)$-threshold

In this subsection we will give small proofs of the sequent Item 1 from
Section 5.1.

######  Lemma 5.5.

Let $\mathbf{q}=q_{0},\dots,q_{k-1}$. For all $j<k$, there are polynomial-size
$\mathsf{e}\mathsf{LNDT}^{+}$ proofs over extension axioms $\mathcal{T}$ of:

$q_{j}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{q}}_{1}$

###### Proof.

First we derive,

(6) $q_{j}\mbox{\Large$\,\leftrightarrow\,$}t^{q_{j}}_{1}$

as follows:

$\begin{array}[]{r@{\ \dseqar\ }ll}q_{j}\
\mbox{\Large$\,\leftrightarrow\,$}&0q_{j}(0\vee 1)&\text{by
\lx@cref{creftype~refnum}{Truth}, axioms and $\mathsf{cut}$ }\\\ \
\mbox{\Large$\,\leftrightarrow\,$}&t^{\varepsilon}_{1}q_{j}(t^{\varepsilon}_{1}\vee
t^{\varepsilon}_{0})&\text{by extension axioms $\mathcal{T}$ and
\lx@cref{creftype~refnum}{mon-replacing-result}}\\\ \
\mbox{\Large$\,\leftrightarrow\,$}&t^{q_{j}}_{1}&\text{by extension axioms
$\mathcal{T}$}\end{array}$

By repeatedly applying Lemma 5.4.Item 1 we obtain polynomial-size proofs of,

$t^{q_{0}}_{0},\dots,t^{q_{j-1}}_{0},t^{q_{j}}_{1},t^{q_{j+1}}_{0},\dots,t^{q_{k-1}}_{0}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{q}}_{1}$

However, we also have small proofs of
$\mbox{\Large$\,\rightarrow\,$}t^{q_{j}}_{0}$ by Proposition 4.5.Item 1, and
so applying $k-1$ cuts we obtain a polynomial-size proof of:

(7) $t^{q_{j}}_{1}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{q}}_{1}$

The required sequent now follows by simply cutting Eq. 6 against Eq. 7. ∎

######  Proposition 5.6.

There are polynomial-size $\mathsf{e}\mathsf{LNDT}^{+}$ proofs of Item 1,
i.e.,

$\mathsf{L}\mathsf{PHP}_{n}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}}_{n+1}$

over extension axioms $\mathcal{T}$.

###### Proof.

Let $i\in\\{1,\dots,n+1\\}$. By Lemma 5.5 above, we have small proofs of,

$p_{ij}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}_{i}}_{1}$

for each $j=1,\dots,n$. By applying $n-1$ $\vee\text{-}l$ steps we derive:

(8)
$\bigvee\mathbf{p}_{i}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}_{i}}_{1}$

Now, applying Lemma 5.4.Item 1 $n$ times (and using cuts), we obtain small
proofs of:

(9)
$t^{\mathbf{p}_{1}}_{1},\dots,t^{\mathbf{p}_{n+1}}_{1}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}}_{n+1}$

Finally, by instantiating Eq. 8 for each $i=1,\dots,n+1$ and applying $n+1$
$\mathsf{cut}$ steps against Eq. 9 we derive the required sequent:

$\bigvee\mathbf{p}_{1},\dots,\bigvee\mathbf{p}_{n+1}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}}_{n+1}\qed$

###  5.3. From $(n+1)$-threshold to $\mathsf{R}\mathsf{PHP}_{n}$

Before deriving the final sequent Item 3 for our proof of $\mathsf{PHP}_{n}$,
we will need some lemmas.

######  Lemma 5.7.

Let $\mathbf{q}=q_{0},\dots,q_{k-1}$. There are polynomial-size
$\mathsf{e}\mathsf{LNDT}^{+}$ proofs of,

$q,t^{\mathbf{q}}_{1}\mbox{\Large$\,\rightarrow\,$}\\{0q(0\vee
q_{i})\\}_{i<k}$

over extension axioms $\mathcal{T}$.

###### Proof.

For each $i<k$, by Proposition 3.17.Item 4 we have a (constant-size) proof of,

$q,q_{i}\mbox{\Large$\,\rightarrow\,$}0q(0\vee q_{i})$

and so by cutting against appropriate instances of Eq. 6 we obtain:

$q,t^{q_{i}}_{1}\mbox{\Large$\,\rightarrow\,$}0q(0\vee q_{i})$

Instantiating the above for each $i<k$ and applying several
$\mathsf{w}\text{-}r$ and $\vee\text{-}l$ steps we obtain:

(10)
$q,\bigvee\limits_{i<k}t^{q_{i}}_{1}\mbox{\Large$\,\rightarrow\,$}\\{0q(0\vee
q_{i})\\}_{i<k}$

Now, by repeatedly applying Lemma 5.4.Item 2 (under cuts) and $\vee\text{-}r$
steps we obtain polynomial-size proofs of:

(11)
$t^{\mathbf{q}}_{1}\mbox{\Large$\,\rightarrow\,$}\bigvee\limits_{i<k}t^{q_{i}}_{1}$

Finally, we conclude by cutting Eq. 11 above against Eq. 10. ∎

######  Lemma 5.8.

Let $\mathbf{p}=p_{0},\dots,p_{k-1}$. There are polynomial-size
$\mathsf{e}\mathsf{LNDT}^{+}$ proofs of,

$t^{\mathbf{p}}_{2}\mbox{\Large$\,\rightarrow\,$}\\{0q_{i}(0\vee
q_{i^{\prime}})\\}_{i<i^{\prime}<k}$

over extension axioms $\mathcal{T}$.

###### Proof.

We proceed by induction on the length $k$ of $\mathbf{q}$. In the base case,
when $\mathbf{q}=\varepsilon$, we have an axiom
$t^{\varepsilon}_{2}\mbox{\Large$\,\rightarrow\,$}0$ from $\mathcal{T}$,
whence we conclude by a cut against the $0$-axiom and $\mathsf{w}\text{-}r$.

For the inductive step, we obtain by two applications of Lemma 5.4.Item 2 the
following sequents:

$\begin{array}[]{r@{\ \seqar\ }l}t^{q\mathbf{q}}_{2}\
\mbox{\Large$\,\rightarrow\,$}&t^{q}_{1},t^{\mathbf{q}}_{2}\\\
t^{q\mathbf{q}}_{2}\
\mbox{\Large$\,\rightarrow\,$}&t^{q}_{2},t^{\mathbf{q}}_{1}\end{array}$

Now we already have small proofs of $t^{q}_{1}\mbox{\Large$\,\rightarrow\,$}q$
from Eq. 6 and of $t^{q}_{2}\mbox{\Large$\,\rightarrow\,$}$ from Proposition
4.5.Item 3, and so cutting against the respective sequents above we obtain:

(12) $\displaystyle t^{q\mathbf{q}}_{2}$ $\displaystyle\
\mbox{\Large$\,\rightarrow\,$}\ q,t^{\mathbf{q}}_{2}$ (13) $\displaystyle
t^{q\mathbf{q}}_{2}$ $\displaystyle\ \mbox{\Large$\,\rightarrow\,$}\
t^{\mathbf{q}}_{1}$

Finally, we combine these sequents using cuts as follows:

Eq. 12 $t^{q\mathbf{q}}_{2}\mbox{\Large$\,\rightarrow\,$}q,t^{\mathbf{q}}_{2}$
Eq. 13 $t^{q\mathbf{q}}_{2}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{q}}_{1}$
Lemma 5.7 $q,t^{\mathbf{q}}_{1}\mbox{\Large$\,\rightarrow\,$}\\{0q(0\vee
q_{i})\\}_{i<k}$ $\scriptstyle 2\mathsf{cut}\;$
$t^{q\mathbf{q}}_{2}\mbox{\Large$\,\rightarrow\,$}\\{0q(0\vee q_{i})\\}_{i<k}$
$\mathit{IH}$ $t^{\mathbf{q}}_{2}\mbox{\Large$\,\rightarrow\,$}\\{0q_{i}(0\vee
q_{i^{\prime}})\\}_{i<i^{\prime}<k}$ $\scriptstyle\mathsf{cut}\;$
$t^{q\mathbf{q}}_{2}\mbox{\Large$\,\rightarrow\,$}\\{0q_{i}(0\vee
q_{i^{\prime}})\\}_{i<i^{\prime}<k}$

where the proof marked $\mathit{IH}$ is obtained from the inductive
hypothesis. ∎

######  Proposition 5.9.

There are polynomial-size $\mathsf{e}\mathsf{LNDT}^{+}$ proofs over
$\mathcal{T}$ of Item 3, i.e. of:

$t^{\mathbf{p}^{\intercal}}_{n+1}\mbox{\Large$\,\rightarrow\,$}\mathsf{R}\mathsf{PHP}_{n}$

###### Proof.

Recall that
$\mathbf{p}^{\intercal}=\mathbf{p}^{\intercal}_{1},\dots,\mathbf{p}^{\intercal}_{n}$,
so by $n-1$ applications of Lemma 5.4.Item 2 (and cuts) we have small proofs
of:

(14)
$t^{\mathbf{p}^{\intercal}}_{n+1}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}^{\intercal}_{1}}_{2},\dots,t^{\mathbf{p}^{\intercal}_{n}}_{2}$

Now, instantiating Lemma 5.8 with $\mathbf{q}=\mathbf{p}^{\intercal}_{j}$ we
also have small proofs of,

(15)
$t^{\mathbf{p}^{\intercal}_{j}}_{2}\mbox{\Large$\,\rightarrow\,$}\\{0p_{ij}(0\vee
p_{i^{\prime}j})\\}_{1\leq i<i^{\prime}\leq n}$

for each $j=1,\dots,n$. Finally, we may apply $n$ $\mathsf{cut}$ steps on Eq.
14 against each instance of Eq. 15 (for $j=1,\dots,n$) and apply
$\vee\text{-}r$ steps to obtain the required sequent. ∎

###  5.4. Putting it all together

We are now ready to assemble our proofs for $\mathsf{PHP}_{n}$.

###### Proof of Theorem 5.2.

We simply cut together the proofs of Item 1, Item 2 and Item 3 that we have so
far constructed:

${{}{}{}\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\text{\lx@cref{creftype~refnum}{lphp-
implies-thrPijn+1}}$}}}}\kern 1.43518pt\kern-0.7pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}}\vbox{\vbox
to1.8pt{\vfill\hbox to171.66707pt{\hrulefill}\kern 1.0pt\hbox
to171.66707pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\kern-0.7pt\hbox{\kern 59.06682pt\hbox{\hbox{$\kern
0.0pt\hbox{$\mathsf{L}\mathsf{PHP}_{n}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}}_{n+1}$}\kern
0.0pt$}}\kern 59.06682pt}}}\kern 0.0pt}\kern 10.00002pt}\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\text{\lx@cref{creftype~refnum}{thr-
symmetric-permutations}}$}}}}\kern 1.43518pt\kern-0.7pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}}\vbox{\vbox
to1.8pt{\vfill\hbox to193.58374pt{\hrulefill}\kern 1.0pt\hbox
to193.58374pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\kern-0.7pt\hbox{\kern 81.1364pt\hbox{\hbox{$\kern
0.0pt\hbox{$t^{\mathbf{p}}_{n+1}\mbox{\Large$\,\rightarrow\,$}t^{\mathbf{p}^{\intercal}}_{n+1}$}\kern
0.0pt$}}\kern 81.1364pt}}}\kern 0.0pt}\kern 10.00002pt}\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\text{\lx@cref{creftype~refnum}{thrPjin+1-implies-
rphp}}$}}}}\kern 1.43518pt\kern-0.7pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}}\vbox{\vbox
to1.8pt{\vfill\hbox to172.52817pt{\hrulefill}\kern 1.0pt\hbox
to172.52817pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\kern-0.7pt\hbox{\kern 58.05293pt\hbox{\hbox{$\kern
0.0pt\hbox{$t^{\mathbf{p}^{\intercal}}_{n+1}\mbox{\Large$\,\rightarrow\,$}\mathsf{R}\mathsf{PHP}_{n}$}\kern
0.0pt$}}\kern 58.05293pt}}}\kern 0.0pt}}}}\kern 1.43518pt\hbox{\kern
59.06682pt\hbox to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
2\mathsf{cut}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to440.65924pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 58.05293pt}\kern 1.43518pt\hbox{\kern
240.07405pt\hbox{\hbox{$\mathsf{L}\mathsf{PHP}_{n}\mbox{\Large$\,\rightarrow\,$}\mathsf{R}\mathsf{PHP}_{n}$}}\kern
239.06017pt}}}\kern 0.0pt}}}\qed$

##  6\. Positive simulation of non-positive proofs

In the previous section we showcased the capacity of the system
$\mathsf{e}\mathsf{LNDT}^{+}$ to formalise basic counting arguments by giving
polynomial-size proofs of the pigeonhole principle. In this section we go
further and give a general polynomial simulation of $\mathsf{e}\mathsf{LNDT}$,
over positive sequents, by adapting a method from [3].

######  Theorem 6.1.

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

While the high-level structure of the argument is similar to that of [3], we
must make several specialisations to the current setting due to the
peculiarities of eNDT formulas and extension axioms.

###  6.1. Summary of proof structure

Before giving the low-level details, let us survey our approach towards
proving Theorem 6.1, in particular comparing it to the analogous methodology
from [3]. Our strategy is divided into three main parts, which mimic the
analogous proof structure from [3].

In the first part, Section 6.2, we deal with the non-positive formulas
occurring in an $\mathsf{e}\mathsf{LNDT}$ proof. The intuition is similar to
what is done in [3] where they first reduced all negations to the variables
using De Morgan duality. In our setting formulas are no longer closed under
duality but, nonetheless, we are able to devise for each formula $A$ an
appropriate ‘positive normal form’ $A^{-}$. $A^{-}$ may contain negative
literals (in particular as decision variables), but all decisions themselves
are positive. We duly consider an extension
${\mathsf{e}\mathsf{LNDT}^{+}_{-}}$ of $\mathsf{e}\mathsf{LNDT}^{+}$ which
admits negative literals $\overline{p}$ and has two extra axioms:
$p,\overline{p}\mbox{\Large$\,\rightarrow\,$}$ and
$\mbox{\Large$\,\rightarrow\,$}p,\overline{p}$. The main result of the first
part is that $\mathsf{e}\mathsf{LNDT}^{+}_{-}$ polynomially simulates
$\mathsf{e}\mathsf{LNDT}$ over positive sequents (Corollary 6.5), by
essentially replacing each formula occurrence $A$ by $A^{-}$ and locally
repairing the proof (Theorem 6.3).

In the second part the aim is to ‘replace’ negative literals in a
$\mathsf{e}\mathsf{LNDT}^{+}_{-}$ proof by certain threshold formulas from
Definition 4.3. The is the same idea as in [3], but in our setting we must
deal with certain technicalities encountered when substituting extended
formulas in $\mathsf{e}\mathsf{LNDT}^{+}_{-}$ and
$\mathsf{e}\mathsf{LNDT}^{+}$. In particular, if a literal occurs as a
decision variable, then we cannot directly substitute it for an extension
variable (e.g. a threshold formula $t^{\mathbf{p}}_{k}$), since the syntax of
$\mathsf{e}\mathsf{LNDT}$ (and its fragments) does not allow for this. To
handle this issue appropriately, we introduce in Section 6.3 a refinement of
our previous threshold extension variables and axioms, defined mutually
inductively with eNDT formulas themselves, that accounts for all such
substitution situations (Definition 6.6).

For the remainder of the argument, in Section 6.4 we fix a
$\mathsf{e}\mathsf{LNDT}^{+}_{-}$ proof $P$ of
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$ over extension axioms
$\mathcal{A}$ and propositional variables $\mathbf{p}=p_{0},\dots,p_{m-1}$. We
define, for $k\geq 0$, systems $\mathsf{e}\mathsf{LNDT}^{+}_{k}(P)$ that each
have polynomial-size proofs $P^{k}$ of
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$ (Lemma 6.12). Morally speaking,
this simulation is by ‘substituting’ thresholds for negative literals, and the
consequent new axioms required in $\mathsf{e}\mathsf{LNDT}^{+}_{k}(P)$ are
parametrised by the threshold $k$. We point out that
$\mathsf{e}\mathsf{LNDT}^{+}_{k}(P)$ itself is tailored to the specific set of
extension axioms $\mathcal{A}$ and propositional variables $\mathbf{p}$ to
facilitate the choice of threshold formulas and required extension
variables/axioms.

The final part, Section 6.5, essentially stitches together proofs obtained in
each ${\mathsf{e}\mathsf{LNDT}^{+}_{k}(P)}$ for $0\leq k\leq m+1$. More
precisely, using basic properties of threshold formulas, we show that each
$\mathsf{e}\mathsf{LNDT}^{+}_{k}(P)$ proof of a positive sequent
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$ can be polynomially transformed
into a $\mathsf{e}\mathsf{LNDT}^{+}$ proof of
$t^{\mathbf{p}}_{k},\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,t^{\mathbf{p}}_{k+1}$,
over appropriate extension axioms (Lemma 6.14). We conclude the argument for
our main result Theorem 6.1 by simply cutting these together and appealing to
Proposition 4.5.

###  6.2. Positive normal form of $\mathsf{e}\mathsf{LNDT}$ proofs

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. For this reason, let us introduce, for
each propositional variable $p$, a distinguished variable $\overline{p}$,
which we shall also refer to as ‘negative literals’.

The system $\mathsf{e}\mathsf{LNDT}^{+}_{-}$ is defined just like
$\mathsf{e}\mathsf{LNDT}^{+}$ but also allows negative literals $\overline{p}$
to appear in (positive) decision steps. All syntactic positivity constraints
remain. Furthermore, $\mathsf{e}\mathsf{LNDT}^{+}_{-}$ has two additional
initial sequents:

$\scriptstyle\neg\text{-}l\;$ $p,\overline{p}\mbox{\Large$\,\rightarrow\,$}$
$\scriptstyle\neg\text{-}r\;$ $\mbox{\Large$\,\rightarrow\,$}p,\overline{p}$

The system $\mathsf{e}\mathsf{LNDT}^{+}_{-}$ admits essentially a ‘normal
form’ of $\mathsf{e}\mathsf{LNDT}$ proofs:

######  Definition 6.2.

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

$\begin{array}[]{r@{\ :=\ }l}0^{-}&0\\\ 1^{-}&1\\\ p^{-}&p\\\
\overline{p}^{-}&\overline{p}\end{array}\qquad\begin{array}[]{r@{\ :=\
}l}e_{i}^{-}&e_{i}\\\ \vskip 3.0pt plus 1.0pt minus 1.0pt\cr(A\vee
B)^{-}&A^{-}\vee B^{-}\\\ \vskip 3.0pt plus 1.0pt minus
1.0pt\cr(ApB)^{-}&0\overline{p}(0\vee A^{-})\vee 0p(0\vee B^{-})\end{array}$

For a multiset of formulas $\Gamma=A_{1},\dots,A_{n}$ we write
$\Gamma^{-}:=A^{-}_{1},\dots,A^{-}_{n}$. For a set of extension axioms
$\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$, we
write $\mathcal{A}^{-}$ for
$\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A^{-}_{i}\\}_{i<n}$.

######  Theorem 6.3.

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

Notice that, since $\cdot^{-}$ commutes with all connectives except for
decisions, to prove the above result it suffices to just derive the
translation of decision steps. For this it will be useful to have another
‘truth’ lemma:

######  Lemma 6.4 (Truth for $\cdot^{-}$-translation).

Let $\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}\\}_{i<n}$ 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}^{-}$:

  1. (1)

$(ApB)^{-}\mbox{\Large$\,\rightarrow\,$}A^{-},p$

  2. (2)

$(ApB)^{-},p\mbox{\Large$\,\rightarrow\,$}B^{-}$

  3. (3)

$A^{-}\mbox{\Large$\,\rightarrow\,$}(ApB)^{-},p$

  4. (4)

$p,B^{-}\mbox{\Large$\,\rightarrow\,$}(ApB)^{-}$

###### Proof.

We give the proofs explicitly below:

$\scriptstyle 0\;$ $0\mbox{\Large$\,\rightarrow\,$}$ $\scriptstyle
2\mathsf{w}\text{-}r\;$ $0\mbox{\Large$\,\rightarrow\,$}A^{-},p$
$\scriptstyle\mathsf{id}\;$ $A^{-}\mbox{\Large$\,\rightarrow\,$}A^{-}$
$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$
$\overline{p},A^{-}\mbox{\Large$\,\rightarrow\,$}A^{-},p$
$\scriptstyle\overline{p}^{+}\text{-}l\;$ $0\overline{p}(0\vee
A^{-})\mbox{\Large$\,\rightarrow\,$}A^{-},p$ $\scriptstyle 0\;$
$0\mbox{\Large$\,\rightarrow\,$}$ $\scriptstyle 2\mathsf{w}\text{-}r\;$
$0\mbox{\Large$\,\rightarrow\,$}A^{-},p$ $\scriptstyle\mathsf{id}\;$
$p\mbox{\Large$\,\rightarrow\,$}p$
$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$
$p,B^{-}\mbox{\Large$\,\rightarrow\,$}A^{-},p$ $\scriptstyle p^{+}\text{-}l\;$
$0p(0\vee B^{-})\mbox{\Large$\,\rightarrow\,$}A^{-},p$
$\scriptstyle\vee\text{-}l\;$ $(ApB)^{-}\mbox{\Large$\,\rightarrow\,$}A^{-},p$
$\scriptstyle 0\;$ $0\mbox{\Large$\,\rightarrow\,$}$
$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$
$0,p\mbox{\Large$\,\rightarrow\,$}B^{-}$ $\scriptstyle\neg\text{-}l\;$
$\overline{p},p\mbox{\Large$\,\rightarrow\,$}$
$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$
$\overline{p},A^{-},p\mbox{\Large$\,\rightarrow\,$}B^{-}$
$\scriptstyle\overline{p}^{+}\text{-}l\;$ $0\overline{p}(0\vee
A^{-}),p\mbox{\Large$\,\rightarrow\,$}B^{-}$ $\scriptstyle 0\;$
$0\mbox{\Large$\,\rightarrow\,$}$
$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$
$0,p\mbox{\Large$\,\rightarrow\,$}B^{-}$ $\scriptstyle\mathsf{id}\;$
$B^{-}\mbox{\Large$\,\rightarrow\,$}B^{-}$ $\scriptstyle
2\mathsf{w}\text{-}l\;$ $p,B^{-},p\mbox{\Large$\,\rightarrow\,$}B^{-}$
$\scriptstyle p^{+}\text{-}l\;$ $0p(0\vee
B^{-}),p\mbox{\Large$\,\rightarrow\,$}B$ $\scriptstyle\vee\text{-}l\;$
$(ApB)^{-},p\mbox{\Large$\,\rightarrow\,$}B^{-}$ ${{{}{}\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
17.46533pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
14.79689pt\hbox{\vbox{\offinterlineskip\hbox{\kern
15.28218pt\hbox{\hbox{\hbox{$$}}}\kern 15.28218pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\neg\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to30.56438pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\mbox{\Large$\,\rightarrow\,$}\overline{p},p$}\kern
0.0pt$}}}}}\kern 0.0pt}}\kern 7.18335pt}\kern 1.43518pt\hbox{\kern
7.61354pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to44.93108pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern
7.61354pt\hbox{\hbox{$\kern
0.0pt\hbox{$A^{-}\mbox{\Large$\,\rightarrow\,$}0\overline{p},p$}\kern
0.0pt$}}}}}\kern 0.0pt}\kern 10.00002pt}\hbox{\kern
17.01915pt\hbox{\vbox{\offinterlineskip\hbox{\kern 0.84898pt\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
17.41103pt\hbox{\hbox{\hbox{$$}}}\kern 17.41103pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to34.82207pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$A^{-}\mbox{\Large$\,\rightarrow\,$}A^{-}$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 9.46004pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
2\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to53.74216pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$A^{-}\mbox{\Large$\,\rightarrow\,$}0,A^{-},p$}\kern
0.0pt$}}}}}\kern 0.0pt}}}}\kern 1.43518pt\hbox{\kern 25.07887pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\overline{p}^{+}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to125.6924pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern
48.83177pt\hbox{\hbox{$A^{-}\mbox{\Large$\,\rightarrow\,$}0\overline{p}(0\vee
A^{-}),p$}}\kern 23.7529pt}}}\kern 0.0pt}}}\kern 1.43518pt\hbox{\kern
48.83177pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}r,\vee\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to78.1866pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 23.7529pt}\kern
1.43518pt\hbox{\kern 55.32828pt\hbox{\hbox{$\kern
0.0pt\hbox{$A^{-}\mbox{\Large$\,\rightarrow\,$}(ApB)^{-},p$}\kern
0.0pt$}}\kern 30.2494pt}}}\kern 0.0pt}}}\vbox{\hbox{}}}\ \
{{}{}\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
25.07887pt\hbox{\vbox{\offinterlineskip\hbox{\kern 3.3101pt\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
13.07559pt\hbox{\hbox{\hbox{$$}}}\kern 13.07559pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to26.1512pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$p\mbox{\Large$\,\rightarrow\,$}p$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 11.92116pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to49.99352pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$p,B^{-}\mbox{\Large$\,\rightarrow\,$}0,p$}\kern 0.0pt$}}}}}\kern
0.0pt}\kern 10.00002pt}\hbox{\kern
25.07887pt\hbox{\vbox{\offinterlineskip\hbox{\kern 0.84898pt\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
17.99782pt\hbox{\hbox{\hbox{$$}}}\kern 17.99782pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to35.99565pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$B^{-}\mbox{\Large$\,\rightarrow\,$}B^{-}$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 9.46004pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to54.91574pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$p,B^{-}\mbox{\Large$\,\rightarrow\,$}0,B^{-}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}}\kern 1.43518pt\hbox{\kern 25.07887pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\overline{p}^{+}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to139.98814pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern
55.37723pt\hbox{\hbox{$p,B^{-}\mbox{\Large$\,\rightarrow\,$}0p(0\vee
B^{-})$}}\kern 30.29836pt}}}\kern 0.0pt}}}\kern 1.43518pt\hbox{\kern
55.37723pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}r,\vee\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to79.39142pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 30.29836pt}\kern
1.43518pt\hbox{\kern 62.18274pt\hbox{\hbox{$\kern
0.0pt\hbox{$p,B^{-}\mbox{\Large$\,\rightarrow\,$}(ApB)^{-}$}\kern
0.0pt$}}\kern 37.10387pt}}}\kern 0.0pt}}}\qed$

We can now prove our polynomial-size interpretation of
$\mathsf{e}\mathsf{LNDT}$ within $\mathsf{e}\mathsf{LNDT}^{+}_{-}$:

###### Proof of Theorem 6.3.

We proceed by a straightforward induction on the length of $P$. The critical
cases are when $P$ ends with decision steps, which we translate as follows. A
left decision step,

$\Gamma,A\mbox{\Large$\,\rightarrow\,$}\Delta,p$$\Gamma,p,B\mbox{\Large$\,\rightarrow\,$}\Delta$
$\scriptstyle p\text{-}l\;$ $\Gamma,ApB\mbox{\Large$\,\rightarrow\,$}\Delta$

is simulated by the following derivation:

Lemma 6.4.Item 1 $(ApB)^{-}\mbox{\Large$\,\rightarrow\,$}A^{-},p$
$\Gamma,A^{-}\mbox{\Large$\,\rightarrow\,$}\Delta,p$
$\scriptstyle\mathsf{cut}\;$
$\Gamma,(ApB)^{-}\mbox{\Large$\,\rightarrow\,$}\Delta,p$ Lemma 6.4.Item 2
$(ApB)^{-},p\mbox{\Large$\,\rightarrow\,$}B^{-}$
$\Gamma,p,B^{-}\mbox{\Large$\,\rightarrow\,$}\Delta$
$\scriptstyle\mathsf{cut}\;$
$\Gamma,(ApB)^{-},p\mbox{\Large$\,\rightarrow\,$}\Delta$
$\scriptstyle\mathsf{cut}\;$
$\Gamma,(ApB)^{-}\mbox{\Large$\,\rightarrow\,$}\Delta$

A right decision step,

$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A,p$$\Gamma,p\mbox{\Large$\,\rightarrow\,$}\Delta,B$
$\scriptstyle p\text{-}r\;$ $\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,ApB$

is simulated by the following derivation:

${{{}{}}{{}{}}\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
12.49995pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,A^{-},p$}}\kern
10.00002pt}\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\text{\lx@cref{creftype~refnum}{Truth-
negtrans}.\lx@cref{creftype~refnum}{item:truth-negtrans-0case-implies-
dec}}$}}}}\kern 1.43518pt\kern-0.7pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}}\vbox{\vbox
to1.8pt{\vfill\hbox to373.50072pt{\hrulefill}\kern 1.0pt\hbox
to373.50072pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\kern-0.7pt\hbox{\kern 154.15356pt\hbox{\hbox{$\kern
0.0pt\hbox{$A^{-}\mbox{\Large$\,\rightarrow\,$}(ApB)^{-},p$}\kern
0.0pt$}}\kern 154.15356pt}}}\kern 0.0pt}}}}\kern 1.43518pt\hbox{\kern
0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{cut}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to283.306pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 154.15356pt}\kern 1.43518pt\hbox{\kern
104.22565pt\hbox{\hbox{$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,(ApB)^{-},p$}}\kern
258.37921pt}}}\kern 0.0pt}\kern 10.00002pt}\hbox{\kern
12.49995pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\Gamma,p\mbox{\Large$\,\rightarrow\,$}\Delta,B^{-}$}}\kern
10.00002pt}\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{$\text{\lx@cref{creftype~refnum}{Truth-
negtrans}.\lx@cref{creftype~refnum}{item:truth-negtrans-1case-implies-
dec}}$}}}}\kern 1.43518pt\kern-0.7pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}}\vbox{\vbox
to1.8pt{\vfill\hbox to373.50072pt{\hrulefill}\kern 1.0pt\hbox
to373.50072pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower-0.7pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\kern-0.7pt\hbox{\kern 153.86017pt\hbox{\hbox{$\kern
0.0pt\hbox{$p,B^{-}\mbox{\Large$\,\rightarrow\,$}(ApB)^{-}$}\kern
0.0pt$}}\kern 153.86017pt}}}\kern 0.0pt}}}}\kern 1.43518pt\hbox{\kern
0.0pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{cut}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to284.18619pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 153.86017pt}\kern 1.43518pt\hbox{\kern
104.87929pt\hbox{\hbox{$\Gamma,x\mbox{\Large$\,\rightarrow\,$}\Delta,(ApB)^{-}$}}\kern
258.73946pt}}}\kern 0.0pt}}}}\kern 1.43518pt\hbox{\kern 116.7256pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{cut}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to535.04076pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 258.73946pt}\kern 1.43518pt\hbox{\kern
351.55646pt\hbox{\hbox{$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta,(ApB)^{-}$}}\kern
493.57031pt}}}\kern 0.0pt}}}\qed$

Finally we note that the translation above gives rise to a bona fide
polynomial simulation of $\mathsf{e}\mathsf{LNDT}$ by
$\mathsf{e}\mathsf{LNDT}^{+}_{-}$ over positive sequents:

######  Corollary 6.5.

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

###### Proof.

From Theorem 6.3 above, it suffices to derive
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$ from
$\Gamma^{-}\mbox{\Large$\,\rightarrow\,$}\Delta^{-}$. For this we shall give
short proofs of,

(16) $A\ \mbox{\Large$\,\leftrightarrow\,$}\ A^{-}$

when $A$ is positive and free of extension variables, whence
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$ follows from
$\Gamma^{-}\mbox{\Large$\,\rightarrow\,$}\Delta^{-}$ by several cuts. We
proceed by structural induction on $A$, for which the critical case is when
$A$ is a decision formula. We prove the two directions separately.

First, note that we have polynomial-size proofs of the following sequents:

(17) $\displaystyle Ap(A\vee B)$ $\displaystyle\
\mbox{\Large$\,\rightarrow\,$}\ A,p$ by Proposition 3.17.Item 1 (18)
$\displaystyle Ap(A\vee B)$ $\displaystyle\ \mbox{\Large$\,\rightarrow\,$}\
A\vee B$ by Proposition 3.17.Item 2 and $\vee\text{-}r$ (19) $\displaystyle A$
$\displaystyle\ \mbox{\Large$\,\rightarrow\,$}\ (Ap(A\vee B))^{-},p$ by Lemma
6.4.Item 3 and $\mathit{IH}$ (20) $\displaystyle p,A\vee B$ $\displaystyle\
\mbox{\Large$\,\rightarrow\,$}\ (Ap(A\vee B))^{-}$ by Lemma 6.4.Item 4 and
$\mathit{IH}$

We arrange these into a proof of the left-right direction as follows:

Eq. 17 Eq. 19 $\scriptstyle A\text{-}\mathsf{cut}\;$ $Ap(A\vee
B)\mbox{\Large$\,\rightarrow\,$}(Ap(A\vee B))^{-},p$ Eq. 18 Eq. 20
$\scriptstyle A\vee B\text{-}\mathsf{cut}\;$ $Ap(A\vee
B),p\mbox{\Large$\,\rightarrow\,$}(Ap(A\vee B))^{-}$ $\scriptstyle
p\text{-}\mathsf{cut}\;$ $Ap(A\vee B)\mbox{\Large$\,\rightarrow\,$}(Ap(A\vee
B))^{-}$

Next, note that we have small proofs of the following sequents:

(21) $\displaystyle A$ $\displaystyle\ \mbox{\Large$\,\rightarrow\,$}\
Ap(A\vee B)$ by Proposition 3.17.Item 3 (22) $\displaystyle p,B$
$\displaystyle\ \mbox{\Large$\,\rightarrow\,$}\ Ap(A\vee B)$ by Proposition
3.17.Item 4 (23) $\displaystyle(Ap(A\vee B))^{-}$ $\displaystyle\
\mbox{\Large$\,\rightarrow\,$}\ {A},p$ by Lemma 6.4.Item 1 and $\mathit{IH}$
(24) $\displaystyle(Ap(A\vee B))^{-}$ $\displaystyle\
\mbox{\Large$\,\rightarrow\,$}\ {A\lor B}$ by Lemma 6.4.Item 2 and
$\mathit{IH}$

We arrange these into a proof of the left-right direction as follows:

${{{}{}}{{}{}}\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\kern
20.08328pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\text{\lx@cref{creftype~refnum}{eq:negtransposdec-
implies-negtransAorx}}\quad$}}\kern
10.00002pt}\hbox{\hbox{$\quad\text{\lx@cref{creftype~refnum}{eq:A-implies-
posdec}}$}}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
A\text{-}\mathsf{cut}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to433.02861pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
155.79187pt\hbox{\hbox{$Ap(A\vee B)^{-}\mbox{\Large$\,\rightarrow\,$}Ap(A\vee
B),p$}}\kern 155.79187pt}}}\kern 0.0pt}\kern 10.00002pt}\hbox{\kern
34.85504pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{$\text{\lx@cref{creftype~refnum}{eq:negtransposdecandx-
implies-negtransB}}\quad$}}\kern
10.00002pt}\hbox{\hbox{$\quad\text{\lx@cref{creftype~refnum}{eq:A-implies-
posdec}}$}}}}}\kern 1.43518pt\hbox{\kern 0.0pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle A\lor
B\text{-}\mathsf{cut}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to439.80643pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern 1.43518pt\hbox{\kern
159.18079pt\hbox{\hbox{$Ap(A\vee
B)^{-},p\mbox{\Large$\,\rightarrow\,$}Ap(A\vee B)$}}\kern 159.18079pt}}}\kern
0.0pt}}}}\kern 1.43518pt\hbox{\kern 175.87515pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle
p\text{-}\mathsf{cut}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to602.71742pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}\kern 159.18079pt}\kern 1.43518pt\hbox{\kern
421.24927pt\hbox{\hbox{$Ap(A\vee B)^{-}\mbox{\Large$\,\rightarrow\,$}Ap(A\vee
B)$}}\kern 404.5549pt}}}\kern 0.0pt}}}\qed$

###  6.3. Generalised counting formulas

The argument of [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, whereas in our setting we deal with
extension variables that represent NBPs via extension axioms, and so handling
substitutions is much more subtle and notationally heavy.

We avoid giving a uniform treatment of this, instead specialising to counting
formulas, but we must nonetheless carefully give an appropriate mutually
recursive formulation of formulas and extension variables.

######  Definition 6.6 (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,
with $\mathbf{p},k,A,B$ ranging as just described:

(25) $\begin{array}[]{r@{\ \extiff\ }ll}[{\scriptstyle
A}{t^{\varepsilon}_{0}}{\scriptstyle(A\vee B)}]\
\mbox{\Large$\,\leftrightarrow\,$}&A\vee B&\\\ [{\scriptstyle
A}{t^{\varepsilon}_{k}}{\scriptstyle(A\vee B)}]\
\mbox{\Large$\,\leftrightarrow\,$}&A&k\neq 0\\\ [{\scriptstyle
A}{t^{p\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]\
\mbox{\Large$\,\leftrightarrow\,$}&[{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]p([{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]\vee[{\scriptstyle
A}{t^{\mathbf{p}}_{k-1}}{\scriptstyle(A\vee B)}])\end{array}$

Note that, despite the presentation, $[{\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, we do not permit. This is why we use the
square brackets to distinguish it from other formulas, though we shall justify
this notation shortly.

One should view the extension variables above and the notion of an
$\mathsf{e}\mathsf{LNDT}^{+}$ formula as being _mutually_ defined, so as to
avoid foundational issues. For instance, we allow an extension variable
$[{\scriptstyle C}{t^{\mathbf{p}}_{k}}{\scriptstyle(C\vee D)}]$, where $C$ or
$D$ may themselves contain extension variables of the form $[{\scriptstyle
A}{t^{\mathbf{q}}_{k}}{\scriptstyle(A\vee B)}]$. By building up formulas and
extension variables by mutual induction we ensure that such constructions are
well-founded. Let us briefly make this formal in the following remark:

######  Remark 6.7 (Well-foundedness of $\mathcal{T}$).

We may define the extension variables $[{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]$ and
$\mathsf{e}\mathsf{LNDT}^{+}$ formulas ‘in stages’ as follows:

  * •

Write $\Phi_{0}$ for the set of all $\mathsf{e}\mathsf{LNDT}^{+}$ formulas
over some base set of extension variables $E_{0}=\\{e_{00},e_{01},\dots\\}$.

  * •

Write $T_{n}$ for the set of all extension variables $t^{\mathbf{p}}_{k}$ and
of the form $[{\scriptstyle A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]$
with $A,B\in\Phi_{n}$.

  * •

Write $\Phi_{n+1}$ for the set of all formulas built from propositional
variables, disjunctions, positive decisions and extension variables from
$T_{n}$, $E_{n}$ and a fresh set of new extension variables
$E_{n+1}=\\{e_{(n+1)0},e_{(n+1)1},\dots\\}$.

Within each $T_{n}$ we (partially well-)order extension variables by the
length of the superscript $\mathbf{p}$, and within each $E_{n}$ we
(well-)order the $e_{ni}$s by the subscript $i$. Finally, we set
$E_{n}<T_{n}<E_{n+1}$ (i.e. if $e\in E_{n}$, $t\in T_{n}$ and $e^{\prime}\in
E_{n+1}$ then $e<t<e^{\prime}$). In this way the extension axioms from Eq. 25
(and Eq. 5) indeed satisfy the required well-foundedness criterion. We may
also admit further extension axioms allowing elements of $E_{n}$ to abbreviate
formulas in $\Phi_{n}$ (satisfying the indexing condition internal to
$E_{n}$), preserving well-foundedness. We shall indeed do this later.

Note, however, that the required order type on indices of these extension
variables, a priori, exceeds the ordinal $\omega$. This causes no issue for us
since, in any finite proof, we will only use finitely many extension
variables, and so may construe each index as a (relatively small) natural
number while preserving the aforementioned order. We shall gloss over this
issue in what follows.

As previously mentioned, our notation $[{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]$ is designed to be suggestive,
justified by the following counterpart of the truth conditions from
Proposition 3.17:

######  Proposition 6.8 (Truth conditions for threshold decisions).

There are polynomial size $\mathsf{e}\mathsf{LNDT}^{+}$ proofs over
$\mathcal{T}$ of:

  1. (1)

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

  2. (2)

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

  3. (3)

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

  4. (4)

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

###### Proof.

We proceed by induction on the length of $\mathbf{p}$. For the base case when
$\mathbf{p}=\varepsilon$, we have the following proofs:

$\begin{array}[]{c@{\qquad}c}{\vbox{\hbox{\kern
25.07887pt\hbox{\vbox{\offinterlineskip\hbox{\kern 5.49722pt\hbox{\hbox{\kern
13.83348pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
6.27771pt\hbox{\vbox{\offinterlineskip\hbox{\kern
10.54436pt\hbox{\hbox{\hbox{$$}}}\kern 10.54436pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower 0.0pt\hbox{$\scriptstyle 1\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to21.08871pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$\mbox{\Large$\,\rightarrow\,$}1$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 0.61124pt}\kern 1.43518pt\hbox{\kern 5.66647pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathcal{T},\mathsf{cut}\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to22.31119pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern
5.66647pt\hbox{\hbox{$\kern
0.0pt\hbox{$\mbox{\Large$\,\rightarrow\,$}t^{\varepsilon}_{0}$}\kern
0.0pt$}}}}}\kern 0.0pt}}\kern 24.99718pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to72.30556pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern 0.0pt\hbox{$[{\scriptstyle
A}{t^{\varepsilon}_{0}}{\scriptstyle(A\vee
B)}]\mbox{\Large$\,\rightarrow\,$}A,t^{\varepsilon}_{0}$}\kern
0.0pt$}}}}}\kern 0.0pt}}}&{\vbox{\hbox{\kern
19.05559pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
7.83327pt\hbox{\vbox{\offinterlineskip\hbox{\kern
40.41824pt\hbox{\hbox{\hbox{$$}}}\kern 40.41824pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathcal{T}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to80.83649pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$[{\scriptstyle A}{t^{\varepsilon}_{0}}{\scriptstyle(A\vee
B)}]\mbox{\Large$\,\rightarrow\,$}A\vee B$}\kern 0.0pt$}}}}}\kern
0.0pt}}}\kern 1.43518pt\hbox{\kern 7.83327pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id},\vee,\mathsf{cut}\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to80.83649pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}\kern 0.0pt}\kern
1.43518pt\hbox{\kern 11.16656pt\hbox{\hbox{$\kern 0.0pt\hbox{$[{\scriptstyle
A}{t^{\varepsilon}_{0}}{\scriptstyle(A\vee
B)}]\mbox{\Large$\,\rightarrow\,$}A,B$}\kern 0.0pt$}}\kern 3.3333pt}}}\kern
0.0pt}}}\\\ {\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
25.26059pt\hbox{\vbox{\offinterlineskip\hbox{\kern 0.98785pt\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
15.54436pt\hbox{\hbox{\hbox{$$}}}\kern 15.54436pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to31.08873pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}A$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 9.5989pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}r,\vee\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to50.28656pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}A\vee B$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 5.67604pt}\kern 1.43518pt\hbox{\kern 19.58455pt\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathcal{T},\mathsf{cut}\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to61.63866pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern
19.58455pt\hbox{\hbox{$\kern
0.0pt\hbox{$A\mbox{\Large$\,\rightarrow\,$}[{\scriptstyle
A}{t^{\varepsilon}_{0}}{\scriptstyle(A\vee B)}]$}\kern 0.0pt$}}}}}\kern
0.0pt}}}&{\vbox{\hbox{\kern
0.0pt\hbox{\vbox{\offinterlineskip\hbox{\hbox{\hbox{\kern
36.82031pt\hbox{\vbox{\offinterlineskip\hbox{\kern 6.02791pt\hbox{\hbox{\kern
8.61105pt\hbox{\vbox{\offinterlineskip\hbox{\kern
16.13115pt\hbox{\hbox{\hbox{$$}}}\kern 16.13115pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{id}\;$}}$}}\vbox{\vbox to0.4pt{\vfill\hbox
to32.26231pt{\hrulefill}\vfill}}\hbox to0.0pt{\hbox{$\smash{\lower
0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$B\mbox{\Large$\,\rightarrow\,$}B$}\kern 0.0pt$}}}}}\kern
0.0pt}}\kern 14.63896pt}\kern 1.43518pt\hbox{\hbox
to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathsf{w}\text{-}l,\mathsf{w}\text{-}r,\vee\text{-}r\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to61.54025pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern
1.43518pt\hbox{\hbox{\hbox{$\kern
0.0pt\hbox{$t^{\varepsilon}_{0},B\mbox{\Large$\,\rightarrow\,$}A\vee B$}\kern
0.0pt$}}}}}\kern 0.0pt}}\kern 5.67604pt}\kern 1.43518pt\hbox{\kern
31.14427pt\hbox to0.0pt{\hss\hbox{$\smash{\lower
0.0pt\hbox{$\scriptstyle\mathcal{T},\mathsf{cut}\;$}}$}}\vbox{\vbox
to0.4pt{\vfill\hbox to72.89235pt{\hrulefill}\vfill}}\hbox
to0.0pt{\hbox{$\smash{\lower 0.0pt\hbox{$$}}$}\hss}}\kern 1.43518pt\hbox{\kern
31.14427pt\hbox{\hbox{$\kern
0.0pt\hbox{$t^{\varepsilon}_{0},B\mbox{\Large$\,\rightarrow\,$}[{\scriptstyle
A}{t^{\varepsilon}_{0}}{\scriptstyle(A\vee B)}]$}\kern 0.0pt$}}}}}\kern
0.0pt}}}\end{array}$

For the inductive step for Item 1 we derive the following sequents:

$\begin{array}[]{r@{\ \seqar\ }ll}[{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]\
\mbox{\Large$\,\rightarrow\,$}&A,t^{\mathbf{p}}_{k}&\text{by $\mathit{IH}$}\\\
[{\scriptstyle A}{t^{\mathbf{p}}_{k-1}}{\scriptstyle(A\vee B)}]\
\mbox{\Large$\,\rightarrow\,$}&A,t^{\mathbf{p}}_{k-1}&\text{by
$\mathit{IH}$}\\\ [{\scriptstyle A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee
B)}]p([{\scriptstyle A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee
B)}]\vee[{\scriptstyle A}{t^{\mathbf{p}}_{k-1}}{\scriptstyle(A\vee B)}])\
\mbox{\Large$\,\rightarrow\,$}&A,t^{\mathbf{p}}_{k}p(t^{\mathbf{p}}_{k}\vee
t^{\mathbf{p}}_{k-1})&\text{by \lx@cref{creftype~refnum}{refined-replacement}
}\\\ [{\scriptstyle A}{t^{p\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]\
\mbox{\Large$\,\rightarrow\,$}&A,t^{p\mathbf{p}}_{k}&\text{by $\mathcal{T}$
and $2\mathsf{cut}$}\end{array}$

For the inductive step for Item 2 we derive the following sequents:

$\begin{array}[]{r@{\ \seqar\ }ll}[{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]\
\mbox{\Large$\,\rightarrow\,$}&A,B&\text{by $\mathit{IH}$}\\\ p,[{\scriptstyle
A}{t^{\mathbf{p}}_{k-1}}{\scriptstyle(A\vee B)}]\
\mbox{\Large$\,\rightarrow\,$}&A,B&\text{by $\mathit{IH}$ and
$\mathsf{w}\text{-}l$}\\\ [{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]p([{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]\vee[{\scriptstyle
A}{t^{\mathbf{p}}_{k-1}}{\scriptstyle(A\vee B)}])\
\mbox{\Large$\,\rightarrow\,$}&A,B&\text{by $p^{+}\text{-}l$}\\\
[{\scriptstyle A}{t^{p\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]\
\mbox{\Large$\,\rightarrow\,$}&A,B&\text{by $\mathcal{T}$ and
$\mathsf{cut}$}\end{array}$

For the inductive step for Item 3 we derive the following sequents:

$\begin{array}[]{r@{\ \seqar\ }ll}A\
\mbox{\Large$\,\rightarrow\,$}&[{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}],p&\text{by $\mathit{IH}$ and
$\mathsf{w}\text{-}r$}\\\ A\ \mbox{\Large$\,\rightarrow\,$}&[{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}],[{\scriptstyle
A}{t^{\mathbf{p}}_{k-1}}{\scriptstyle(A\vee B)}]&\text{by $\mathit{IH}$ and
$\mathsf{w}\text{-}r$}\\\ A\ \mbox{\Large$\,\rightarrow\,$}&[{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]p([{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]\vee[{\scriptstyle
A}{t^{\mathbf{p}}_{k-1}}{\scriptstyle(A\vee B)}])&\text{by $p^{+}\text{-}r$
}\\\ A\ \mbox{\Large$\,\rightarrow\,$}&[{\scriptstyle
A}{t^{p\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]&\text{by $\mathcal{T}$ and
$\mathsf{cut}$}\end{array}$

For the inductive step for Item 4 we derive the following sequents:

$\begin{array}[]{r@{\ \seqar\ }ll}t^{\mathbf{p}}_{k},B\
\mbox{\Large$\,\rightarrow\,$}&[{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]&\text{by $\mathit{IH}$}\\\
t^{\mathbf{p}}_{k-1},B\ \mbox{\Large$\,\rightarrow\,$}&[{\scriptstyle
A}{t^{\mathbf{p}}_{k-1}}{\scriptstyle(A\vee B)}]&\text{by $\mathit{IH}$}\\\
t^{\mathbf{p}}_{k}p(t^{\mathbf{p}}_{k}\vee t^{\mathbf{p}}_{k-1}),B\
\mbox{\Large$\,\rightarrow\,$}&[{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]p([{\scriptstyle
A}{t^{\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]\vee[{\scriptstyle
A}{t^{\mathbf{p}}_{k-1}}{\scriptstyle(A\vee B)}])&\text{by
\lx@cref{creftype~refnum}{refined-replacement}}\\\ t^{p\mathbf{p}}_{k},B\
\mbox{\Large$\,\rightarrow\,$}&[{\scriptstyle
A}{t^{p\mathbf{p}}_{k}}{\scriptstyle(A\vee B)}]&\text{by $\mathcal{T}$ and
$2\mathsf{cut}$}\qed\end{array}$

###  6.4. ‘Substituting’ thresholds for negative literals

For the remainder of this section, let us work with a fixed
$\mathsf{e}\mathsf{LNDT}^{+}_{-}$ proof $P$, over extension axioms
$\mathcal{A}=\\{e_{i}\mbox{\Large$\,\leftrightarrow\,$}A_{i}(e_{0},\dots,e_{i-1})\\}_{i<n}$,
of a positive sequent $\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$ containing
propositional variables among $\mathbf{p}=p_{0},\dots,p_{m-1}$ and extension
variables among $\mathbf{e}=e_{0},\dots,e_{n-1}$.

Recall that, since we are eventually trying to give a polynomial simulation of
$\mathsf{e}\mathsf{LNDT}$ by $\mathsf{e}\mathsf{LNDT}^{+}$ over positive
sequents, our consideration of $\mathsf{e}\mathsf{LNDT}^{+}_{-}$ here
suffices, by Corollary 6.5. We shall also work with the extension axioms
$\mathcal{T}$ from the previous subsection, and will soon explain its
interaction with $\mathcal{A}$ from $P$.

Throughout this section, we shall write $\mathbf{p}_{i}$ for
$p_{0},\dots,p_{i-1},p_{i+1},\dots,p_{m-1}$, i.e. $\mathbf{p}$ with the
variable $p_{i}$ removed. We shall define yet another intermediary system
$\mathsf{e}\mathsf{LNDT}^{+}_{k}(P)$, or rather a family of such systems, one
for each $k\geq 0$. Before that, we need to introduce the following
translation of formulas.

######  Definition 6.9 (‘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 a $\mathsf{e}\mathsf{LNDT}^{+}$
formula $A^{k}$ (over $\mathbf{p}$, some extension variables $\mathbf{e}^{k}$
and extension variables from $\mathcal{T}$) as follows:

  * •

$0^{k}:=0$

  * •

$1^{k}:=1$

  * •

$p_{i}^{k}:={p_{i}}$

  * •

$\overline{p}_{i}^{k}:=t^{\mathbf{p}_{i}}_{k}$

  * •

$e_{i}^{k}$ is a fresh extension variable.

  * •

$(A\vee B)^{k}:=A^{k}\vee B^{k}$

  * •

$(Ap_{i}(A\vee B))^{k}:=A^{k}p_{i}(A^{k}\vee B^{k})$

  * •

$(A\overline{p}_{i}(A\vee B))^{k}:=[{\scriptstyle
A^{k}}{t^{\mathbf{p}[0/{p_{i}}]}_{k}}{\scriptstyle(A^{k}\vee B^{k})}]$

We also define
$\mathcal{A}^{k}:=\\{e_{i}^{k}\mbox{\Large$\,\leftrightarrow\,$}A_{i}^{k}(e_{0}^{k},\dots,e_{i-1}^{k})\\}_{i<n}$,
and if $\Gamma=B_{1},\dots,B_{l}$ we write $\Gamma^{k}$ for
$B_{1}^{k},\dots,B_{l}^{k}$.

In what follows, we shall work with the set of extension axioms
$\mathcal{T}\cup\mathcal{A}^{k}$, so let us take a moment to justify that this
set of extension axioms is indeed well-founded.

######  Remark 6.10 (Well-foundedness, again).

Following on from Remark 6.7, well-foundedness of
$\mathcal{T}\cup\mathcal{A}^{k}$ follows from a suitable indexing of the
extension variables therein. To this end we assign ‘stages’ to each formula
$A^{k}$ by $\mathcal{A}$-induction on $A$, using the notation of Remark 6.7:

  * •

$p_{i}^{k},0^{k},1^{k}\in\Phi_{0}$.

  * •

$\overline{p}_{i}^{k}\in T_{0}$.

  * •

$e_{i}^{k}\in E_{m}\subseteq\Phi_{m}$ if
$A_{i}^{k}(e_{0}^{k},\dots,e_{i-1}^{k})\in\Phi_{m}$, with index $i$ (i.e.,
$e_{i}^{k}$ is $e_{mi}$).

  * •

$(A\vee B)^{k}\in\Phi_{m}$ if $A^{k},B^{k}\in\Phi_{m}$.

  * •

$(Ap_{i}(A\vee B))^{k}\in\Phi_{m}$ if $A^{k},B^{k}\in\Phi_{m}$.

  * •

$(A\overline{p}_{i}(A\vee B))^{k}\in T_{m}\subseteq\Phi_{m+1}$ if
$A^{k},B^{k}\in\Phi_{m}$.

Note in particular that stages can grow even for formulas free of $e_{i}^{k}$
since we may have nested decisions on negated variables $\overline{p}_{i}$.

Once again, in terms of proof complexity, we will gloss over this subtlety and
simply count the number of propositional and extension variable occurrences in
a proof, assuming that each variable can be equipped with a ‘small’ index.

We are now ready to define our intermediary systems.

######  Definition 6.11.

The system $\mathsf{e}\mathsf{LNDT}^{+}_{k}(P)$ is defined just like
$\mathsf{e}\mathsf{LNDT}^{+}$, but includes additional initial sequents,

(26) $\scriptstyle t\text{-}l\;$
$p_{i},t^{\mathbf{p}_{i}}_{k}\mbox{\Large$\,\rightarrow\,$}$ $\scriptstyle
t\text{-}r\;$ $\mbox{\Large$\,\rightarrow\,$}p_{i},t^{\mathbf{p}_{i}}_{k}$

and may only use the extension axioms $\mathcal{T}\cup\mathcal{A}^{k}$.

######  Lemma 6.12.

There is an $\mathsf{e}\mathsf{LNDT}^{+}_{k}(P)$ proof of
$\Gamma\mbox{\Large$\,\rightarrow\,$}\Delta$ of size polynomial in $|P|$.

###### Proof.

We construct the required proof $P^{k}$ by replacing every formula occurrence
$A$ in $P$ by $A^{k}$. Note that all structural steps, identities, cuts remain
correct. An extension axiom for $e_{i}$ from $\mathcal{A}$ is just translated
to the corresponding extension axiom for $e_{i}^{k}$ from $\mathcal{A}^{k}$,
and the initial sequents $\neg\text{-}l$ and $\neg\text{-}r$ from