1639 \lmcsheadingLABEL:LastPageApr. 07, 2020Aug. 12, 2020

For a coNP property $\psi(x)$, given $n\geq 1$, we can construct a size $n^{O(1)}$ propositional formula ${|\mkern-2.5mu|}\psi{|\mkern-2.5mu|}^{n}(x,y)$ with $n$ atoms $x=(x_{1},\dots,x_{n})$ and $n^{O(1)}$ atoms $y$ such that for any $a\in{\{0,1\}^{n}}$, $\psi(a)$ is true iff ${|\mkern-2.5mu|}\psi{|\mkern-2.5mu|}^{n}(a,y)\in\mbox{TAUT}$. This is just a restatement of the NP-completeness of SAT. In addition, if $\psi(x)$ is defined in a suitable language of arithmetic and has a suitable logical form, the translation can be defined purely syntactically without a reference to machines or computations. This then allows to transform also a possible first-order proof of $\forall x\psi(x)$ into a sequence of short propositional proofs of tautologies ${|\mkern-2.5mu|}\psi{|\mkern-2.5mu|}^{n}$, $n=1,2,\dots$; if the original proof uses axioms of theory $T$ (essentially any sound r.e. theory) then the propositional proofs will be in a proof system $P_{T}$ associated to $T$. Many standard proof systems are of the form $P_{T}$ for some $T$, and this is often the most efficient way how to construct short $P_{T}$-proofs of uniform sequences of tautologies. Although the unprovability of $\forall x\psi(x)$ in $T$ does not imply lower bounds for $P_{T}$-proofs of the tautologies, a method used in establishing the unprovability sometimes yields an insight how the lower bound could be proved. All this is a well-established part of proof complexity and the reader can find it in [4, Chpt.12] (or in references given there).

The translation is, however, not entirely faithful for formulas of a certain logical form, and this is an obstacle for transforming the conditional unprovability result for strong universal theories in [3] into conditional lower bounds for strong proof systems. To explain the problem in some detail assume $\psi(x)$ has the form

where $\varphi$ is a p-time property and $|x|$ is the bit length of $x$. The provability of $\forall x\psi(x)$ in a universal $T$ can be analyzed using the KPT theorem which provides an efficient interactive algorithm for finding $i$ given $x$ (cf. [6] or [4, Sec.12.2]). The same method does not, however, work in the propositional setting. To illustrate this assume that ${|\mkern-2.5mu|}\psi{|\mkern-2.5mu|}^{n}$ has a proof in proof system $P_{T}$ attached to $T$ and from that we can deduce in $T$ that

is a tautology (in addition the translation assures that all $y_{i}$ are disjoint tuples of atoms). This implies in $T$ that for all assignments $a$ and $b=(b_{0},\dots,b_{n-1})$ for all $x$ and all $y$ variables there is $i<n$ such that ${|\mkern-2.5mu|}\psi{|\mkern-2.5mu|}^{n}(a,b)$ is true. But to get (1) (and then use the KPT analysis from [3]) we would need to show that for all $a$ there is one $i<n$ such that for all $b_{i}$ the formula is true. Unfortunately, to derive this one needs to use the bounded collection scheme (allowing to move the quantifier bounding $i$ before the quantifier bounding $b_{i}$) and this scheme is not available in universal theories under consideration, cf. [1]. The reader can find more about this issue in [3, Sec.5] or at the end of [4, Sec.12.8]; knowing this background offers my motivation for this research (which differs perhaps from that of [7]) but it is not needed to understand the argument below.

Pich and Santhanam [7] proposed a direct way how to bypass this obstacle: simply ignore it and prove a version of the KPT theorem for (some, at least) strong propositional proof systems. For such proof systems a conditional lower bound can be indeed proved, cf. [7] or [3].

[[7]] Let P be a propositional proof system. The system has KPT interpolation if there are a constant $k\geq 1$ and $k$ p-time functions

such that whenever $\pi$ is a P-proof of a disjunction of the form

where $x$ is a $n$-tuple of atoms and $y_{1},\dots,y_{m}$ are disjoint tuples of atoms, then for all $a\in{\{0,1\}^{n}}$ the following is valid for all $b_{1},\dots,b_{m}$ of the appropriate lengths:

• •

  either $A_{i_{1}}(a,y_{i_{1}})\in\mbox{TAUT}$ for $i_{1}=f_{1}(a,\pi)$ or, if $A_{i_{1}}(a,b_{i_{1}})$ is false,

• •

  $A_{i_{2}}(a,y_{i_{2}})\in\mbox{TAUT}$ for $i_{2}=f_{2}(a,\pi,b_{i_{1}})$ or, if $A_{i_{2}}(a,b_{i_{2}})$ is false,

• •

  $\dots$, or

• •

  $A_{i_{k}}(a,y_{i_{k}})\in\mbox{TAUT}$ for $i_{k}=f_{k}(a,\pi,b_{i_{1}},\dots,b_{i_{k-1}})$.

Unfortunately, we show in this note that this property fails for strong proof systems (above a low depth Frege system) for essentially the same reasons why ordinary feasible interpolation fails for them (cf. [4, Sec.18.7]). For a set $U\subseteq{{\{0,1\}}^{*}}$ and $n\geq 1$ put $U_{n}:=U\cap{\{0,1\}}^{n}$. $\mbox{LK}_{3/2}$ is the $\Sigma$-depth $1$ subsystem of sequent calculus (cf. [4, Sec.3.4]).

