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.

semanticsandmetalogical results. – François G. Dorais♦ Mar 11 '12 at 3:34expressedin each of these logics. The second sentence is aboutinferencein formal deductive systems. These are quite different matters, especially in the case of second-order logic. So there is no clash between the two. – Andreas Blass Mar 13 '12 at 17:49