The proof and search complexity of three combinatorial principles

This work concerns the propositional proof complexity and computational complexity of Frankl's theorem on the trace of sets, the Kneser-Lovasz theorem, and the Tucker lemma.;We show that propositional translations of Frankl's theorem on the trace of sets has quasi-polynomial size Frege proofs. For constant values of the parameter t, we prove that Frankl's theorem has polynomial size AC0-Frege proofs from instances of the pigeonhole 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 of k. We present a new counting-based combinatorial proof of the Kneser-Lovasz theorem that 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=1 case of the truncated Tucker lemma has polynomial size extended Frege proofs.;We show that the 2-D TUCKER search problem is PPA-hard under many-one reductions; therefore it is complete for PPA. The same holds for k-D Tucker for all k ≥ 2. This corrects a claim in the literature that the Tucker search problem is in PPAD.;Frankl's theorem, the Kneser-Lovasz theorem, and the truncated Tucker lemma are all shown to give total NP search problems. These problems are all shown to be PPP-hard under many-one reductions.