An NP search problem is the problems of finding a witness to the given NP predicate, and TFNP is the class of total NP search problems. TFNP contains a number of subclasses containing natural problems; for example, PLS is the class of efficient local search heuristics. These classes are characterized by the combinatorial principle that guarantees the existence of a solution; for example, PLS is the class of such problems whose totality is assured by the principle “every dag with at least one edge has a sink.” We show many strong connections between these search classes and the computational power—in particular the proof complexity—of their underlying principles. These connections, along with lower bounds in the propositional proof systems Nullstellensatz and bounded-depth LK, allow us to prove several new relative separations among PLS, and Papadimitriou’s classes PPP, PPA, PPAD, and PPADS.