Sign up ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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 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.

share|cite|improve this question
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 -… – 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

1 Answer 1

up vote 2 down vote accepted

As François G. Dorais pointed out you have to read carefully wikipedia's article.

The main difference in expressiveness between first order logic and second order logic is given by the semantics.

We can turn a second order language in a special kind of first order language simply considering second order variables as variables ranging over a different sort, or making no distinction between first and second order variables and using two unary predicates, one for first order objects (i.e. individuals), the other for second order ones (i.e. relations), to distinguish when a variable have to range over individuals or when it ranges over relations.
With these trick we can completely translate second order syntax in a first order one.

The same trick cannot be applied in general for the second order semantics, in particular for the standard semantics. In standard semantics we impose that in every interpretation the second order variables range over the power set of the domain of the interpretation (i.e. the range of variation for first order variables). If we want to reduce second order semantics to first order ones with the trick above we cannot require such strict condition, in this case the domain of variation for second order variable could be every family of subset of the domain of the interpretation. These kind of things are allowed in Henkin semantics which are simply a rewriting of first order multisorted semantics for second order logics but which are also weaker semantics (less expressive) when compared with standard ones.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.