This is a retry of question Would Wiles proof of Fermat theorem reduce if you fill in the variables?. I stated that question badly, but my intention are genuine and hope do to a better job here.
First of all, with proof reduction I mean that there is a set of reduction rules (algorithm) that simplifies or alters a proof written in a formal logic. In such way, that the adapted proof will have a certain property after executing, for instance no higher order theorems, or no induction.
A normal mathematical proof is not likely to be reduced, because the mathematician did his best to have a minimum proof. However, if certain variables of the end theorem of the proof are replaced by constants, and this is substituted back over the proof, then a reduction algorithm may simplify such proof. Still, there is no guarantee that significant simplification can be performed on the proof.
Things get a little different when all variables of the end theorem are instantiated to constants, such that the end theorem is a quantifier free theorem. In that situation, ones hopes that the proof collapses and reduces to a trivial proof. This gives the mathematician confidence, that the end theorem is indeed correct (paradoxes have the property that they do not reduce).
If you do such reduction manually, then it often turns out not to be difficult. In case of induction, it can be unrolled if the n is known. However, to do this automated with an algorithm, is far from trivial. There is sequent calculus and cut-elimination and this is not simple.
Suppose there is a second order logic proof and the variables of the end theorem are replaced by constants and substituted back over the proof. For that, it would be nice to have an algorithm that reduces to proof to a trivial first order logic (+PA) proof.
However, it is impossible that we can prove in second order logic that such algorithm is guaranteed to give result. Because, falsum is a quantifier free formula, and by proving that the algorithm halts and gives result, we actually proof the relative consistency of second order logic to first order logic. Since, second order logic can prove the consistency of first order logic, it would mean that second order logic would prove its own consistency, which is not possible, unless it is inconsistent.
Still, the algorithm could exist (and in fact, if second order logic is consistent, it exists, by just searching for the theorem in first order logic), but you need a logic stronger than second order logic, to prove that the algorithm actually works.
Given above I expect (and maybe I am wrong here), that there are second order logical proof that do not reduce straight forward in a first order trivial proof, if all variables are filled in.
I am curious how those proofs look like and if there is a simple natural example (so, that is my question). Also if there is any literature in this area (in case I see it all wrong :-)