# Higher Order Logics

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 2nd order logic.) Why is this, what makes them less well-behaved or less useful with respect to logic/proof theory/other fields?

-
Godel's incompleteness theorem applies to first-order logic. For instance, one version of the first incompleteness theorem is that the set of true first-order sentences about the natural numbers is undecidable. –  Akhil Mathew Jul 21 '10 at 12:36
@Akhil: Thanks for your answer. I thought Godel's Incompleteness theorem applies to any recursively enumerable logic however? –  Noldorin Jul 21 '10 at 12:38
I guess I'm also looking for a more high-level picture, especially with regards to the foundations of mathematics and proof theory... –  Noldorin Jul 21 '10 at 12:40
Yeah, you're right; if I remember correctly it can be made to say more in the higher-order case. Not sure what/why I was commenting there. Sorry. –  Akhil Mathew Jul 21 '10 at 13:34

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.

-
So as I understand you, true 2nd order logic (Henkin semantics) retains all the proofs of 1st order logic and adds more, without any problems whatsoever in terms of completeness (or compactness?). Can this be extended indefinitely to higher and higher order logics, thus encompassing a greater range of proofs? Also, are there any advantages to "standard semantics". Sorry for the long list of questions. –  Noldorin Jul 21 '10 at 13:46
@Noldorin: Yes, you can come up with stronger and stronger second-order logics with the Henkin semantics, and third-order logic gives you new theorems in the second-order language. The standard semantics is a source of useful intuitions, like the uniqueness proof for the reals. –  Charles Stewart Jul 22 '10 at 7:16
@Carles: Thanks for the response. So is this "Henkin higher order logic" suitable for creating a proof theory (i.e. for verification of arbitrary proofs)? Would it be limited in any ways other than the universal Godel's Incompelteness theorem, or not? (In simple terms, is there something 'better' for HOL out there?) The Wikipedia article seems to imply Henkin semantics are lacking in some way, but perhaps I've misunderstood... Also, do Henkin semantics wok fine extending either natural deduction or sequent calculus systems? –  Noldorin Jul 22 '10 at 8:12
@Noldorin: Yes, you can use the usual technology of first-order many-sorted logic. I've argued a bit on WP with CBM & other editors on the 2nd-order logic pages about ways in which that article leads many of its readers astray (I see I said "Talking in terms of models is more honest, to my way of thinking, than what seems to me a three-way confusion of syntax, semantics and metaphysics"), but relatively little changed. –  Charles Stewart Jul 22 '10 at 8:52
That's good to know... What about my other questions, though? (Yeah, I'm always having more! Maybe it should have been a new question.) In fact I've got one or two more than I'll ask right now in a new question. –  Noldorin Jul 22 '10 at 9:01

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.

-
As Charles Stewart states, this is only true under standard semantics. Henkin semantics make higher-order logics complete (and possibly compact too?). –  Noldorin Jul 23 '10 at 18:43
Interesting... I'm surprised my logic book didn't mention that. –  Akhil Mathew Jul 23 '10 at 20:33

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.

-
HOLs are both complete and compact if you use Henkin semantics. –  Noldorin Jul 28 '10 at 7:31
Yes. This is why I said "A further sense in which Higher Order Logics with standard or saturated semantics (HOL, hereafter)". –  vanden Jul 28 '10 at 13:38