Is higher order type theory the same as higher order logic?

Question

The internal language of a topos is higher order intuitionistic type theory (or logic). Here the higher order simply refers to allowing function types.

In mathematical logic we have higher-order logics where quantification is allowed not just sets, but powers of sets.

Are these the same notion of higher-order here?

Answer 1

Basically yes. See Introduction to Higher-Order Categorical Logic by Lambek and Scott 1988 for the details.

Answer 2

There are really two different meanings of "higher-order":

Referring to syntax

Systems that include variables for one or more types of "individuals" and also variabels for "sets" of individuals, "relations" on the set of individuals, or "functions" from individuals to individuals are called "higher order".

One common system for higher-order logic (with one type of individuals) is the following inductive definition of a large collection of "types":

• The set of individuals is a type
• If $\sigma_1, \ldots, \sigma_k$ are types, then there is a type $\sigma_1 \times \cdots \times \sigma_k$ whose elements are sequences $(a_1, \ldots, a_k)$ where $a_i$ is of type $\sigma_1$ for each $i \leq k$. There are also projection functions to extract each component of such a sequence.
• If $\sigma$ and $\delta$ are types, there is a type $\sigma \to \delta$ whose elements are functions with domain $\sigma$ and codomain $\delta$ (i.e. functions that take an input of type $\sigma$ to an output of type $\delta$)
• If $\sigma$ is a type, there is a type $P(\sigma)$ each element of which is a subset of $\sigma$

The logic contains, for each type, a universal quantifier over objects of that type and an existential quantifier over objects of that type. As you can see, this looks just like a kind of type theory. One difference is that higher-order logic is more like classical logic than intuitionistic type theory. In particular there are no dependent types and no "judgments", just formulas and proofs that are analogous to the ones from first-order logic.

Indeed, all the syntax of this "higher-order" logic can be interpreted as just a multi-sorted first-order logic.

Referring to semantics

"Higher-order semantics", also called "full semantics" and "standard semantics", are a particular semantics for higher-order logic in which the "higher order sorts" are taken to include all the elements they possible can. For example, in full semantics, once the set of individuals $i$ is determined for a model, the collection of objects of type $P(i)$ in that model must be contain all subsets of $i$, and the collection of objects of type $i\to i$ must contain all functions from $i$ to $i$, etc. In this way, all the higher types in a model are determined solely by the set of individuals in the model.

In "Henkin semantics" for higher-order logic, the collection of objects of type $P(i)$ in the model might be a proper subset of the powerset of $i$ in that model, and the collection of objects of type $i \to i$ might be just a proper subset of all the function from $i$ to $i$, etc.

These semantics have very different properties. Full semantics, by more or less arbitrarily reducing the number of models, allows for categorical theories for the natural numbers and the real numbers. Henkin semantics have the same completeness and compactness properties as first-order logic.