From what I understand, Higher Order Logics cannot be reduced to lower ones -- for example, Second Order Logic cannot be reduced to FOPL. But, can't I use FOPL to reason about the behavior of a Turing Machine running a second order logic solver, and thus solve second order logic problems in FOPL?
Edit: I mean reducibility in the sense of http://en.wikipedia.org/wiki/Second-order_logic#Non-reducibility_to_first-order_logic that there are second order sentences that cannot be expressed in first order logic. I suppose solve was the wrong word to use. What I meant is that I don't see why one can't view application of the inference rules of second order logic as just string rewriting, and so come up with a way of representing such strings and the inference rules in FOPL, and thereby perform whatever inference I could in Second Order Logic using FOPL.