Simple Type Theory = HOL — the basis of higher-order logic

Building logic on top of the typed lambda calculus

Goal of this page

Understand simple types (base types and function types) and the typed lambda calculus, and see how higher-order logic (HOL), obtained by adding equality and quantifiers on top, is a system that can quantify even over predicates and functions. Know that this is the basis of HOL Light / Isabelle.

1. Why do we need types?

If we naively allow "anything may be applied to anything", we can write expressions such as $x\,x$ (applying $x$ to itself). Russell's paradox, "the set of all sets that do not contain themselves", which caused a contradiction in naive set theory, has the same essence: unrestricted self-application.

Church chose to assign a type to every term and to require the types of a function and its argument to match, thereby cutting off this danger at the level of grammar. An expression whose types do not match simply "cannot be written". This is simple type theory (the simply typed lambda calculus, 1940).

2. Simple types — base types and function types

Types are built up from a few base types by forming function types. HOL takes two base types.

  • $\iota$ (iota): the type of individuals (objects, e.g. natural numbers or points)
  • $o$ (omicron): the type of truth values (propositions; the two values true and false)

Then, from types $\sigma, \tau$ we form the function type $\sigma \to \tau$ (the type of functions taking a $\sigma$ and returning a $\tau$). We read $\to$ as right-associative, so $\sigma \to \tau \to \rho$ denotes $\sigma \to (\tau \to \rho)$.

Typing rules (the essentials)

We write $t : \tau$ to say that term $t$ has type $\tau$. There are basically just two rules.

Application: if $f : \sigma \to \tau$ and $a : \sigma$ then $f\,a : \tau$.
Abstraction: if $t : \tau$ under $x : \sigma$, then $\lambda x{:}\sigma.\, t : \sigma \to \tau$.

$$\dfrac{f : \sigma \to \tau \quad a : \sigma}{f\,a : \tau} \qquad \dfrac{x:\sigma \;\vdash\; t : \tau}{\lambda x{:}\sigma.\,t : \sigma \to \tau}$$

Application is allowed only when the argument type $\sigma$ matches exactly. Hence $x\,x$ would require $x$ to be both $\sigma \to \tau$ and $\sigma$ at once, and since $\sigma \neq \sigma \to \tau$ it has no type. Self-application is rejected by the grammar.

A predicate is represented as a function taking an individual and returning a truth value, i.e. type $\iota \to o$. For example "$x$ is prime" is a term of type $\iota \to o$. A binary relation has type $\iota \to \iota \to o$.

3. Higher-order quantification

In first-order logic, one can quantify only over individuals (the $x$ in "for all $x$" has type $\iota$). In higher-order logic, one can also quantify over predicates and functions themselves — that is, over objects of higher type such as $\iota \to o$ or $\iota \to \iota$.

The quantifier $\forall$ can be seen as a higher-order function taking a predicate (type $\iota \to o$) and returning a truth value (type $o$). Universal quantification over individuals has type $(\iota \to o) \to o$.

A quantifier is a "function that takes a predicate" predicate P ι → o pass ∀ (universal) (ι → o) → o returns a truth value o ∀ P. P(x) reads "for every predicate P" = higher-order
Figure 1: Higher-order quantification. A predicate $P$ has type $\iota \to o$, and the universal quantifier $\forall$ takes that predicate and returns a truth value $o$, so it has type $(\iota \to o) \to o$. Being able to quantify over predicates themselves ($\forall P.\,\dots$) is the defining feature of higher-order logic.
Read Figure 1 as text

A predicate $P$ takes an individual $\iota$ and returns a truth value $o$, so its type is $\iota \to o$. The universal quantifier $\forall$ takes that predicate $P$ as its argument and returns a truth value $o$, so its type is $(\iota \to o) \to o$. First-order logic quantifies only over individuals $x$, whereas higher-order logic can also quantify over objects of higher type such as the predicate $P$.

With higher-order quantification, a principle like mathematical induction, "for every property $P$", can be written as a single formula inside the system rather than as a meta-level note. The power is great, but the price is that the completeness of first-order logic (every valid formula is provable) does not hold under the standard semantics (this relates to the incompleteness discussed in the Advanced level).

4. HOL — from a few axioms

Higher-order logic (HOL) is the simply typed lambda calculus together with a truth-value type $o$, an equality $=$, and the logical connectives and quantifiers. What is striking is that HOL takes equality as the most primitive notion, from which the other connectives can be defined (for example "true" can be introduced as $(\lambda x.\,x) = (\lambda x.\,x)$).

HOL Light and Isabelle/HOL build this system on just a few axioms. Representative ones are the following three.

  • Equality axioms (reflexivity, substitution, etc.: equals may be replaced by equals)
  • Choice (Hilbert's $\varepsilon$: if something satisfies a property $P$, one can be chosen; the axiom is $(\exists x.\,P\,x) \Rightarrow P(\varepsilon\,P)$, where $\varepsilon\,P$ denotes "something satisfying $P$", if any)
  • Infinity (guarantees that the type $\iota$ of individuals is infinite, allowing the natural numbers to be constructed)

From this small starting point one can define the natural numbers, the reals, and set-theoretic constructions, and develop much of mathematics in a machine-checkable form. Since type checking is decidable and the inference rules are simple, HOL is easy to implement as a small trusted kernel. This is why HOL is chosen as the foundation of proof assistants (Proof Assistants & LCF).

Summary

Key points

  • Simple type theory: build types from base types $\iota$ (individuals), $o$ (truth values) and function types $\sigma \to \tau$
  • By matching types, self-application like $x\,x$ is ruled out at the level of grammar
  • Predicates are $\iota \to o$, binary relations $\iota \to \iota \to o$
  • Higher-order quantification: one can quantify over predicates and functions themselves ($\forall P.\,\dots$)
  • HOL = typed lambda calculus + equality and quantifiers. From a few axioms (equality, choice, infinity) it develops mathematics and forms the basis of HOL Light / Isabelle

Frequently Asked Questions

What is simple type theory?

A system based on the typed lambda calculus of Church (1940). Every term is assigned a type, and by giving a function $f$ the type $\sigma \to \tau$ and its argument the type $\sigma$, dangerous expressions such as self-application are ruled out at the level of grammar. HOL is this typed lambda calculus together with a truth-value type $o$ and equality and quantifiers.

How does first-order logic differ from higher-order logic?

First-order logic can quantify only over individuals. Higher-order logic can quantify over predicates and functions themselves ("for every property $P$"). It can write the principle of mathematical induction as a single formula in the system, so the expressive power is greater, but completeness and similar properties are weaker than in first-order logic.

Why do proof assistants build on HOL?

On top of the typed lambda calculus, an easily mechanizable syntax, HOL develops much of mathematics from just a few axioms (equality, choice, infinity), and type checking is decidable with simple inference rules, so it is easy to implement as a small trusted kernel. HOL Light and Isabelle/HOL use this HOL as their basis.