The motivation for this question is the following: Say we have a formula $\phi$ in peano arithmetic, and we have proof $\pi$ of $\phi$ using possibly higher order arithmetic or category theory (that is the proof assumes larger proof-theoretic ordinals). It is often the case that the inaccessible cardinal required to do category theory is completely overkill for the result, as the proof does not actually do any complicated induction. For a precise example, FLT depends on category theory yet is believed to have a proof in PA.
I would like to know if there are any results pertaining to the following question: Is there a general (semi)-decision procedure which, given a formula $\phi$ in a given system of strength $\alpha$, analyzes a proof $\pi$ in a system of strength $\beta>\alpha$ and outputs a more elementary proof of $\phi$ if such a proof exists, possibly under certain constraints?