Short proofs of the Kneser-Lovász coloring principle
type: Item
instance of: scholarly article
title: Short proofs of the Kneser-Lovász coloring principle
zbMATH Open document ID: 1443.03040
author: James Aisenberg
author: Maria Luisa Bonet
author: Samuel R. Buss
author: Adrian Crăciun
author: Gabriel Istrate
published in: Information and Computation
publication date: 2018-06-14T00:00:00Z
full work available at URL: http://hdl.handle.net/2117/124274
review text: 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, th…
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 05C15
zbMATH DE Number: 6889859
zbMATH Keywords: proof complexity
zbMATH Keywords: extended Frege
zbMATH Keywords: Kneser-Lovász theorem
zbMATH Keywords: chromatic number
zbMATH Keywords: Tucker lemma
MaRDI profile type: Publication
OpenAlex ID: W2790199059
Wikidata QID: Q113872845
cites work: Short Proofs of the Kneser-Lovász Coloring Principle
cites work: Q4375783
cites work: Improved witnessing and local improvement principles for second-order bounded arithmetic
cites work: Q4850545
cites work: Quasipolynomial size proofs of the propositional pigeonhole principle
cites work: Q3794177
cites work: Polynomial size proofs of the propositional pigeonhole principle
cites work: Propositional consistency proofs
cites work: Q4263835
cites work: Propositional proofs and reductions between NP search problems
cites work: Q4133141
cites work: Q4152212
cites work: The relative efficiency of propositional proof systems
cites work: INTERSECTION THEOREMS FOR SYSTEMS OF FINITE SETS
cites work: Non-trivial intersecting families
cites work: A constructive proof of Tucker's combinatorial lemma
cites work: SOME INTERSECTION THEOREMS FOR SYSTEMS OF FINITE SETS
cites work: Short Proofs for the Determinant Identities
cites work: Proof Complexity and the Kneser-Lovász Theorem
cites work: Dual weak pigeonhole principle, Boolean complexity, and derandomization
cites work: The provably total NP search problems of weak second order bounded arithmetic
cites work: Q4856172
cites work: Kneser's conjecture, chromatic number, and homotopy
cites work: A combinatorical proof of Kneser's conjecture
cites work: On the complexity of the parity argument and other inefficient proofs of existence
cites work: Q3755452
cites work: Q3773878
cites work: The Complexity of Propositional Proofs
cites work: Q3882451
cites work: Generalized Kneser coloring theorems with combinatorial proofs
DOI: 10.1016/J.IC.2018.02.010
Recommended article: Short Proofs of the Kneser-Lovász Coloring Principle
Recommended article: Short proofs of coloring theorems on planar graphs
Recommended article: A short proof for Chen's alternative Kneser coloring lemma
Recommended article: Generalized Kneser coloring theorems with combinatorial proofs
Recommended article: A short list color proof of Grötzsch's theorem
Recommended article: A Coloring Proof of a Generalisation of Fermat's Little Theorem
Recommended article: Easier proofs of coloring theorems
Recommended article: Q3484859
Recommended article: Q3015575
Recommended article: A new proof of the colored Kruskal-Katona theorem
description: scientific article; zbMATH DE number 6889859