Syntax and Semantics

Introduction

This chapter describes the syntax and set-theoretic semantics of the logic supported by the HOL system, which is a variant of Church's simple theory of types (Church 1940) and will henceforth be called the HOL logic, or just HOL. The meta-language for this description will be English, enhanced with various mathematical notations and conventions. The object language of this description is the HOL logic. Note that there is a 'meta-language', in a different sense, associated with the HOL logic, namely the programming language ML. This is the language used to manipulate the HOL logic by users of the system. It is hoped that because of context, no confusion results from these two uses of the word 'meta-language'. When ML is the object of study (as in (Milner, Tofte, and Harper 1990)), ML is the object language under consideration—and English is again the meta-language!

The HOL syntax contains syntactic categories of types and terms whose elements are intended to denote respectively certain sets and elements of sets. This set theoretic interpretation will be developed alongside the description of the HOL syntax, and in the next chapter the HOL proof system will be shown to be sound for reasoning about properties of the set theoretic model.¹ This model is given in terms of a fixed set of sets $\cal U$, which will be called the universe and which is assumed to have the following properties.

Inhab   Each element of $\cal U$ is a non-empty set.

Sub   If $X\in{\cal U}$ and $\emptyset\not=Y\subseteq X$, then $Y\in{\cal U}$.

Prod   If $X\in{\cal U}$ and $Y\in{\cal U}$, then $X\times Y\in{\cal U}$. The set $X\times Y$ is the cartesian product, consisting of ordered pairs $(x,y)$ with $x\in X$ and $y\in Y$, with the usual set-theoretic coding of ordered pairs, viz. $(x,y)=\{\{x\},\{x,y\}\}$.

Pow   If $X\in{\cal U}$, then the powerset $P(X)=\{Y:Y\subseteq X\}$ is also an element of $\cal U$.

Infty   $\cal U$ contains a distinguished infinite set $\inds$.

Choice   There is a distinguished element $\ch\in\prod_{X\in{\cal U}}X$. The elements of the product $\prod_{X\in{\cal U}}X$ are (dependently typed) functions: thus for all $X\in{\cal U}$, $X$ is non-empty by Inhab and $\ch(X)\in X$ witnesses this.

There are some consequences of these assumptions which will be needed. In set theory functions are identified with their graphs, which are certain sets of ordered pairs. Thus the set $X\fun Y$ of all functions from a set $X$ to a set $Y$ is a subset of $P(X\times Y)$; and it is a non-empty set when $Y$ is non-empty. So Sub, Prod and Pow together imply that $\cal U$ also satisfies

Fun   If $X\in{\cal U}$ and $Y\in{\cal U}$, then $X\fun Y\in{\cal U}$.

By iterating Prod, one has that the cartesian product of any finite, non-zero number of sets in $\cal U$ is again in $\cal U$. $\cal U$ also contains the cartesian product of no sets, which is to say that it contains a one-element set (by virtue of Sub applied to any set in ${\cal U}$—Infty guarantees there is one); for definiteness, a particular one-element set will be singled out.

Unit   $\cal U$ contains a distinguished one-element set $1=\{0\}$.

Similarly, because of Sub and Infty, $\cal U$ contains two-element sets, one of which will be singled out.

Bool   $\cal U$ contains a distinguished two-element set $\two=\{0,1\}$.

The above assumptions on $\cal U$ are weaker than those imposed on a universe of sets by the axioms of Zermelo-Fraenkel set theory with the Axiom of Choice (ZFC), principally because $\cal U$ is not required to satisfy any form of the Axiom of Replacement. Indeed, it is possible to prove the existence of a set $\cal U$ with the above properties from the axioms of ZFC. (For example one could take $\cal U$ to consist of all non-empty sets in the von Neumann cumulative hierarchy formed before stage $\omega+\omega$.) Thus, as with many other pieces of mathematics, it is possible in principal to give a completely formal version within ZFC set theory of the semantics of the HOL logic to be given below.

Types

The types of the HOL logic are expressions that denote sets (in the universe $\cal U$). Following tradition, $\sigma$, possibly decorated with subscripts or primes, is used to range over arbitrary types.

There are four kinds of types in the HOL logic. These can be described informally by the following BNF grammar, in which $\alpha$ ranges over type variables, $c$ ranges over atomic types and $\mathit{op}$ ranges over type operators.

$$\sigma \quad ::= \quad \underbrace{\alpha}_{\text{type variables}} \quad\mid\quad \underbrace{c}_{\text{atomic types}} \quad\mid\quad \underbrace{(\sigma_1, \ldots , \sigma_n)\mathit{op}}_{\text{compound types}} \quad\mid\quad \underbrace{\sigma_1\fun\sigma_2}_{\substack{\text{function types}\\(\text{domain }\sigma_1,\ \text{codomain }\sigma_2)}}$$

In more detail, the four kinds of types are as follows.

1. Type variables: these stand for arbitrary sets in the universe. In Church's original formulation of simple type theory, type variables are part of the meta-language and are used to range over object language types. Proofs containing type variables were understood as proof schemes (i.e. families of proofs). To support such proof schemes within the HOL logic, type variables have been added to the object language type system.²

2. Atomic types: these denote fixed sets in the universe. Each theory determines a particular collection of atomic types. For example, the standard atomic types $\ty{bool}$ and $\ty{ind}$ denote, respectively, the distinguished two-element set $\two$ and the distinguished infinite set $\inds$.

