# 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. Oct 13, 2017 at 19:07
• 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? Oct 13, 2017 at 20:39
• It's vague specifically because it doesn't say the union for all n, it says the union up to some n. It's like the difference between $f(1) + f(2) + f(3) + ... + f(n)$ and $f(1) + f(2) + f(3) + ...$. As this notation is commonly used, the latter is understood to continue forever as an infinite series, the former is finitely long and has $n$ terms. Oct 13, 2017 at 20:41
• 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. Oct 13, 2017 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. Oct 13, 2017 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. Oct 20, 2017 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$? Oct 22, 2017 at 21:56