# advantage of first-order logic over second-order logic

As I look over the post that has the similar question, I began to wonder:

The only reason I found is that first-order logic can prove validity of some second-order logic formula/sentences, as some of second-order logic can be modelled by first-order logic, as provided by compactness/completeness theorem.

However, according to my knowledge, as second-order logic is more expressive, some in second-order logic do not reduce to first-order logic; therefore, some cannot be modelled by first-order logic.

First of all, is there anything I am getting wrong?

Secondly, if I am right, why do we prefer first-order logic over second-order logic (I know that first-order logic has completeness (and finite proof system) but second-order logic is STILL more expressive.....)

As I look over my question, I feel that maybe completeness (and finite proof system) of first-order theory is enough for preferring first-order logic, but still... I feel unsure.

Thanks.

• May 10, 2012 at 11:02
• Completeness is a wonderful thing. Much like we don't usually work with all functions from $\mathbb R$ to $\mathbb R$ but only with continuous, or differentiable, or continuously differentiable, or infinitely differentiable, or analytic functions. We like to work with things which behave nicely. Compactness and completeness are very nice. May 10, 2012 at 11:09
• @Asaf: in principle, if you didn't have compactness or completeness, but you had a nice model theory anyway, it might be possible to work with that and just not have a good proof theory. One example of this is finite model theory. But in the particular case of second-order logic with full semantics, there is no proof theory and the model theory requires answering lots of set-theoretic questions, so it's hard to make much progress at all. May 10, 2012 at 11:35

You already know that first-order logic has a completeness theorem. That means that we can determine validity in first-order logic by looking at deductions - it makes proof theory possible. In second-order logic with full semantics, because there is no completeness theorem, to study things like validity we end up having to answer questions about the power set of the domain.

Here's an example. There is a sentence $\phi_1$ in the second-order language of ordered fields that characterizes the real numbers, up to isomorphism, in second-order logic with full semantics. There is another sentence $\phi_2$, in the language with just equality, which states that the domain has cardinality $\aleph_1$ (that is, any model of $\phi_2$ in second-order logic with full semantics has a domain of that cardinality). Now in order to show that $\phi_1 \to \phi_2$ in this logic, we would have to prove the continuum hypothesis, and to disprove that implication we would have to disprove the continuum hypothesis (this is because $\phi_1$ has only one model up to isomorphism).

Examples like this give us a sense that studying second-order logic with full semantics comes down, in many cases, to studying set theory. But if that's that case, many people say, why not just study set theory, as with ZFC? Studying set theory in the guise of "logic" only seems to obfuscate what's going on.

Moreover, for those who want to use the logic for foundational purposes, it is unattractive to pick a logic that seems to already have the answers to set-theoretic questions like the continuum hypothesis built into it - this goes against the idea that "logic" itself should make a minimal number of ontological assumptions.

This sort of argument was made in detail by Quine, who called second-order logic with full semantics "set theory in sheep's clothing". Not everyone agrees with this, and many people do use second-order logic with Henkin semantics as a way to keep the expressiveness without including the set theory. But the dominant opinion accepts Quine's argument.

I also recommend "The Road to Modern Logic-An Interpretation" by José Ferreirós, Bulletin of Symbolic Logic (2001), 441-484. This paper has a very nice historical study of the development of what is now called first-order logic.

• But theorem prover like Isabelle und HOL Light use higher-order logic. Mar 22, 2018 at 23:09
• @jjcale: because those systems only look at provability, it doesn't make any difference to them whether we interpret the results in full semantics or in Henkin semantics; those provers only use the syntax of higher order logic, which we could equally well interpret as a kind of first-order logic if we wanted to. Mar 22, 2018 at 23:13