Are higher order logics substantially stronger than second order

Question

Do we get much by using logics of order higher that 2? Does each transition to next level provides much power?

Answer 1

There is a precise sense in which third-order and higher-order logics, with full semantics, are no stronger than second-order logic with full semantics. For any formula of higher-order logic $\phi$ there is another formula of second-order logic $\phi'$ such that $\phi$ is valid in full higher-order semantics if and only if $\phi'$ is valid in full second-order semantics. This is described in more detail in the Stanford Encyclopedia of Philosophy article on higher-order logic. It is a standard fact for any course about second-order logic.

Answer 2

What is "power"? What is "full semantics"? If you use ZFC set theory to define "full semantics", then ZFC set theory is mostly responsible for your "power".

If you use Henkin semantics, then your comprehension axioms will determine your "power". If you just allow predicative comprehension axioms, which can only quantify over lower levels, then you should not gain any power at all, not even for second order logic over first order logic. If you allow impredicative quantification over equal or lower levels, then each new level provides more power.

However, the typical "foundational" higher order logic systems are even more liberal or aggressive with respect to the allowed impredicative quantification in the comprehension axioms. They follow Frank P. Ramsey and Rudolf Carnap, who

accepted the ban on explicit circularity, but argued against the ban on circular quantification.

So in this case, there is no restriction at all with respect to the allowed quantification in the comprehension axioms. As a consequence, each new level again provides more power. The complete system has the same consistency strength as simple type theory, bounded Zermelo set theory, Mac Lane set theory or NF(U).

---

Maybe back to the question of "power". If you proved a formula $F(P,Q,x,y)$ to be a tautology, then you have automatically also proven that $F(P(z),Q(z),x(z),y(z))$ is a tautology as well for any $z$ which doesn't occur in $F(P,Q,x,y)$. In higher order logic, the same is true for $F(P(Z,z),Q(Z,z),x(Z,z),y(Z,z))$. It is this power to introduce "abbreviations" which allows you to write down proofs concisely. I don't know exactly how much space you can save by this, but it is at least an exponential gain in conciseness in some cases. I guess the possible gain in conciseness can even be double exponential or double double ... exponential for specifically construed cases.

---

Maybe back to the question of "full semantics". You might also interpret higher order variables with respect to a "last word semantics". For the Peano axioms this would mean, whatever way you introduce to define a predicate (for example you may add a new function for exponentiation, or a new predicate for "whatever"), the induction axiom will still be true for any formula making use of any of the available functions and predicates. But the "last word" property becomes problematics as soon as there are more than two axioms which both have the last word, because obviously there can be only one last word, or if there is more than one last word, then these words can contradict each other.