8
$\begingroup$

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?

$\endgroup$
5
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ In particular, higher-order logic in general has a syntax that looks exactly like type theory, with not only sets but also relations and functions of various sorts. The reason someone might hear primarily about quantification over sets is that in the particular context of higher-order arithmetic the other relations and functions can be coded as sets. $\endgroup$ – Carl Mummert Oct 1 '13 at 20:15
  • 1
    $\begingroup$ This is a comment not an answer imho. $\endgroup$ – cic May 26 '16 at 15:44
1
$\begingroup$

Yes, it is the same notion.

There are two parts to the answer. First, consider:

  • In "first order logic", a formula (predicate) refers to individuals.
  • In "second order logic", a formula (predicate) may refer to individuals and formulas(predicates) of first order logic.
  • In "n-th order logic", a formula (predicate) may refers to individuals and predicates of first order, second ... 'n-1'th order logic.

In "higher order logic", as a synonym for "Church's type theory", we have syntax for (typed) functions and a basic type of truth values, so we can identify sets with their characteristic function from individuals to truth values. It is easy to see we can construct formulas belonging to logic for any order, because a functions can take another functions as argument (i.e. it includes all finite order logics).

This definition is from Andrews "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof."

Now, for the second part.

Today, there are many more variants of type theory (e.g. one may want to distinguish sets from propositions). One may wish to make precise statements whether "higher-order" in one language corresponds to "higher order" in the other. For a semi-formal argument, one should then have an explicit encoding ready, such as the one in Felty, Miller "Encoding a Dependent Type Lambda Calculus in Higher Order Logic."

However, remaining on an informal level: it seems safe to expect that "functions" in one system will correspond to something like functions in the other, and that the above intuition (or intent) from classical mathematical logic carries over across formalisms. Any type theory will distinguish a set of sets of numbers from a set of numbers.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.