Why are higher-order logics less well-behaved?

Question

I've read about about higher-order logics (i.e. those that build on first-order predicate logic) but am not too clear on their applications. While they are capable of expressing a greater range of proofs (though never all, by Godel's Incompleteness theorem), they are often said to be less "well-behaved".

Mathematicians generally seem to stay clear of such logics when possible, yet they are certainly necessary for prooving some more complicated concepts/theorems, as I understand. (For example, it seems the reals can only be constructed using at least $2^{\text{nd}}$ order logic.) Why is this, what makes them less well-behaved or less useful with respect to logic/proof theory/other fields?

Answer 1

Unfortunately the term is ambiguous: there two kinds of semantics of higher-order languages, and only one is problematic. Consider the language of second-order arithmetic, where there are quantifiers over both natural numbers and sets of natural numbers.

First is what Quine called "set-theory in sheep's clothing": this is where quantification over sets of natural numbers is defined to be over all the sets of number that can be posited. It's the theory we use when we prove that there can be only one complete, totally ordered field. It isn't really a logic, there's no complete notion of proof formalisation for it. Wikipedia calls this "standard semantics"; I'm not sure if there is an authority for this.

Then there's Henkin semantics, which uses the rule analogous to the lambda-calculus to define a semantics for second-order quantifiers. This can be seen as still in the realm of first-order logic, in that sense that the second-order system can be translated into a first-order system conserving provability. This is how second-order arithmetic is defined.

All the theorems of the Henkin semantics will be "theorems" in the first.

Answer 2

Second-order logic does not satisfy the completeness and compactness theorems. Here is a proof that the compactness theorem fails (which itself implies that the completeness theorem fails, because completeness implies compactness). Namely, there is a second-order way (call it $F$) of expressing that a set is finite: every injective function on the set is surjective. This means that if $P$ is a relation on the product set $S \times S$ such that $P$ satisfies the conditions to be a function, and $P(x,y), P(z,y)$ imply $x=z$, then for all $w$ there is $q$ with $P(w,q)$. This statement is quantified over $P$ as well as the variables $x,y,z,w,q$ so is second-order and clearly expresses finiteness.

However, we also have the statement $T_n$ "there exist distinct $x_0, \dots x_n$ in the set," which is even first order, and states that the set has cardinality at least $n$. So the conjunction of $F$ and any finite collection of the $T_n$ is satisfiable, but all of them together cannot be satisfied.

Answer 3

A further sense in which Higher Order Logics with standard or saturated semantics (HOL, hereafter) are less well-behaved than First Order Logic (FOL, hereafter) is a direct consequences of the failure of Completeness (and thus, as explained in other answers, of Compactness). The set of logical truths and the set of correct claims of semantic consequence for these logics are not recursively enumerable.

FOL is Complete, yet not Decidable. So, we determine of an arbitrary sentences and sets of sentences of the language of FOL if those sentences are logical truths or if a set has a given sentence as a consequence. But, since FOL is Complete and proofs are finitely long, we can (in the mathematicians sense of "can") enumerate the proofs and inspect one by one, checking what sentence the proof shows as a theorem or what sentence the proof derives from what set of assumptions. This gets us a recursive enumeration of the truths and the sentence/set pairs that stand in the consequence relation. (This does not contradict the failure of decidability as we cannot conclude that since we've yet to come across a proof in out enumeration, there isn't one if only we kept looking.)

Since HOL's are not Complete, this means of showing them recursively enumerable is not available. Indeed, there can be no means; were there such a means, it could be exploited to induce a Complete proof system, and there cannot be such a Complete proof system as the HOL's are not Compact.