This work concerns the propositional proof complexity and computational complexity of Frankl's theorem on the trace of sets, the Kneser-Lovász 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-Lovász 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-Lovász 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-Lovász 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-Lovász 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.