TFNP studies the complexity of total, verifiable search problems, and represents the first layer of the total function polynomial hierarchy (TFPH). Recently, problems in higher levels of the TFPH have gained significant attention, partly due to their close connection to circuit lower bounds. However, very little is known about the relationships between problems in levels of the hierarchy beyond TFNP.

Connections to proof complexity have had an outsized impact on our understanding of the relationships between subclasses of TFNP in the black-box model. Subclasses are characterized by provability in certain proof systems, which has allowed for tools from proof complexity to be applied in order to separate TFNP problems. In this work we begin a systematic study of the relationship between subclasses of total search problems in the polynomial hierarchy and proof systems. We show that, akin to TFNP, reductions to a problem in TFSigma_d are equivalent to proofs of the formulas expressing the totality of the problems in some Sigma_d-proof system. Having established this general correspondence, we examine important subclasses of TFPH. We show that reductions to the Strong Range Avoidance problem are equivalent to proofs in a Sigma_2-variant of the (unary) Sherali-Adams proof system. As well, we explore the TFPH classes which result from well-studied proof systems, introducing a number of new TFSigma_2 classes which characterize variants of DNF resolution, as well as TFSigma_d classes capturing levels of Sigma_d-bounded-depth Frege.