We consider Total Functional $\NP$ ($\TFNP$) search problems. Such problems are based on combinatorial principles that guarantee, through locally checkable conditions, that a solution to the problem exists in an exponentially-large domain, and have the property that any solution has a polynomial-size witness that can be verified in polynomial time. These problems can be classified according to the combinatorial principle that guarantees the existence of a solution; for example, $\PPP$ is the class of such problems whose totality is assured by the Pigeonhole Principle. We show many strong connections between relativized versions of 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 the classes $\PLS$, $\PPP$, $\PPA$, $\PPAD$, and $\PPADS$.