3. Compound types: These have the form $(\sigma_1,\ldots,\sigma_n)\ty{op}$, where $\sigma_1$, $\dots$, $\sigma_n$ are the argument types and $\mathit{op}$ is a type operator of arity $n$. Type operators denote operations for constructing sets. The type $(\sigma_1,\ldots,\sigma_n)\ty{op}$ denotes the set resulting from applying the operation denoted by $\mathit{op}$ to the sets denoted by $\sigma_1$, $\dots$, $\sigma_n$. For example, $\ty{list}$ is a type operator with arity 1. It denotes the operation of forming all finite lists of elements from a given set. Another example is the type operator $\ty{prod}$ of arity 2 which denotes the cartesian product operation. The type $(\sigma_1,\sigma_2)\ty{prod}$ is written as $\sigma_1\times\sigma_2$.

4. Function types: If $\sigma_1$ and $\sigma_2$ are types, then $\sigma_1\fun\sigma_2$ is the function type with domain $\sigma_1$ and codomain $\sigma_2$. It denotes the set of all (total) functions from the set denoted by its domain to the set denoted by its codomain. (In the literature $\sigma_1\fun\sigma_2$ is written without the arrow and backwards—i.e. as $\sigma_2\sigma_1$.) Note that syntactically $\fun$ is simply a distinguished type operator of arity 2 written with infix notation. It is singled out in the definition of HOL types because it will always denote the same operation in any model of a HOL theory—in contrast to the other type operators which may be interpreted differently in different models. (See Section 1.2.2.)

It turns out to be convenient to identify atomic types with compound types constructed with $0$-ary type operators. For example, the atomic type $\ty{bool}$ of truth-values can be regarded as being an abbreviation for $()\ty{bool}$. This identification will be made in the technical details that follow, but in the informal presentation atomic types will continue to be distinguished from compound types, and $()c$ will still be written as $c$.

Type structures

The term 'type constant' is used to cover both atomic types and type operators. It is assumed that an infinite set $\mathsf{TyNames}$ of the names of type constants is given. The greek letter $\nu$ is used to range over arbitrary members of $\mathsf{TyNames}$, $c$ will continue to be used to range over the names of atomic types (i.e. $0$-ary type constants), and $\mathit{op}$ is used to range over the names of type operators (i.e. $n$-ary type constants, where $n>0$).

It is assumed that an infinite set $\mathsf{TyVars}$ of type variables is given. Greek letters $\alpha,\beta,\ldots$, possibly with subscripts or primes, are used to range over $\mathsf{TyVars}$. The sets $\mathsf{TyNames}$ and $\mathsf{TyVars}$ are assumed disjoint.

A type structure is a set $\Omega$ of type constants. A type constant is a pair $(\nu,n)$ where $\nu\in\mathsf{TyNames}$ is the name of the constant and $n$ is its arity. Thus $\Omega\subseteq\mathsf{TyNames}\times\mathbb{N}$ (where $\mathbb{N}$ is the set of natural numbers). It is assumed that no two distinct type constants have the same name, i.e. whenever $(\nu, n_1)\in\Omega$ and $(\nu, n_2)\in\Omega$, then $n_1 = n_2$.

The set $\mathsf{Types}_{\Omega}$ of types over a structure ${\Omega}$ can now be defined as the smallest set such that:

• $\mathsf{TyVars}\ \subseteq\ \mathsf{Types}_{\Omega}$.

• If $(\nu,0)\in\Omega$ then $()\nu\in\mathsf{Types}_{\Omega}$.

• If $(\nu,n)\in\Omega$ and $\sigma_i\in\mathsf{Types}_{\Omega}$ for $1\leq i\leq n$, then $(\sigma_1,\ \ldots\ ,\sigma_n)\nu\in\mathsf{Types}_{\Omega}$.

• If $\sigma_1\in\mathsf{Types}_{\Omega}$ and $\sigma_2\in\mathsf{Types}_{\Omega}$ then $\sigma_1\fun\sigma_2\in\mathsf{Types}_{\Omega}$.

The type operator $\fun$ is assumed to associate to the right, so that

$$\sigma_1\fun\sigma_2\fun\ldots\fun \sigma_n\fun\sigma$$

abbreviates

$$\sigma_1\fun(\sigma_2\fun\ldots\fun (\sigma_n\fun\sigma)\ldots)$$

The notation $tyvars(\sigma)$ is used to denote the set of type variables occurring in $\sigma$.

Semantics of types

A model $M$ of a type structure $\Omega$ is specified by giving for each type constant $(\nu,n)$ an $n$-ary function

$$M(\nu):{\cal U}^{n}\longrightarrow{\cal U}$$

Thus given sets $X_1,\ldots,X_n$ in the universe $\cal U$, $M(\nu)(X_1,\ldots,X_n)$ is also a set in the universe. In case $n=0$, this amounts to specifying an element $M(\nu)\in{\cal U}$ for the atomic type $\nu$.

Types containing no type variables are called monomorphic, whereas those that do contain type variables are called polymorphic. What is the meaning of a polymorphic type? One can only say what set a polymorphic type denotes once one has instantiated its type variables to particular sets. So its overall meaning is not a single set, but is rather a set-valued function, ${\cal U}^{n}\longrightarrow{\cal U}$, assigning a set for each particular assignment of sets to the relevant type variables. The arity $n$ corresponds to the number of type variables involved. It is convenient in this connection to be able to consider a type variable to be involved in the semantics of a type $\sigma$ whether or not it actually occurs in $\sigma$, leading to the notion of a type-in-context.

A type context, $\mathit{\alpha{}s}$, is simply a finite (possibly empty) list of distinct type variables $\alpha_{1},\ldots,\alpha_{n}$. A type-in-context is a pair, written $\mathit{\alpha{}s}.\sigma$, where $\mathit{\alpha{}s}$ is a type context, $\sigma$ is a type (over some given type structure) and all the type variables occurring in $\sigma$ appear somewhere in the list $\mathit{\alpha{}s}$. The list $\mathit{\alpha{}s}$ may also contain type variables which do not occur in $\sigma$.

