Interpolation by a Game
Jan Kraíček · Mathematical logic quarterly · 1998
Abstract We introduce a notion of a real game (a generalisation of the Karchmer‐Wigderson game (cf. [3]) and of real communication complexity, and relate this complexity to the size of monotone real formulas and circuits. We give an exponential lower bound for tree‐like monotone protocols (defined in [4, Definition 2.2]) of small real communication complexity solving the monotone communication complexity problem associated with the bipartite perfect matching problem. This work is motivated by a research in interpolation theorems for prepositional logic (by a problem posed in [5, Section 8], in particular). Our main objective is to extend the communication complexity approach of [4, 5] to a wider class of proof systems. In this direction we obtain an effective interpolation in a form of a protocol of small real communication complexity. Together with the above mentioned lower bound for tree‐like protocols this yields as a corollary a lower bound on the number of steps for particular semantic derivations of Hall's theorem (these include tree‐like cutting planes proofs for which an exponential lower bound was demonstrated in [2]).