Abstract
The feasible interpolation theorem for semantic derivations from [J. Krajicek, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J.
Symbolic Logic 62(2) (1997) 457-486] allows to derive from some short semantic derivations (e.g. in resolution) of the disjointness of two NP sets U and V a small communication protocol (a general dag-like protocol in the sense of Krajicek (1997) computing the Karchmer-Wigderson multi-function KW[U, V] associated with the sets, and such a protocol further yields a small circuit separating U from V. When U is closed upwards, the protocol computes the monotone Karchmer-Wigderson multi-function KWm [U,V] and the resulting circuit is monotone.
Krajicek [Interpolation by a game, Math. Logic Quart. 44(4) (1998) 450-458] extended the feasible interpolation theorem to a larger class of semantic derivations using the notion of a real communication complexity (e.g. to the cutting planes proof system CP).
In this paper, we generalize the method to a still larger class of semantic derivations by allowing randomized protocols. We also introduce an extension of the monotone circuit model, monotone circuits with a local oracle (CLOs), that, does correspond to communication protocols for KWm [U, V] making errors.
The new randomized feasible interpolation thus shows that a short semantic derivation (from a certain class of derivations larger than in the original method) of the disjointness of U, V, U closed upwards, yields a small randomized protocol for KWm [U, V] and hence a small monotone CLO separating the two sets. This research is motivated by the open problem to establish a lower bound for proof system R(LIN/F-2) operating with clauses formed by linear Boolean functions over F-2.
The new randomized feasible interpolation applies to this proof system and also to (the semantic versions of) cutting planes CP, to small width resolution over CP of Krajfeek [Discretely ordered modules as a first-order extension of the cutting planes proof system, J. Symbolic Logic 63(4) (1998) 1582-1596] (system R(CP)) and to random resolution RR of Buss, Kolodziejczyk and Thapen [Fragments of approximate counting, J.
Symbolic Logic 79(2) (2014) 496-525]. The method does not yield yet lengths-of-proofs lower bounds; for this it is necessary to establish lower bounds for randomized protocols or for monotone CLOs.