For each $\sigma$ there are minimal contexts $\mathit{\alpha{}s}$ for which $\mathit{\alpha{}s}.\sigma$ is a type-in-context, which only differ by the order in which the type variables of $\sigma$ are listed in $\mathit{\alpha{}s}$. In order to select one such context, let us assume that $\mathsf{TyVars}$ comes with a fixed total order and define the canonical context of the type $\sigma$ to consist of exactly the type variables it contains, listed in order.³

Let $M$ be a model of a type structure $\Omega$. For each type-in-context $\mathit{\alpha{}s}.\sigma$ over $\Omega$, define a function

$$\den{\mathit{\alpha{}s}.\sigma}_{M}:{\cal U}^{n}\longrightarrow{\cal U}$$

(where $n$ is the length of the context) by induction on the structure of $\sigma$ as follows.

• If $\sigma$ is a type variable, it must be $\alpha_{i}$ for some unique $i=1,\ldots,n$ and then $\den{\mathit{\alpha{}s}.\sigma}_{M}$ is the $i$th projection function, which sends $(X_{1},\ldots,X_{n})\in{\cal U}^{n}$ to $X_{i}\in{\cal U}$.

• If $\sigma$ is a function type $\sigma_{1}\fun\sigma_{2}$, then $\den{\mathit{\alpha{}s}.\sigma}_M$ sends $\mathit{xs}\in{\cal U}^n$ to the set of all functions from $\den{\mathit{\alpha{}s}.\sigma_1}_M(\mathit{xs})$ to $\den{\mathit{\alpha{}s}.\sigma_2}_M(\mathit{xs})$. (This makes use of the property Fun of $\cal U$.)

• If $\sigma$ is a compound type $(\sigma_{1},\ldots,\sigma_{m})\nu$, then $\den{\mathit{\alpha{}s}.\sigma}_{M}$ sends $\mathit{xs}$ to $M(\nu)(S_{1},\ldots,S_{m})$ where each $S_{j}$ is $\den{\mathit{\alpha{}s}.\sigma_{j}}_{M}(\mathit{xs})$.

One can now define the meaning of a type $\sigma$ in a model $M$ to be the function

$$\den{\sigma}_{M}:{\cal U}^{n}\longrightarrow{\cal U}$$

given by $\den{\mathit{\alpha{}s}.\sigma}_{M}$, where $\mathit{\alpha{}s}$ is the canonical context of $\sigma$. If $\sigma$ is monomorphic, then $n=0$ and $\den{\sigma}_{M}$ can be identified with the element $\den{\sigma}_{M}()$ of $\cal U$. When the particular model $M$ is clear from the context, $\den{\_}_{M}$ will be written $\den{\_}$.

To summarize, given a model in $\cal U$ of a type structure $\Omega$, the semantics interprets monomorphic types over $\Omega$ as sets in $\cal U$ and more generally, interprets polymorphic types involving $n$ type variables as $n$-ary functions ${\cal U}^{n}\longrightarrow{\cal U}$ on the universe. Function types are interpreted by full function sets.

Examples   Suppose that $\Omega$ contains a type constant $(\textsl{b},0)$ and that the model $M$ assigns the set $\two$ to $\textsl{b}$. Then:

1. $\den{\textsl{b}\fun\textsl{b}\fun\textsl{b}}=\two\fun\two\fun\two\in{\cal U}$.

2. $\den{(\alpha\fun\textsl{b})\fun\alpha}:{\cal U}\longrightarrow{\cal U}$ is the function sending $X\in{\cal U}$ to $(X\fun\two)\fun X\in{\cal U}$.

3. $\den{\alpha,\beta . (\alpha\fun\textsl{b})\fun\alpha}:{\cal U}^{2}\longrightarrow{\cal U}$ is the function sending $(X,Y)\in{\cal U}^{2}$ to $(X\fun\two)\fun X\in{\cal U}$.

Remark   A more traditional approach to the semantics would involve giving meanings to types in the presence of 'environments' assigning sets in $\cal U$ to all type variables. The use of types-in-contexts is almost the same as using partial environments with finite domains—it is just that the context ties down the admissible domain to a particular finite (ordered) set of type variables. At the level of types there is not much to choose between the two approaches. However for the syntax and semantics of terms to be given below, where there is a dependency both on type variables and on individual variables, the approach used here seems best.

Instances and substitution

If $\sigma$ and $\tau_1,\ldots,\tau_n$ are types over a type structure $\Omega$,

$$\sigma[\tau_{1},\ldots,\tau_{p}/\beta_{1},\ldots,\beta_{p}]$$

will denote the type resulting from the simultaneous substitution for each $i=1,\ldots,p$ of $\tau_i$ for the type variable $\beta_i$ in $\sigma$. The resulting type is called an instance of $\sigma$. The following lemma about instances will be useful later; it is proved by induction on the structure of $\sigma$.

Lemma 1   Suppose that $\sigma$ is a type containing distinct type variables $\beta_1,\ldots,\beta_p$ and that $\sigma'=\sigma[\tau_{1},\ldots,\tau_{n}/\beta_1,\ldots,\beta_p]$ is an instance of $\sigma$. Then the types $\tau_1,\ldots,\tau_p$ are uniquely determined by $\sigma$ and $\sigma'$.

We also need to know how the semantics of types behaves with respect to substitution:

Lemma 2   Given types-in-context $\mathit{\beta{}s}.\sigma$ and $\mathit{\alpha{}s}.\tau_i$ ($i=1,\ldots,p$, where $p$ is the length of $\mathit{\beta{}s}$), let $\sigma'$ be the instance $\sigma[\mathit{\tau{}s}/\mathit{\beta{}s}]$. Then $\mathit{\alpha{}s}.\sigma'$ is also a type-in-context and its meaning in any model $M$ is related to that of $\mathit{\beta{}s}.\sigma$ as follows. For all $\mathit{xs}\in{\cal U}^n$ (where $n$ is the length of $\mathit{\alpha{}s}$)

