Yes, it makes sense to consider such variants of the problem. Apart from the complexity-theoretic motivation, they arise quite naturally in the study of weak fragments of arithmetic (bounded arithmetic): for example, it is known that Buss’ theory $S_2$ (or equivalently, $I\Delta_0+\Omega_1$) is finitely axiomatizable if and only if $S_2$ proves that the polynomial hierarchy collapses (in an explicit way, i.e., there is a $\Sigma^P_n$-algorithm $M$ such that $S_2$ proves that $M$ solves a $\Sigma^P_{n+1}$-complete problem).

Unfortunately, the answer to the second part of your question is no, it does not seem to make the problem any easier, even if we ask for provability in an extremely weak theory (such as PV, and similar fragments of bounded arithmetic).

Yes, it makes sense to consider such variants of the problem. Apart from the complexity-theoretic motivation, they arise quite naturally in the study of weak fragments of arithmetic (bounded arithmetic): for example, it is known that Buss’ theory $S_2$ (or equivalently, $I\Delta_0+\Omega_1$) is finitely axiomatizable if and only if $S_2$ proves that the polynomial hierarchy collapses (in an explicit way, i.e., there is a $\Sigma^P_n$-algorithm $M$ such that $S_2$ proves that $M$ solves a $\Sigma^P_{n+1}$-complete problem).

Unfortunately, the answer to the second part of your question is no, it does not seem to make the problem any easier, even if we ask for provability in an extremely weak theory (such as PV, and similar fragments of bounded arithmetic).

If you want to learn more about these issues, you can consult Bounded Arithmetic, Propositional Logic, and Complexity Theory by Krajíček, or Logical foundations of proof complexity by Cook and Nguyen.