Write $U(x,y)$ for a p-time relation that $y$ witnesses $x\in U$ and similarly $V(x,z)$ for $V$, with the length of both $y$ and $z$ p-bounded in the length of $x$. Let $n,m\geq 1$ and for $m$ strings $x_{1},\dots x_{m}$ of length $n$ each consider the following $2m$ propositional formulas translating the predicates $U(x,y)$ and $V(x,z)$ (which we shall denote also $U$ and $V$ in order to ease on notation):

• •

  $U(x_{i},y_{i})$: $x_{i}$ is an $n$-tuple of atoms for bits of $x_{i}$ and $y_{i}$ is an $n^{O(1)}$-tuple of atoms for bits of a witness associated with $x_{i}$ together with bits needed to encode $U$ as propositional formula suitable for P (e.g. as 3CNF),

• •

  $V(x_{i},z_{i})$: analogously for $V$,

• •

  where all $x_{i},y_{i},z_{i}$ are disjoint.

Consider the induction statement:

and write it as a disjunction with $m+1$ disjuncts:

Now replace $x_{i}\in U$ by $x_{i}\notin V$ and $x_{m}\in U$ by $x_{m}\notin V$ and write it propositionally:

Note that except the $x$-variables the $m+1$ disjuncts are disjoint.

Now apply the supposed KPT interpolation to (5). W.l.o.g. we shall assume (and arrange that in the construction below) that $x_{1}\in U$ and $x_{m}\in V$ (with witnesses $y_{1}$ and $z_{m}$, respectively). Hence Student in the KPT computation is supposed to find $i<m$ for which the $i$-th disjunct

is valid (i.e. where the induction step going from $i$ to $i+1$ fails). We shall show that the existence of such a KPT p-time Student allows to separate $U_{n}$ from $V_{n}$ with a non-negligible advantage violating the hypotheses of the theorem.

Take any $m$ such that $3\cdot 2^{k-1}\leq m\leq n^{O(1)}$ (the upper bound implies that the proof in Claim 1 is of size $n^{O(1)}$). For $1\leq i<m$ define:

Note that any string $w=(w_{1},\dots,w_{m})\in W[m]$ satisfies $w_{1}\in U$ and $w_{m}\in V$.

Let $k\geq 1$ and $f_{1},\dots,f_{k}$ be the constant and the p-time functions provided the assumed KPT interpolation for P. Assume that $1\leq i_{1}<m$ is the most frequent value $f_{1}$ computes on inputs from $W[m]$ (thinking of a P-proof $\pi$ as fixed). This maximal frequency $\gamma$ is at least $1/m$. (Here the frequency means with respect to the product of distributions ${\bf D}_{n}$ on ${\{0,1\}}^{n}$ for which it is assumed that $U_{n},V_{n}$ are hard to separate.)

Now we describe a process that transforms the assumed successful strategy​ for​ Student into a p-time algorithm​ with​ p-size advice, separating $U_{n},V_{n}$ with a non-negligible advantage.

Assume first $i_{1}<m/2$. By averaging there are $u_{1},\dots u_{m/2}\in U_{n}$ s.t. $f_{1}(w)=i_{1}$ with frequency at least $1/(2m)$ (the factor $2$ in the denominator allows us to forget about the “up to the negligible error” phrase) for all $w$ of the form:

Fix such $u_{1},\dots,u_{m/2}$ and also witnesses $a_{1},\dots,a_{m/2}$ for their membership in $U$. These will be used as advice for the eventual algorithm.

If $i_{1}\geq m/2$ then fill analogously the last $m/2$ positions by elements of $V_{n}$ and include the relevant witnesses in the advice. W.l.o.g. we assume that the first case $i_{1}<m/2$ occurred.

We interpret this situation as reducing the Student-Teacher computation to $k-1$ rounds on smaller universe $W[m/2]$. Namely, given $w=(w_{1},\dots,w_{m/2})\in W[m/2]$ define:

and run $f_{1}$ on $\tilde{w}$. If $f_{1}(\tilde{w})\neq i_{1}$, declare failure. Otherwise use the advice witnesses to produce a falsifying assignment for $A_{i_{1}}$: $U(u_{i_{1}+1},a_{i_{1}+1})$ holds.

After this first step use functions $f_{2},f_{3},\dots$ (and Claim 2 for the smaller universes) and as long as they give values $j<m/2$ always answer for Teacher using the advice strings $a_{j}$. Eventually Student proposes value $j\geq m/2$: choose the most frequent such value $i_{2}\geq m/2$ and proceed as in case of $i_{1}$, further restricting domain (6) as in binary search. Repeating this at most $(k-1)$-times the situation will be as follows:

1. (1)

   The universe will shrink at most to $W[m/(2^{k-1})]$ which is at least $W[3]$. In fact, we shall arrange in the last step that exactly $W[3]$ remains (by filling in more positions by elements of $U_{n}$ or $V_{n}$, respectively, if needed) and hence the inputs before applying the last KPT function $f_{k}$ are of the form $(w_{1},w_{2},w_{3})$ with $w_{1}\in U$ and $w_{3}\in V$.

   Note that Student gets to use $f_{k}$ because if he succeeded earlier it would violate Claim 2.

2. (2)

   The last function $f_{k}$ has to find a gap in the induction, and this itself will violate Claim 2. In particular, the gap is either between $w_{1}$ and $w_{2}$ and then $w_{2}\in V$, or between $w_{2}$ and $w_{3}$ and then $w_{2}\in U$.

3. (3)

   This process has the probability $\geq 1/(2m)$, i.e. non-negligible, of not failing in any of the $k-1$ rounds and hence it will not fail and will compute correctly the membership of (any) $w_{2}$ in $U$ or $V$ with a non-negligible probability. In all cases when the process fails output random bit $0$ or $1$ with equal probability.

This proves the theorem. ∎