$$\den{\mathit{\alpha{}s}.\sigma'}(\mathit{xs}) = \den{\mathit{\beta{}s}.\sigma}(\den{\mathit{\alpha{}s}.\tau_{1}}(\mathit{xs}), \ldots ,\den{\mathit{\alpha{}s}.\tau_{p}}(\mathit{xs}))$$

Once again, the lemma can be proved by induction on the structure of $\sigma$.

Terms

The terms of the HOL logic are expressions that denote elements of the sets denoted by types. The meta-variable $t$ is used to range over arbitrary terms, possibly decorated with subscripts or primes.

There are four kinds of terms in the HOL logic. These can be described approximately by the following BNF grammar, in which $x$ ranges over variables and $c$ ranges over constants.

$$t \quad ::= \quad \underbrace{x}_{\text{variables}} \quad\mid\quad \underbrace{\con{c}}_{\text{constants}} \quad\mid\quad \underbrace{t\ t'}_{\substack{\text{function applications}\\(\text{function }t,\ \text{argument }t')}} \quad\mid\quad \underbrace{\lambda x .\ t}_{\lambda\text{-abstractions}}$$

Informally, a $\lambda$-term $\lambda x.\ t$ denotes a function $v\mapsto t[v/x]$, where $t[v/x]$ denotes the result of substituting $v$ for $x$ in $t$. An application $t\ t'$ denotes the result of applying the function denoted by $t$ to the value denoted by $t'$. This will be made more precise below.

The BNF grammar just given omits mention of types. In fact, each term in the HOL logic is associated with a unique type. The notation $t_{\sigma}$ is traditionally used to range over terms of type $\sigma$. A more accurate grammar of terms is:

