Short proofs of the Kneser-Lovasz coloring principle

We prove that propositional translations of the Kneser-Lovasz theorem have polynomial size extended Frege proofs and quasi-polynomial size Frege proofs for all fixed values ofk. We present a new counting-based combinatorial proof of the Kneser-Lovasz theorem based on the Hilton-Milner theorem; this avoids the topological arguments of prior proofs for all but finitely many base cases. We introduce new "truncated Tucker lemma" principles, which are miniaturizations of the octahedral Tucker lemma. The truncated Tucker lemma implies the Kneser-Lovasz theorem. We show that the k = 1case of the truncated Tucker lemma has polynomial size extended Frege proofs. (C) 2018 Elsevier Inc. All rights reserved.