# What is the relationship between FOPL and Higher Order Logics?

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.

-
You should specify what you mean by "reducing" one logic to another and what you mean by "problems" of a logic and "solving" such problems. I conjecture that, once you make your question precise, the answer will be evident. – Andreas Blass Mar 11 '12 at 1:35
Please read the entire Wikipedia article, especially the sections titled semantics and metalogical results. – François G. Dorais Mar 11 '12 at 3:34
You might also want to read this old answer of mine - mathoverflow.net/questions/71344/… – François G. Dorais Mar 11 '12 at 4:06
As I predicted, once you make the question precise, the answer becomes evident: The first sentence of your question is about semantics, i.e., about what can be expressed in each of these logics. The second sentence is about inference in 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