$$t_{\sigma} \quad ::= \quad x_{\sigma} \quad\mid\quad \con{c}_{\sigma} \quad\mid\quad (t_{\sigma'\fun\sigma}\ t'_{\sigma'})_{\sigma} \quad\mid\quad (\lambda x_{\sigma_1} .\ t_{\sigma_2})_{\sigma_1\fun\sigma_2}$$

In fact, just as the definition of types was relative to a particular type structure $\Omega$, the formal definition of terms is relative to a given collection of typed constants over $\Omega$. Assume that an infinite set $\mathsf{Names}$ of names is given. A constant over $\Omega$ is a pair $(\con{c}, \sigma)$, where $\con{c}\in\mathsf{Names}$ and $\sigma\in\mathsf{Types}_{\Omega}$. A signature over $\Omega$ is just a set $\Sigma_\Omega$ of such constants.

The set $\mathsf{Terms}_{\Sigma_{\Omega}}$ of terms over $\Sigma_{\Omega}$ is defined to be the smallest set closed under the following rules of formation:

1. Constants: If $(\con{c},\sigma)\in{\Sigma_{\Omega}}$ and $\sigma'\in\mathsf{Types}_{\Omega}$ is an instance of $\sigma$, then $(\con{c},{\sigma'})\in\mathsf{Terms}_{\Sigma_{\Omega}}$. Terms formed in this way are called constants and are written $\con{c}_{\sigma'}$.

2. Variables: If $x\in\mathsf{Names}$ and $\sigma\in\mathsf{Types}_{\Omega}$, then $\mathtt{var}\ x_{\sigma}\in\mathsf{Terms}_{\Sigma_{\Omega}}$. Terms formed in this way are called variables. The marker $\mathtt{var}$ is purely a device to distinguish variables from constants with the same name. A variable $\mathtt{var}\ x_{\sigma}$ will usually be written as $x_{\sigma}$, if it is clear from the context that $x$ is a variable rather than a constant.

3. Function applications: If $t_{\sigma'{\fun}\sigma}\in\mathsf{Terms}_{\Sigma_{\Omega}}$ and $t'_{\sigma'}\in\mathsf{Terms}_{\Sigma_{\Omega}}$, then $(t_{\sigma'\fun\sigma}\ t'_{\sigma'})_{\sigma}\in \mathsf{Terms}_{\Sigma_{\Omega}}$. (Terms formed in this way are sometimes called combinations.)

4. $\lambda$-Abstractions: If $\mathtt{var}\ x_{\sigma_1}\in\mathsf{Terms}_{\Sigma_{\Omega}}$ and $t_{\sigma_2}\in\mathsf{Terms}_{\Sigma_{\Omega}}$, then $(\lambda x_{\sigma_1}.\ t_{\sigma_2})_{\sigma_1\fun\sigma_2} \in\mathsf{Terms}_{\Sigma_{\Omega}}$.

Note that it is possible for constants and variables to have the same name. It is also possible for different variables to have the same name, if they have different types.

The type subscript on a term may be omitted if it is clear from the structure of the term or the context in which it occurs what its type must be.

Function application is assumed to associate to the left, so that $t\ t_1\ t_2\ \ldots\ t_n$ abbreviates $(\ \ldots\ ((t\ t_1)\ t_2)\ \ldots\ t_n)$.

The notation $\lambda x_1\ x_2\ \cdots\ x_n.\ t$ abbreviates $\lambda x_1.\ (\lambda x_2.\ \cdots\ (\lambda x_n.\ t)\ \cdots\ )$.

A term is called polymorphic if it contains a type variable. Otherwise it is called monomorphic. Note that a term $t_{\sigma}$ may be polymorphic even though $\sigma$ is monomorphic—for example, $(f_{\alpha\fun\textsl{b}}\ x_{\alpha})_{\textsl{b}}$, where $\textsl{b}$ is an atomic type. The expression $tyvars(t_{\sigma})$ denotes the set of type variables occurring in $t_{\sigma}$.

An occurrence of a variable $x_{\sigma}$ is called bound if it occurs within the scope of a textually enclosing $\lambda x_{\sigma}$, otherwise the occurrence is called free. Note that $\lambda x_{\sigma}$ does not bind $x_{\sigma'}$ if $\sigma\neq \sigma'$. A term in which all occurrences of variables are bound is called closed.

Terms-in-context

A context $\mathit{\alpha{}s},\!\mathit{xs}$ consists of a type context $\mathit{\alpha{}s}$ together with a list $\mathit{xs}=x_{1},\ldots,x_{m}$ of distinct variables whose types only contain type variables from the list $\mathit{\alpha{}s}$.

The condition that $\mathit{xs}$ contains distinct variables needs some comment. Since a variable is specified by both a name and a type, it is permitted for $\mathit{xs}$ to contain repeated names, so long as different types are attached to the names. This aspect of the syntax means that one has to proceed with caution when defining the meaning of type variable instantiation, since instantiation may cause variables to become equal ‘accidentally’: see Section 1.3.3.

A term-in-context $\mathit{\alpha{}s},\!\mathit{xs}.t$ consists of a context together with a term $t$ satisfying the following conditions.

• $\mathit{\alpha{}s}$ contains any type variable that occurs in $\mathit{xs}$ and $t$.

• $\mathit{xs}$ contains any variable that occurs freely in $t$.

• $\mathit{xs}$ does not contain any variable that occurs bound in $t$.

The context $\mathit{\alpha{}s},\!\mathit{xs}$ may contain (type) variables which do not appear in $t$. Note that the combination of the second and third conditions implies that a variable cannot have both free and bound occurrences in $t$. For an arbitrary term, there is always an $\alpha$-equivalent term which satisfies this condition, obtained by renaming the bound variables as necessary.⁴ In the semantics of terms to be given below we will restrict attention to such terms. Then the meaning of an arbitrary term is taken to be the meaning of some $\alpha$-variant of it having no variable both free and bound. (The semantics will equate $\alpha$-variants, so it does not matter which is chosen.) Evidently for such a term there is a minimal context $\mathit{\alpha{}s},\!\mathit{xs}$, unique up to the order in which variables are listed, for which $\mathit{\alpha{}s},\!\mathit{xs}.t$ is a term-in-context. As for type variables, we will assume given a fixed total order on variables. Then the unique minimal context with variables listed in order will be called the canonical context of the term $t$.

Semantics of terms

Let $\Sigma_{\Omega}$ be a signature over a type structure $\Omega$ (see Section 1.3). A model $M$ of $\Sigma_{\Omega}$ is specified by a model of the type structure plus for each constant $(\con{c},\sigma)\in\Sigma_{\Omega}$ an element

$$M(\con{c},\sigma) \in \prod_{\mathit{xs}\in{\cal U}^{n}}\den{\sigma}_{M}(\mathit{xs})$$

of the indicated cartesian product, where $n$ is the number of type variables occurring in $\sigma$. In other words $M(\con{c},\sigma)$ is a (dependently typed) function assigning to each $\mathit{xs}\in{\cal U}^{n}$ an element of $\den{\sigma}_{M}(\mathit{xs})$. In the case that $n=0$ (so that $\sigma$ is monomorphic), $\den{\sigma}_{M}$ was identified with a set in $\cal U$ and then $M(c,\sigma)$ can be identified with an element of that set.

The meaning of HOL terms in such a model will now be described. The semantics interprets closed terms involving no type variables as elements of sets in $\cal U$ (the particular set involved being derived from the type of the term as in Section 1.2.2). More generally, if the closed term involves $n$ type variables then it is interpreted as an element of a product $\prod_{\mathit{xs}\in{\cal U}^{n}}Y(\mathit{xs})$, where the function $Y:{\cal U}^{n}\longrightarrow{\cal U}$ is derived from the type of the term (in a type context derived from the term). Thus the meaning of the term is a (dependently typed) function which, when applied to any meanings chosen for the type variables in the term, yields a meaning for the term as an element of a set in $\cal U$. On the other hand, if the term involves $m$ free variables but no type variables, then it is interpreted as a function $Y_1\times\cdots\times Y_m\fun Y$ where the sets $Y_1,\ldots,Y_m$ in $\cal U$ are the interpretations of the types of the free variables in the term and the set $Y\in{\cal U}$ is the interpretation of the type of the term; thus the meaning of the term is a function which, when applied to any meanings chosen for the free variables in the term, yields a meaning for the term. Finally, the most general case is of a term involving $n$ type variables and $m$ free variables: it is interpreted as an element of a product

$$\prod_{\mathit{xs}\in{\cal U}^{n}}Y_{1}(\mathit{xs})\times\cdots\times Y_{m}(\mathit{xs}) \;\fun\; Y(\mathit{xs})$$

where the functions $Y_{1},\ldots,Y_{m},Y:{\cal U}^{n}\longrightarrow{\cal U}$ are determined by the types of the free variables and the type of the term (in a type context derived from the term).

More precisely, given a term-in-context $\mathit{\alpha{}s},\!\mathit{xs}.t$ over $\Sigma_{\Omega}$ suppose

• $t$ has type $\tau$

• $\mathit{xs}=x_{1},\ldots,x_{m}$ and each $x_{j}$ has type $\sigma_{j}$

• $\mathit{\alpha{}s}=\alpha_{1},\ldots,\alpha_{n}$.

Then since $\mathit{\alpha{}s},\!\mathit{xs}.t$ is a term-in-context, $\mathit{\alpha{}s}.\tau$ and $\mathit{\alpha{}s}.\sigma_{j}$ are types-in-context, and hence give rise to functions $\den{\mathit{\alpha{}s}.\tau}_{M}$ and $\den{\mathit{\alpha{}s}.\sigma_{j}}_{M}$ from ${\cal U}^{n}$ to $\cal U$ as in Section 1.2.2. The meaning of $\mathit{\alpha{}s},\!\mathit{xs}.t$ in the model $M$ will be given by an element

$$\den{\mathit{\alpha{}s},\!\mathit{xs}.t}_{M} \in \prod_{\mathit{xs}\in{\cal U}^{n}} \left(\prod_{j=1}^{m}\den{\mathit{\alpha{}s}.\sigma_{j}}_{M}(\mathit{xs})\right) \fun \den{\mathit{\alpha{}s}.\tau}_{M}(\mathit{xs}) .$$

In other words, given

$$\begin{array}{rcl} \mathit{xs} & = & (X_{1},\ldots,X_{n})\in{\cal U}^{n} \\ \mathit{ys} & = & (y_{1},\ldots,y_{m})\in\den{\mathit{\alpha{}s}.\sigma_{1}}_{M}(\mathit{xs}) \times\cdots\times \den{\mathit{\alpha{}s}.\sigma_{m}}_{M}(\mathit{xs}) \end{array}$$

one gets an element $\den{\mathit{\alpha{}s},\!\mathit{xs}.t}_{M}(\mathit{xs})(\mathit{ys})$ of $\den{\mathit{\alpha{}s}.\tau}_{M}(\mathit{xs})$. The definition of $\den{\mathit{\alpha{}s},\!\mathit{xs}.t}_{M}$ proceeds by induction on the structure of the term $t$, as follows. (As before, the subscript $M$ will be dropped from the semantic brackets $\den{\_}$ when the particular model involved is clear from the context.)

• If $t$ is a variable, it must be $x_{j}$ for some unique $j=1,\ldots,m$, so $\tau=\sigma_{j}$ and then $\den{\mathit{\alpha{}s},\!\mathit{xs}.t}(\mathit{xs})(\mathit{ys})$ is defined to be $y_{j}$.

• Suppose $t$ is a constant $\con{c}_{\sigma'}$, where $(\con{c},\sigma)\in\Sigma_{\Omega}$ and $\sigma'$ is an instance of $\sigma$. Then by Lemma 1 of 1.2.3, $\sigma'=\sigma[\tau_{1},\ldots,\tau_{p}/\beta_{1},\ldots,\beta_{p}]$ for uniquely determined types $\tau_{1},\ldots,\tau_{p}$ (where $\beta_{1},\ldots,\beta_{p}$ are the type variables occurring in $\sigma$). Then define $\den{\mathit{\alpha{}s},\!\mathit{xs}.t}(\mathit{xs})(\mathit{ys})$ to be $M(\con{c},\sigma)(\den{\mathit{\alpha{}s}.\tau_{1}}(\mathit{xs}), \ldots,\den{\mathit{\alpha{}s}.\tau_{p}}(\mathit{xs}))$, which is an element of $\den{\mathit{\alpha{}s}.\tau}(\mathit{xs})$ by Lemma 2 of 1.2.3 (since $\tau$ is $\sigma'$).

• Suppose $t$ is a function application term $(t_{1}\ t_{2})$ where $t_{1}$ is of type $\tau'\fun\tau$ and $t_{2}$ is of type $\tau'$. Then $f=\den{\mathit{\alpha{}s},\!\mathit{xs}.t_{1}}(\mathit{xs})(\mathit{ys})$, being an element of $\den{\mathit{\alpha{}s}.\tau'\fun\tau}(\mathit{xs})$, is a function from the set $\den{\mathit{\alpha{}s}.\tau'}(\mathit{xs})$ to the set $\den{\mathit{\alpha{}s}.\tau}(\mathit{xs})$ which one can apply to the element $y=\den{\mathit{\alpha{}s},\!\mathit{xs}.t_{2}}(\mathit{xs})(\mathit{ys})$. Define $\den{\mathit{\alpha{}s},\!\mathit{xs}.t}(\mathit{xs})(\mathit{ys})$ to be $f(y)$.

• Suppose $t$ is the abstraction term $\lambda x.t_{2}$ where $x$ is of type $\tau_{1}$ and $t_{2}$ of type $\tau_{2}$. Thus $\tau=\tau_{1}\fun\tau_{2}$ and $\den{\mathit{\alpha{}s}.\tau}(\mathit{xs})$ is the function set $\den{\mathit{\alpha{}s}.\tau_{1}}(\mathit{xs})\fun\den{\mathit{\alpha{}s}.\tau_{2}}(\mathit{xs})$. Define $\den{\mathit{\alpha{}s},\!\mathit{xs}.t}(\mathit{xs})(\mathit{ys})$ to be the element of this set which is the function sending $y\in\den{\mathit{\alpha{}s}.\tau_{1}}(\mathit{xs})$ to $\den{\mathit{\alpha{}s},\!\mathit{xs},\!x.t_{2}}(\mathit{xs})(\mathit{ys},y)$. (Note that since $\mathit{\alpha{}s},\!\mathit{xs}.t$ is a term-in-context, by convention the bound variable $x$ does not occur in $\mathit{xs}$ and thus $\mathit{\alpha{}s},\!\mathit{xs},\!x.t_{2}$ is also a term-in-context.)

Now define the meaning of a term $t_{\tau}$ in a model $M$ to be the dependently typed function

$$\den{t_{\tau}} \in \prod_{\mathit{xs}\in{\cal U}^{n}} \left(\prod_{j=1}^{m}\den{\mathit{\alpha{}s}.\sigma_{j}}(\mathit{xs})\right) \fun \den{\mathit{\alpha{}s}.\tau}(\mathit{xs})$$

given by $\den{\mathit{\alpha{}s},\!\mathit{xs}.t_{\tau}}$, where $\mathit{\alpha{}s},\!\mathit{xs}$ is the canonical context of $t_{\tau}$. So $n$ is the number of type variables in $t_{\tau}$, $\mathit{\alpha{}s}$ is a list of those type variables, $m$ is the number of ordinary variables occurring freely in $t_{\tau}$ (assumed to be distinct from the bound variables of $t_{\tau}$) and the $\sigma_{j}$ are the types of those variables. (It is important to note that the list $\mathit{\alpha{}s}$, which is part of the canonical context of $t$, may be strictly bigger than the canonical type contexts of $\sigma_{j}$ or $\tau$. So it would not make sense to write just $\den{\sigma_{j}}$ or $\den{\tau}$ in the above definition.)

If $t_{\tau}$ is a closed term, then $m=0$ and for each $\mathit{xs}\in{\cal U}^{n}$ one can identify $\den{t_{\tau}}$ with the element $\den{t_{\tau}}(\mathit{xs})()\in\den{\mathit{\alpha{}s}.\tau}(\mathit{xs})$. So for closed terms one gets

$$\den{t_{\tau}} \in \prod_{\mathit{xs}\in{\cal U}^{n}} \den{\mathit{\alpha{}s}.\tau}(\mathit{xs})$$

where $\mathit{\alpha{}s}$ is the list of type variables occurring in $t_{\tau}$ and $n$ is the length of that list. If moreover, no type variables occur in $t_{\tau}$, then $n=0$ and $\den{t_{\tau}}$ can be identified with the element $\den{t_{\tau}}()$ of the set $\den{\tau}\in{\cal U}$.

The semantics of terms appears somewhat complicated because of the possible dependency of a term upon both type variables and ordinary variables. Examples of how the definition of the semantics works in practice can be found in Section 2.4.2, where the meaning of several terms denoting logical constants is given.

Substitution

Since terms may involve both type variables and ordinary variables, there are two different operations of substitution on terms which have to be considered---substitution of types for type variables and substitution of terms for variables.

Substituting types for type variables in terms

Suppose $t$ is a term, with canonical context $\mathit{\alpha{}s},\!\mathit{xs}$ say, where $\mathit{\alpha{}s} = \alpha_1,\ldots,\alpha_n$, $\mathit{xs} = x_1,\ldots,x_m$ and where for $j=1,\ldots,m$ the type of the variable $x_j$ is $\sigma_j$. If $\mathit{\alpha{}s}'.\tau_{i}$ ($i=1,\ldots,n$) are types-in-context, then substituting the types $\tau_{i}$ for the type variables $\alpha_{i}$ in the list $\mathit{xs}$, one obtains a new list of variables $\mathit{xs}'$. Thus the $j$th entry of $\mathit{xs}'$ has type $\sigma'_{j} = \sigma_{j}[\mathit{\tau{}s}/\mathit{\alpha{}s}]$. Only substitutions with the following property will be considered.

In instantiating the type variables $\mathit{\alpha{}s}$ with the types $\mathit{\tau{}s}$, no two distinct variables in the list $\mathit{xs}$ become equal in the list $\mathit{xs}'$.⁵

This condition ensures that $\mathit{\alpha{}s}',\mathit{xs}'$ really is a context. Then one obtains a new term-in-context $\mathit{\alpha{}s}',\!\mathit{xs}'.t'$ by substituting the types $\mathit{\tau{}s}=\tau_{1},\ldots,\tau_{n}$ for the type variables $\mathit{\alpha{}s}$ in $t$ (with suitable renaming of bound occurrences of variables to make them distinct from the variables in $\mathit{xs}'$). The notation

$$t[\mathit{\tau{}s}/\mathit{\alpha{}s}]$$

is used for the term $t'$.

Lemma 3   The meaning of $\mathit{\alpha{}s}',\!\mathit{xs}'.t'$ in a model is related to that of $t$ as follows. For all $\mathit{xs}'\in{\cal U}^{n'}$ (where $n'$ is the length of $\mathit{\alpha{}s}'$)

$$\den{\mathit{\alpha{}s}',\!\mathit{xs}'.t'}(\mathit{xs}') = \den{t}(\den{\mathit{\alpha{}s}'.\tau_{1}}(\mathit{xs}'),\ldots, \den{\mathit{\alpha{}s}'.\tau_{n}}(\mathit{xs}')).$$

Lemma 2 in 1.2.3 is needed to see that both sides of the above equation are elements of the same set of functions. The validity of the equation is proved by induction on the structure of the term $t$.

Substituting terms for variables in terms

Suppose $t$ is a term, with canonical context $\mathit{\alpha{}s},\!\mathit{xs}$ say, where $\mathit{\alpha{}s} = \alpha_1,\ldots,\alpha_n$, $\mathit{xs} = x_1,\ldots,x_m$ and where for $j=1,\ldots,m$ the type of the variable $x_j$ is $\sigma_j$. If one has terms-in-context $\mathit{\alpha{}s},\!\mathit{xs}'.t_{j}$ for $j=1,\ldots,m$ with $t_{j}$ of the same type as $x_{j}$, say $\sigma_{j}$, then one obtains a new term-in-context $\mathit{\alpha{}s},\!\mathit{xs}'.t''$ by substituting the terms $\mathit{ts}=t_1,\ldots,t_m$ for the variables $\mathit{xs}$ in $t$ (with suitable renaming of bound occurrences of variables to prevent the free variables of the $t_{j}$ becoming bound after substitution). The notation

$$t[\mathit{ts}/\mathit{xs}]$$

is used for the term $t''$.

Lemma 4   The meaning of $\mathit{\alpha{}s},\!\mathit{xs}'.t''$ in a model is related to that of $t$ as follows. For all $\mathit{xs}\in{\cal U}^{n}$ and all $\mathit{ys}'\in\den{\mathit{\alpha{}s}.\sigma'_{1}} \times\cdots\times \den{\mathit{\alpha{}s}.\sigma'_{m'}}$ (where $\sigma'_{j}$ is the type of $x'_{j}$)

$$\den{\mathit{\alpha{}s},\!\mathit{xs}'.t''}(\mathit{xs})(\mathit{ys}') = \den{t}(\mathit{xs})( \den{\mathit{\alpha{}s},\!\mathit{xs}'.t_{1}}(\mathit{xs})(\mathit{ys}'),\ldots, \den{\mathit{\alpha{}s},\!\mathit{xs}'.t_{m}}(\mathit{xs})(\mathit{ys}'))$$

Once again, this result is proved by induction on the structure of the term $t$.

Standard notions

Up to now the syntax of types and terms has been very general. To represent the standard formulas of logic it is necessary to impose some specific structure. In particular, every type structure must contain an atomic type $\ty{bool}$ which is intended to denote the distinguished two-element set $\two\in{\cal U}$, regarded as a set of truth-values. Logical formulas are then identified with terms of type $\ty{bool}$. In addition, various logical constants are assumed to be in all signatures. These requirements are formalized by defining the notion of a standard signature.

Standard type structures

A type structure $\Omega$ is standard if it contains the atomic types $\ty{bool}$ (of booleans or truth-values) and $\ty{ind}$ (of individuals). (In the literature, the symbol $o$ is often used instead of $\ty{bool}$ and $\iota$ instead of $\ty{ind}$.)

A model $M$ of $\Omega$ is standard if $M(\ty{bool})$ and $M(\ty{ind})$ are respectively the distinguished sets $\two$ and $\inds$ in the universe $\cal U$.

It will be assumed from now on that type structures and their models are standard.

Standard signatures

A signature $\Sigma_{\Omega}$ is standard if it contains the following three primitive constants:

$${\imp}_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}$$

$${=}_{\alpha\fun\alpha\fun\ty{bool}}$$

$$\hilbert_{(\alpha\fun\ty{bool})\fun\alpha}$$

The intended interpretation of these constants is that $\imp$ denotes implication, $=_{\sigma\fun\sigma\fun\ty{bool}}$ denotes equality on the set denoted by $\sigma$, and $\hilbert_{(\sigma\fun\ty{bool})\fun\sigma}$ denotes a choice function on the set denoted by $\sigma$. More precisely, a model $M$ of $\Sigma_{\Omega}$ will be called standard if

• $M({\imp},\ty{bool}\fun\ty{bool}\fun\ty{bool})\in(\two\fun\two\fun\two)$ is the standard implication function, sending $b,b'\in\two$ to

  $$(b\imp b') = \left\{ \begin{array}{ll} 0 & \text{if } b=1 \text{ and } b'=0 \\ 1 & \text{otherwise} \end{array} \right.$$

• $M({=},\alpha\fun\alpha\fun\ty{bool})\in\prod_{X\in{\cal U}}.X\fun X\fun\two$ is the function assigning to each $X\in{\cal U}$ the equality test function, sending $x,x'\in X$ to

  $$(x=_{X}x') = \left\{ \begin{array}{ll} 1 & \text{if } x=x' \\ 0 & \text{otherwise} \end{array} \right.$$

• $M(\hilbert,(\alpha\fun\ty{bool})\fun\alpha)\in\prod_{X\in{\cal U}}.(X\fun\two)\fun X$ is the function assigning to each $X\in{\cal U}$ the choice function sending $f\in(X\fun\two)$ to

  $$\ch_{X}(f) = \left\{ \begin{array}{ll} \ch(f^{-1}\{1\}) & \text{if } f^{-1}\{1\}\not=\emptyset\\ \ch(X) & \text{otherwise} \end{array} \right.$$

  where $f^{-1}\{1\}=\{x\in X : f(x)=1\}$. (Note that $f^{-1}\{1\}$ is in $\cal U$ when it is non-empty, by the property Sub of the universe $\cal U$ given in Section 1.1. The function $\ch$ is given by property Choice.)

It will be assumed from now on that signatures and their models are standard.

Remark   This particular choice of primitive constants is arbitrary. The standard collection of logical constants includes $\con{T}$ ('true'), $\con{F}$ ('false'), $\imp$ ('implies'), $\wedge$ ('and'), $\vee$ ('or'), $\neg$ ('not'), $\forall$ ('for all'), $\exists$ ('there exists'), $=$ ('equals'), $\iota$ ('the'), and $\hilbert$ ('a'). This set is redundant, since it can be defined (in a sense explained in Section 2.5.1) from various subsets. In practice, it is necessary to work with the full set of logical constants, and the particular subset taken as primitive is not important. The interested reader can explore this topic further by reading Andrews' book (Andrews 1986) and the references it contains.

Terms of type $\ty{bool}$ are called formulas.

The following notational abbreviations are used:

These notations are special cases of general abbreviatory conventions supported by the HOL system. The first two are infixes and the third is a binder (see DESCRIPTION's sections on parsing and pretty-printing).

1. There are other, ‘non-standard’ models of HOL, which will not concern us here. ↩

2. This technique was invented by Robin Milner for the object logic PPλ of his LCF system. ↩

3. It is possible to work with unordered contexts, specified by finite sets rather than lists, but we choose not to do that since it mildly complicates the definition of the semantics to be given below. ↩

4. Recall that two terms are said to be $\alpha$-equivalent if they differ only in the names of their bound variables. ↩

5. Such an identification of variables could occur if the variables had the same name component and their types became equal on instantiation. ↩