This is a question about terminology, as I am clearly confused on the topic.
The Wikipedia page on higher-order logic defines it as follows:
Higher-order logic is the union of first-, second-, third-, …, nth-order logic; i.e., higher-order logic admits quantification over sets that are nested arbitrarily deeply.
So this is worded vaguely. Taken at face value, it says that higher-order logic is the union of all logics up to some arbitrary $n$. This would imply that higher-order logic is not one thing, but that for each $n$ there is a higher-order logic, so that higher-order logic is sort of just a catch-all term for logic of some order > 2, or what have you.
But then it says that higher-order logic admits quantification over arbitrary-order predicates, which one could interpret as being the union of first-, second-, third-, … order logic without stopping at any $n$, meaning quantifiers of all orders are included. However, this does not imply that there are "infinite-order" predicates that can simultaneously quantify over all finite-order predicates, just that you can have arbitrarily large finite-order predicates.
Then on this Stanford page, it says under "Higher-Order Logic" that $\omega$-order logic is "type theory," with continuation into the transfinite being conceivable.
Is the correct idea that higher-order logic has all quantifiers of finite order, each of which quantifiers over all predicates up to a certain order type, whereas type theory has infinite-order quantifiers enabling you to quantify over all finite-order predicates?
Best Answer
While they don't own the term, the HOL family of mechanized proof assistants (HOL4, HOL Light, Isabelle/HOL) is highly successful and influential. These are all implementations of (extensions of) simple type theory as described by this paper referenced on the HOL4 site. The most significant extension that applies to all of them is that they use a polymorphic typed lambda calculus and not purely a simply typed lambda calculus.
While "type theory" nowadays usually means systems based on typed lambda calculi or the study thereof, to the extent that it is being contrasted to HOL, it is likely to mean specifically dependently typed lambda calculi. Even more specifically, it often means a descendant of Intuitionistic or Martin-Löf Type Theory (ITT). Again, there are highly successful and influential implementations of these, most notably Coq and the LF-family including Twelf. Dependently typed lambda calculi generalize simply typed lambda calculi (and in practice, often generalize polymorphic lambda calculi as well), so something like HOL is, roughly speaking, a sub-language of ITT. However, these systems are used in dramatically different ways. In HOL, a proposition is literally a Boolean expression and the goal is to show that it is the true Boolean. In ITT, a propositions-as-types perspective is typically taken so that a proposition is modeled as a type and the goal is to produce a value of that type.
People usually don't mean Russell's theory of types unless they are talking about the early history of formal logic. "Higher order logic" could possibly also be used simply as a contrast to first-order logic, i.e. as "not-first-order logic" and in that sense second-order logic would be a "higher order logic", but people rarely talk about third- or fourth-order logic, so they'd be likely to specifically refer to second-order logic where most of the good and bad things that come with moving beyond first-order logic have already occurred.