Type theory vs higher-order logic

This is a question about terminology, as I am clearly confused on the topic.

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?

• This paper (sciencedirect.com/science/article/pii/S157086830700081X) describing type theory also calls it higher-order logic. Every variable in it belongs to a definite order, so quantifiers only quantify over predicates of a certain order, not the union of predicates of different orders. – Matt Dickau Oct 13 '17 at 19:07
• I guess this is "simple" type theory, which they distinguish from Russell's ramified type theory. It seems to be different from the way I see type theory described elsewhere. – Mike Battaglia Oct 13 '17 at 19:34
• There is nothing vague about the Wikipedia definition apart from the fact that (in context) the article is defining the language of higher-order logic to be the union of the languages of $n$-th order logic for all $n$. What's wrong with that? – Rob Arthan Oct 13 '17 at 20:39
• If you are just complaining about the wording of the Wikipedia article, you should take that up on Wikipedia. You are also reading too much into the Standard article, the $\omega$-order logic discussed there is exactly the same as what the Wikipedia article means (but doesn't quite describe correctly), i.e., the union $\bigcup_{n \in \omega} \cal L_n$ where $\cal L_n$ is the language of $n$-th order logic. This doesn't allow a single quantifier to range over predicates of all orders. As the Stanford article says, there are conceivable extensions, but that's not what they are talking about. – Rob Arthan Oct 13 '17 at 20:48
• I am just trying to help you make sense of the two references you mention. Church's simple type theory and higher-order logic (in the sense of the Wikipedia article) are equivalent and both can be viewed as the union of a family of finite-order logics. But there are many other type theories and many generalisations of higher-order logic. So your question as phrased ("is the correct idea that ...?") isn't really answerable in general. It can only be answered in the context of a specific system. – Rob Arthan Oct 13 '17 at 21:58

• The Seven Virtues of Simple Type Theory which I linked above describes the embedding of $n$th-order logics into STT and states (but does not further prove) a theorem that the embeddings are faithful. Furthermore, the embedding does not rely on definite description for the "usual" connectives. Ignoring definite description (or targeting a logic with it), the only tricky part about going the other way is handling abstraction of functions which we can either encode as functional relations or disallow with a minor tweak. – Derek Elkins Oct 20 '17 at 23:13
• That much I understand, but why define $\mathsf{T}$ like that? Why not just define $\mathsf{T}$ as the primitive boolean value true directly, expressed as a primitive constant element of $\ast$? – Mike Battaglia Oct 22 '17 at 21:56