Short proofs of the Kneser-Lovász coloring principle (Q1641004)

One of the long-standing open problems in proof complexity is to separate the \textit{Frege} and \textit{extended Frege} (EF) proof systems; even though it is commonly believed that extended Frege should have exponential speed-up over Frege, not even a superlinear separation has been proved. A part of the problem is that we do not even know of good \textit{candidates} for tautologies that have polynomial-size EF proofs, but plausibly require exponential-size Frege proofs. (Here, we are looking for simple combinatorial tautologies rather than reflection principles and the like, as it is assumed that the latter are unlikely to be amenable to direct lower bound techniques.) While various examples have been proposed, virtually all of them turned out to have polynomial or quasipolynomial Frege proofs. \textit{G. Istrate} and \textit{A. Crãciun} [Lect. Notes Comput. Sci. 8561, 138--153 (2014; Zbl 1423.03243)] proposed tautologies expressing the \textit{Kneser-Lovász theorem}, which gives a tight lower bound on the chromatic number of the Kneser graphs \(K(n,k)\) (whose vertices are \(k\)-element subsets of \([n]\), and edges connect disjoint sets). For fixed \(k\), this can be expressed by propositional formulas (DNF) of size polynomial in \(n\). Common proofs of the Kneser--Lovász theorem employ topological or other high-level methods, which are not readily formalizable in weak proof systems. The main result of the present paper is that for any constant \(k\), the Kneser-Lovász tautologies have polynomial EF proofs, and quasipolynomial Frege proofs (hence they cannot yield a more than quasipolynomial separation between Frege and EF). This is shown by an infinite descent argument using elementary counting, which gradually reduces the general case to the base case of constant-size \(n\) (roughly \(n\le k^4\)); the latter has a constant-size brute-force Frege proof just because the Kneser-Lovász theorem is true in the real world. While this is not indicated in the paper, the argument shows that for constant \(k\), the Kneser-Lovász theorem is provable in the bounded arithmetical theory \(S^1_2\) (by the EF argument), and even in \(R^1_2\) (by the Frege argument). Since the non-uniformity of the proof of the base case is unsatisfactory, the authors explore other approaches that might lead to better proofs. They introduce \textit{truncated Tucker lemma} tautologies, and show that the Kneser-Lovász tautologies have poly-size constant-depth Frege derivations from the truncated Tucker lemma. However, the proof complexity of the truncated Tucker lemma tautologies themselves remains largely unknown: the authors only show that they have poly-size EF proofs in the simplest \(k=1\) case.