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. ↩

Theories

Introduction

The result, if any, of a session with the HOL system is an object called a theory. This object is closely related to what a logician would call a theory, but there are some differences arising from the needs of mechanical proof. A HOL theory, like a logician’s theory, contains sets of types, constants, definitions and axioms. In addition, however, a HOL theory, at any point in time, contains an explicit list of theorems that have already been proved from the axioms and definitions. Logicians have no need to distinguish theorems actually proved from those merely provable; hence they do not normally consider sets of proven theorems as part of a theory; rather, they take the theorems of a theory to be the (often infinite) set of all consequences of the axioms and definitions. A related difference between logicians’ theories and HOL theories is that for logicians, theories are static objects, but in HOL they can be thought of as potentially extendable. For example, the HOL system provides tools for adding to theories and combining theories. A typical interaction with HOL consists in combining some existing theories, making some definitions, proving some theorems and then saving the new results.

The purpose of the HOL system is to provide tools to enable well-formed theories to be constructed. The HOL logic is typed: each theory specifies a signature of type and individual constants; these then determine the sets of types and terms as in the previous chapter. All the theorems of such theories are logical consequences of the definitions and axioms of the theory. The HOL system ensures that only well-formed theories can be constructed by allowing theorems to be created only by formal proof. Explicating this involves defining what it means to be a theorem, which leads to the description of the proof system of HOL, to be given below. It is shown to be sound for the set theoretic semantics of HOL described in the previous chapter. This means that a theorem is satisfied by a model if it has a formal proof from axioms which are themselves satisfied by the model. Since a logical contradiction is not satisfied by any model, this guarantees in particular that a theory possessing a model is necessarily consistent, i.e. a logical contradiction cannot be formally proved from its axioms.

This chapter also describes the various mechanisms by which HOL theories can be extended to new theories. Each mechanism is shown to preserve the property of possessing a model. Thus theories built up from the initial HOL theory (which does possess a model) using these mechanisms are guaranteed to be consistent.

Sequents

The HOL logic is phrased in terms of hypothetical assertions called sequents. Fixing a (standard) signature $\Sigma_\Omega$, a sequent is a pair $(\Gamma, t)$ where $\Gamma$ is a finite set of formulas over $\Sigma_\Omega$ and $t$ is a single formula over $\Sigma_\Omega$.¹ The set of formulas $\Gamma$ forming the first component of a sequent is called its set of assumptions and the term $t$ forming the second component is called its conclusion. When it is not ambiguous to do so, a sequent $(\{\},t)$ is written as just $t$.

Intuitively, a model $M$ of $\Sigma_\Omega$ satisfies a sequent $(\Gamma, t)$ if any interpretation of relevant free variables as elements of $M$ making the formulas in $\Gamma$ true, also makes the formula $t$ true. To make this more precise, suppose $\Gamma=\{t_1,\ldots,t_p\}$ and let $\mathit{\alpha{}s},\!\mathit{xs}$ be a context containing all the type variables and all the free variables occurring in the formulas $t,t_{1},\ldots,t_{p}$. Suppose that $\mathit{\alpha{}s}$ has length $n$, that $\mathit{xs}=x_{1},\ldots,x_{m}$ and that the type of $x_{j}$ is $\sigma_{j}$. Since formulas are terms of type $\ty{bool}$, the semantics of terms defined in the previous chapter gives rise to elements $\den{\mathit{\alpha{}s},\!\mathit{xs}.t}_M$ and $\den{\mathit{\alpha{}s},\!\mathit{xs}.t_{k}}_M$ ($k=1,\ldots,p$) in

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

Say that the model $M$ satisfies the sequent $(\Gamma,t)$ and write

$$\Gamma \models_{M} t$$

if for all $\mathit{xs}\in{\cal U}^{n}$ and all $\mathit{ys}\in\den{\mathit{\alpha{}s}.\sigma_{1}}_M(\mathit{xs})\times\cdots\times \den{\mathit{\alpha{}s}.\sigma_{m}}_M(\mathit{xs})$ with

$$\den{\mathit{\alpha{}s},\!\mathit{xs}.t_{k}}_M(\mathit{xs})(\mathit{ys})=1$$

for all $k=1,\ldots,p$, it is also the case that

$$\den{\mathit{\alpha{}s},\!\mathit{xs}.t}_M(\mathit{xs})(\mathit{ys})=1.$$

(Recall that $\two$ is the set $\{0,1\}$.)

In the case $p=0$, the satisfaction of $(\{\},t)$ by $M$ will be written $\models_{M} t$. Thus $\models_{M} t$ means that the dependently typed function

$$\den{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 \:\two$$

is constant with value $1\in\two$.

Logic

A deductive system ${\cal D}$ is a set of pairs $(L,(\Gamma,t))$ where $L$ is a (possibly empty) list of sequents and $(\Gamma,t)$ is a sequent.

A sequent $(\Gamma,t)$ follows from a set of sequents $\Delta$ by a deductive system ${\cal D}$ if and only if there exist sequents $(\Gamma_1,t_1)$, $\ldots$ , $(\Gamma_n,t_n)$ such that:

1. $(\Gamma,t) = (\Gamma_n,t_n)$, and

2. for all $i$ such that $1\leq i\leq n$

   a. either $(\Gamma_i,t_i)\in \Delta$ or

   b. $(L_i,(\Gamma_i,t_i))\in{\cal D}$ for some list $L_i$ of members of $\Delta\cup\{(\Gamma_1,t_1),\ldots,(\Gamma_{i-1},t_{i-1})\}$.

The sequence $(\Gamma_1,t_1),\cdots,(\Gamma_n,t_n)$ is called a proof of $(\Gamma,t)$ from $\Delta$ with respect to ${\cal D}$.

Note that if $(\Gamma,t)$ follows from $\Delta$, then $(\Gamma,t)$ also follows from any $\Delta'$ such that $\Delta\subseteq\Delta'$. This property is called monotonicity.

The notation $t_1,\ldots,t_n\vdash_{{\cal D},\Delta} t$ means that the sequent $(\{t_1,\ldots,t_n\},\ t)$ follows from $\Delta$ by ${\cal D}$. If either ${\cal D}$ or $\Delta$ is clear from the context then it may be omitted. In the case that there are no hypotheses (i.e. $n=0$), just $\vdash t$ is written.

In practice, a particular deductive system is usually specified by a number of (schematic) rules of inference, which take the form

$$\frac{\Gamma_1\turn t_1 \qquad\cdots\qquad\Gamma_n\turn t_n} {\Gamma \turn t}$$

The sequents above the line are called the hypotheses of the rule and the sequent below the line is called its conclusion. Such a rule is schematic because it may contain metavariables standing for arbitrary terms of the appropriate types. Instantiating these metavariables with actual terms, one gets a list of sequents above the line and a single sequent below the line which together constitute a particular element of the deductive system. The instantiations allowed for a particular rule may be restricted by imposing a side condition on the rule.

The HOL deductive system

The deductive system of the HOL logic is specified by eight rules of inference, given below. The first three rules have no hypotheses; their conclusions can always be deduced. The identifiers in square brackets are the names of the ML functions in the HOL system that implement the corresponding inference rules (see DESCRIPTION). Any side conditions restricting the scope of a rule are given immediately below it.

Assumption introduction [ASSUME]

$$\overline{t \turn t}$$

Reflexivity [REFL]

$$\overline{\turn t = t}$$

Beta-conversion [BETA_CONV]

$$\overline{\turn (\lquant{x}t_1)t_2 = t_1[t_2/x]}$$

• Where $t_1[t_2/x]$ is the result of substituting $t_2$ for $x$ in $t_1$, with suitable renaming of variables to prevent free variables in $t_2$ becoming bound after substitution.

Substitution [SUBST]

$$\frac{\Gamma_1\turn t_1 = t_1'\qquad\cdots\qquad\Gamma_n\turn t_n = t_n'\qquad\qquad \Gamma\turn t[t_1,\ldots,t_n]} {\Gamma_1\cup\cdots\cup\Gamma_n\cup\Gamma\turn t[t_1',\ldots,t_n']}$$

• Where $t[t_1,\ldots,t_n]$ denotes a term $t$ with some free occurrences of subterms $t_1$, $\ldots$ , $t_n$ singled out and $t[t_1',\ldots,t_n']$ denotes the result of replacing each selected occurrence of $t_i$ by $t_i'$ (for $1{\leq}i{\leq}n$), with suitable renaming of variables to prevent free variables in $t_i'$ becoming bound after substitution.

Abstraction [ABS]

$$\frac{\Gamma\turn t_1 = t_2} {\Gamma\turn (\lquant{x}t_1) = (\lquant{x}t_2)}$$

• Provided $x$ is not free in $\Gamma$.

Type instantiation [INST_TYPE]

$$\frac{\Gamma\turn t} {\Gamma[\sigma_1,\ldots,\sigma_n/\alpha_1,\ldots,\alpha_n]\turn t[\sigma_1,\ldots,\sigma_n/\alpha_1,\ldots,\alpha_n]}$$

• Where $t[\sigma_1,\ldots,\sigma_n/\alpha_1,\ldots,\alpha_n]$ is the result of substituting, in parallel, the types $\sigma_1$, $\dots$, $\sigma_n$ for type variables $\alpha_1$, $\dots$, $\alpha_n$ in $t$, and where $\Gamma[\sigma_1,\ldots,\sigma_n/\alpha_1,\ldots,\alpha_n]$ is the result of performing the same substitution across all of the theorem’s hypotheses.

• After the instantiation, variables free in the input can not become bound, but distinct free variables in the input may become identified.

Discharging an assumption [DISCH]

$$\frac{\Gamma\turn t_2} {\Gamma -\{t_1\} \turn t_1 \imp t_2}$$

• Where $\Gamma -\{t_1\}$ is the set subtraction of $\{t_1\}$ from $\Gamma$.

Modus Ponens [MP]

$$\frac{\Gamma_1 \turn t_1 \imp t_2 \qquad\qquad \Gamma_2\turn t_1} {\Gamma_1 \cup \Gamma_2 \turn t_2}$$

In addition to these eight rules, there are also four axioms which could have been regarded as rules of inference without hypotheses. This is not done, however, since it is most natural to state the axioms using some defined logical constants and the principle of constant definition has not yet been described. The axioms are given in Section 2.4.3 and the definitions of the extra logical constants they involve are given in Section 2.4.2.

The particular set of rules and axioms chosen to axiomatize the HOL logic is rather arbitrary. It is partly based on the rules that were used in the LCF logic PPλ, since HOL was implemented by modifying the LCF system. In particular, the substitution rule SUBST is exactly the same as the corresponding rule in LCF; the code implementing this was written by Robin Milner and is highly optimized. Because substitution is such a pervasive activity in proof, it was felt to be important that the system primitive be as fast as possible. From a logical point of view it would be better to have a simpler substitution primitive, such as ‘Rule R’ of Andrews’ logic ${\cal Q}_0$, and then to derive more complex rules from it.

Soundness theorem

The rules of the HOL deductive system are sound for the notion of satisfaction defined in Section 2.2: for any instance of the rules of inference, if a (standard) model satisfies the hypotheses of the rule it also satisfies the conclusion.

Proof   The verification of the soundness of the rules is straightforward. The properties of the semantics with respect to substitution given by Lemmas 3 and 4 in Section 1.3.3 are needed for rules BETA_CONV, SUBST and INST_TYPE.² The fact that $=$ and $\imp$ are interpreted standardly (as in Section 1.4.2) is needed for rules REFL, BETA_CONV, SUBST, ABS, DISCH and MP.

HOL Theories

A HOL theory ${\cal T}$ is a $4$-tuple:

$${\cal T} = \langle\mathsf{Struc}_{\cal T},\mathsf{Sig}_{\cal T}, \mathsf{Axioms}_{\cal T},\mathsf{Theorems}_{\cal T}\rangle$$

where

1. $\mathsf{Struc}_{\cal T}$ is a type structure called the type structure of ${\cal T}$;

2. $\mathsf{Sig}_{\cal T}$ is a signature over $\mathsf{Struc}_{\cal T}$ called the signature of ${\cal T}$;

3. $\mathsf{Axioms}_{\cal T}$ is a set of sequents over $\mathsf{Sig}_{\cal T}$ called the axioms of ${\cal T}$;

4. $\mathsf{Theorems}_{\cal T}$ is a set of sequents over $\mathsf{Sig}_{\cal T}$ called the theorems of ${\cal T}$, with the property that every member follows from $\mathsf{Axioms}_{\cal T}$ by the HOL deductive system.

The sets $\mathsf{Types}_{\cal T}$ and $\mathsf{Terms}_{\cal T}$ of types and terms of a theory ${\cal T}$ are, respectively, the sets of types and terms constructable from the type structure and signature of ${\cal T}$, i.e.:

$$\begin{array}{rcl} \mathsf{Types}_{\cal T} & = & \mathsf{Types}_{\mathsf{Struc}_{\cal T}}\\ \mathsf{Terms}_{\cal T} & = & \mathsf{Terms}_{\mathsf{Sig}_{\cal T}} \end{array}$$

A model of a theory $\cal T$ is specified by giving a (standard) model $M$ of the underlying signature of the theory with the property that $M$ satisfies all the sequents which are axioms of $\cal T$. Because of the Soundness Theorem 2.3.2, it follows that $M$ also satisfies any sequents in the set of given theorems, $\mathsf{Theorems}_{\cal T}$.

The theory MIN

The minimal theory MIN is defined by:

$$\mathtt{MIN} = \langle\{(\ty{bool},0),\ (\ty{ind},0)\},\ \{\imp_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}, =_{\alpha\fun\alpha\fun\ty{bool}}, \hilbert_{(\alpha\fun\ty{bool})\fun\alpha}\},\ \{\},\ \{\}\rangle$$

Since the theory MIN has a signature consisting only of standard items and has no axioms, it possesses a unique standard model, which will be denoted Min.

Although the theory MIN contains only the minimal standard syntax, by exploiting the higher order constructs of HOL one can construct a rather rich collection of terms over it. The following theory introduces names for some of these terms that denote useful logical operations in the model Min.

In the implementation, the theory MIN is given the name min, and also contains the distinguished binary type operator $\fun$, for constructing function spaces.

The theory LOG

The theory LOG has the same type structure as MIN. Its signature contains the constants in MIN and the following constants:

$$\begin{array}{l} \con{T}_{\ty{bool}} \\ \forall_{(\alpha\fun\ty{bool})\fun\ty{bool}} \\ \exists_{(\alpha\fun\ty{bool})\fun\ty{bool}} \\ \con{F}_{\ty{bool}} \\ \neg_{\ty{bool}\fun\ty{bool}} \\ \wedge_{\ty{bool}\fun\ty{bool}\fun\ty{bool}} \\ \vee_{\ty{bool}\fun\ty{bool}\fun\ty{bool}} \\ \OneOne_{(\alpha\fun\beta)\fun\ty{bool}} \\ \Onto_{(\alpha\fun\beta)\fun\ty{bool}} \\ \TyDef_{(\alpha\fun\ty{bool})\fun(\beta\fun\alpha)\fun\ty{bool}} \end{array}$$

The following special notation is used in connection with these constants:

The axioms of the theory LOG consist of the following sequents:

$$\begin{array}{l} \turn \con{T} = ((\lquant{x_{\ty{bool}}}x) = (\lquant{x_{\ty{bool}}}x)) \\ \turn \forall = \lquant{P_{\alpha\fun\ty{bool}}}\ P = (\lquant{x}\con{T}) \\ \turn \exists = \lquant{P_{\alpha\fun\ty{bool}}}\ P({\hilbert}\ P) \\ \turn \con{F} = \uquant{b_{\ty{bool}}}\ b \\ \turn \neg = \lquant{b}\ b \imp \con{F} \\ \turn {\wedge} = \lquant{b_1\ b_2}\uquant{b} (b_1\imp (b_2 \imp b)) \imp b \\ \turn {\vee} = \lquant{b_1\ b_2}\uquant{b} (b_1 \imp b)\imp ((b_2 \imp b) \imp b) \\ \turn \OneOne = \lquant{f_{\alpha \fun\beta}}\uquant{x_1\ x_2} (f\ x_1 = f\ x_2) \imp (x_1 = x_2) \\ \turn \Onto = \lquant{f_{\alpha\fun\beta}} \uquant{y}\equant{x} y = f\ x \\ \turn \TyDef = \lambda P_{\alpha\fun\ty{bool}}\ rep_{\beta\fun\alpha}. \OneOne\ rep\ \wedge (\uquant{x}P\ x\ =\ (\equant{y} x = rep\ y)) \end{array}$$

Finally, as for the theory MIN, the set $\mathsf{Theorems}_{\mathtt{LOG}}$ is taken to be empty.

Note that the axioms of the theory LOG are essentially definitions of the new constants of LOG as terms in the original theory MIN. (The mechanism for making such extensions of theories by definitions of new constants will be set out in general in Section 2.5.1.) The first seven axioms define the logical constants for truth, universal quantification, existential quantification, falsity, negation, conjunction and disjunction. Although these definitions may be obscure to some readers, they are in fact standard definitions of these logical constants in terms of implication, equality and choice within higher order logic. The next two axioms define the properties of a function being one-one and onto; they will be used to express the axiom of infinity (see Section 2.4.3), amongst other things. The last axiom defines a constant used for type definitions (see Section 2.5.4).

The unique standard model Min of MIN gives rise to a unique standard model of LOG. This is because, given the semantics of terms set out in Section 1.3.2, to satisfy the above equations one is forced to interpret the new constants in the following way:

• $\den{\con{T}_{\ty{bool}}} = 1 \in \two$

• $\den{\forall_{(\alpha\fun\ty{bool})\fun\ty{bool}}}\in\prod_{X\in{\cal U}}(X\fun\two)\fun\two$ sends $X\in{\cal U}$ and $f\in X\fun\two$ to

  $$\den{\forall}(X)(f) = \left\{ \begin{array}{ll} 1 & \text{if } f^{-1}\{1\}=X \\ 0 & \text{otherwise} \end{array} \right.$$

• $\den{\exists_{(\alpha\fun\ty{bool})\fun\ty{bool}}}\in\prod_{X\in{\cal U}}(X\fun\two)\fun\two$ sends $X\in{\cal U}$ and $f\in X\fun\two$ to

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

• $\den{\con{F}_{\ty{bool}}} = 0 \in \two$

• $\den{\neg_{\ty{bool}\fun\ty{bool}}}\in\two\fun\two$ sends $b\in\two$ to

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

• $\den{\wedge_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}}\in\two\fun\two\fun\two$ sends $b,b'\in\two$ to

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

• $\den{\vee_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}}\in\two\fun\two\fun\two$ sends $b,b'\in\two$ to

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

• $\den{\OneOne_{(\alpha\fun\beta)\fun\ty{bool}}}\in\prod_{(X,Y)\in{\cal U}^{2}} (X\fun Y)\fun \two$ sends $(X,Y)\in{\cal U}^{2}$ and $f\in(X\fun Y)$ to

  $$\den{\OneOne}(X,Y)(f) = \left\{ \begin{array}{ll} 0 & \text{if } f(x)=f(x') \text{ for some } x\not=x' \text{ in } X \\ 1 & \text{otherwise} \end{array} \right.$$

• $\den{\Onto_{(\alpha\fun\beta)\fun\ty{bool}}}\in\prod_{(X,Y)\in{\cal U}^{2}} (X\fun Y)\fun \two$ sends $(X,Y)\in{\cal U}^{2}$ and $f\in(X\fun Y)$ to

  $$\den{\Onto}(X,Y)(f) = \left\{ \begin{array}{ll} 1 & \text{if } \{f(x):x\in X\}=Y \\ 0 & \text{otherwise} \end{array} \right.$$

• $\den{\TyDef_{(\alpha\fun\ty{bool})\fun(\beta\fun\alpha)\fun\ty{bool}}}\in \prod_{(X,Y)\in{\cal U}^{2}} (X\fun\two)\fun(Y\fun X)\fun\two$ sends $(X,Y)\in{\cal U}^{2}$, $f\in(X\fun\two)$ and $g\in(Y\fun X)$ to

  $$\den{\TyDef}(X,Y)(f)(g) = \left\{ \begin{array}{ll} 1 & \text{if } \den{\OneOne}(Y,X)(g)=1\\ & \text{and } f^{-1}\{1\}= \{g(y) : y\in Y\} \\ 0 & \text{otherwise.} \end{array} \right.$$

Since these definitions were obtained by applying the semantics of terms to the left hand sides of the equations which form the axioms of LOG, these axioms are satisfied and one obtains a model of the theory LOG.

The theory INIT

The theory INIT is obtained by adding the following four axioms to the theory LOG.

BOOL_CASES_AX   $\vdash \uquant{b} (b = \con{T}) \vee (b = \con{F})$

ETA_AX   $\vdash \uquant{f_{\alpha\fun\beta}}(\lquant{x}f\ x) = f$

SELECT_AX   $\vdash \uquant{P_{\alpha\fun\ty{bool}}\ x} P\ x \imp P({\hilbert}\ P)$

INFINITY_AX   $\vdash \equant{f_{\ty{ind}\fun \ty{ind}}} \OneOne \ f \conj \neg(\Onto \ f)$

The unique standard model of LOG satisfies these four axioms and hence is the unique standard model of the theory INIT. (For axiom SELECT_AX one needs to use the definition of $\den{\hilbert}$ given in Section 1.4.2; for axiom INFINITY_AX one needs the fact that $\den{\ty{ind}}=\inds$ is an infinite set.)

The theory INIT is the initial theory of the HOL logic. A theory which extends INIT will be called a standard theory.

Implementing theories LOG and INIT

The implementation combines the theories LOG and INIT into a theory bool. It includes all of the constants and axioms from those theories, and includes a number of derived results about those constants. For more on the implementation’s bool theory, see DESCRIPTION.

Consistency

A (standard) theory is consistent if it is not the case that every sequent over its signature can be derived from the theory’s axioms using the HOL logic, or equivalently, if the particular sequent $\turn\con{F}$ cannot be so derived.

The existence of a (standard) model of a theory is sufficient to establish its consistency. For by the Soundness Theorem 2.3.2, any sequent that can be derived from the theory’s axioms will be satisfied by the model, whereas the sequent $\turn\con{F}$ is never satisfied in any standard model. So in particular, the initial theory INIT is consistent.

However, it is possible for a theory to be consistent but not to possess a standard model. This is because the notion of a standard model is quite restrictive---in particular there is no choice how to interpret the integers and their arithmetic in such a model. The famous incompleteness theorem of Gödel ensures that there are sequents which are satisfied in all standard models (i.e. which are ‘true’), but which are not provable in the HOL logic.

Extensions of theories

A theory ${\cal T}'$ is said to be an extension of a theory ${\cal T}$ if:

1. $\mathsf{Struc}_{{\cal T}}\subseteq\mathsf{Struc}_{{\cal T}'}$.
2. $\mathsf{Sig}_{{\cal T}}\subseteq\mathsf{Sig}_{{\cal T}'}$.
3. $\mathsf{Axioms}_{{\cal T}}\subseteq\mathsf{Axioms}_{{\cal T}'}$.
4. $\mathsf{Theorems}_{{\cal T}}\subseteq\mathsf{Theorems}_{{\cal T}'}$.

In this case, any model $M'$ of the larger theory ${\cal T}'$ can be restricted to a model of the smaller theory $\cal T$ in the following way. First, $M'$ gives rise to a model of the structure and signature of $\cal T$ simply by forgetting the values of $M'$ at constants not in $\mathsf{Struc}_{\cal T}$ or $\mathsf{Sig}_{\cal T}$. Denoting this model by $M$, one has for all $\sigma\in\mathsf{Types}_{\cal T}$, $t\in\mathsf{Terms}_{\cal T}$ and for all suitable contexts that

$$\begin{array}{rcl} \den{\mathit{\alpha{}s}.\sigma}_{M} & = & \den{\mathit{\alpha{}s}.\sigma}_{M'} \\ \den{\mathit{\alpha{}s},\!\mathit{xs}.t}_{M} & = & \den{\mathit{\alpha{}s},\!\mathit{xs}.t}_{M'}. \end{array}$$

Consequently if $(\Gamma,t)$ is a sequent over $\mathsf{Sig}_{\cal T}$ (and hence also over $\mathsf{Sig}_{{\cal T}'}$), then $\Gamma \models_{M} t$ if and only if $\Gamma \models_{M'} t$. Since $\mathsf{Axioms}_{\cal T}\subseteq\mathsf{Axioms}_{{\cal T}'}$ and $M'$ is a model of ${\cal T}'$, it follows that $M$ is a model of $\cal T$. $M$ will be called the restriction of the model $M'$ of the theory ${\cal T}'$ to the subtheory $\cal T$.

There are two main mechanisms for making extensions of theories in HOL:

• Extension by a constant specification (see Section 2.5.2).

• Extension by a type specification (see Section 2.5.5).³

The first mechanism allows ‘loose specification’ of constants (as in the Z notation (Spivey 1989), for example); the latter allows new types and type-operators to be introduced. As special cases (when the thing being specified is uniquely determined) one also has:

• Extension by a constant definition (see Section 2.5.1).

• Extension by a type definition (see Section 2.5.4).

These mechanisms are described in the following sections. They all produce definitional extensions in the sense that they extend a theory by adding new constants and types which are defined in terms of properties of existing ones. Their key property is that the extended theory possesses a (standard) model if the original theory does. So a series of these extensions starting from the theory INIT is guaranteed to result in a theory with a standard model, and hence in a consistent theory. It is also possible to extend theories simply by adding new uninterpreted constants and types. This preserves consistency, but is unlikely to be useful without additional axioms. However, when adding arbitrary new axioms, there is no guarantee that consistency is preserved. The advantages of postulation over definition have been likened by Bertrand Russell to the advantages of theft over honest toil.⁴ As it is all too easy to introduce inconsistent axiomatizations, users of the HOL system are strongly advised to resist the temptation to add axioms, but to toil through definitional theories honestly.

Extension by constant definition

A constant definition over a signature $\Sigma_{\Omega}$ is a formula of the form $\con{c}_{\sigma} = t_{\sigma}$, such that:

1. $\con{c}$ is not the name of any constant in $\Sigma_{\Omega}$;

2. $t_{\sigma}$ a closed term in $\mathsf{Terms}_{\Sigma_{\Omega}}$;

3. all the type variables occurring in $t_\sigma$ also occur in $\sigma$.

Given a theory $\cal T$ and such a constant definition over $\mathsf{Sig}_{\cal T}$, then the definitional extension of ${\cal T}$ by $\con{c}_{\sigma}=t_{\sigma}$ is the theory ${\cal T}{+_{\mathit{def}}}\langle \con{c}_{\sigma}=t_{\sigma}\rangle$ defined by:

$${\cal T}{+_{\mathit{def}}}\langle \con{c}_{\sigma}=t_{\sigma}\rangle\ =\ \langle \begin{array}{l} \mathsf{Struc}_{\cal T},\ \mathsf{Sig}_{\cal T}\cup\{(\con{c},\sigma)\},\\ \mathsf{Axioms}_{\cal T}\cup\{ \con{c}_{\sigma}=t_{\sigma} \},\ \mathsf{Theorems}_{\cal T}\rangle \end{array}$$

Note that the mechanism of extension by constant definition has already been used implicitly in forming the theory LOG from the theory MIN in Section 2.4.2. Thus with the notation of this section one has

$$\mathtt{LOG}\; =\; \mathtt{MIN}\;\begin{array}{l} {+_{\mathit{def}}} \langle \con{T} \ =\ ((\lquant{x_{\ty{bool}}}x) = (\lquant{x_{\ty{bool}}}x))\rangle\\ {+_{\mathit{def}}}\langle {\forall}\ =\ \lquant{P_{\alpha\fun\ty{bool}}}\ P = (\lquant{x}\con{T})\rangle\\ {+_{\mathit{def}}}\langle {\exists}\ =\ \lquant{P_{\alpha\fun\ty{bool}}}\ P({\hilbert}\ P)\rangle\\ {+_{\mathit{def}}}\langle \con{F} \ =\ \uquant{b_{\ty{bool}}}\ b\rangle\\ {+_{\mathit{def}}}\langle \neg\ =\ \lquant{b}\ b \imp \con{F} \rangle\\ {+_{\mathit{def}}}\langle {\wedge}\ =\ \lquant{b_1\ b_2}\uquant{b} (b_1\imp (b_2 \imp b)) \imp b\rangle\\ {+_{\mathit{def}}}\langle {\vee}\ =\ \lquant{b_1\ b_2}\uquant{b} (b_1 \imp b)\imp ((b_2 \imp b) \imp b)\rangle\\ {+_{\mathit{def}}}\langle\OneOne \ =\ \lquant{f_{\alpha \fun\beta}} \uquant{x_1\ x_2} (f\ x_1 = f\ x_2) \imp (x_1 = x_2)\rangle\\ {+_{\mathit{def}}}\langle\Onto \ =\ \lquant{f_{\alpha\fun\beta}} \uquant{y}\equant{x} y = f\ x\rangle\\ {+_{\mathit{def}}}\langle\TyDef \ =\ \lambda P_{\alpha\fun\ty{bool}}\ rep_{\beta\fun\alpha}.\ \OneOne\ rep\ \wedge\ (\uquant{x}P\ x \ =\ (\equant{y} x = rep\ y)) \rangle \end{array}$$

If $\cal T$ possesses a standard model then so does the extension ${\cal T}{+_{\mathit{def}}}\langle\con{c}_{\sigma}=t_{\sigma}\rangle$. This will be proved as a corollary of the corresponding result in Section 2.5.2 by showing that extension by constant definition is in fact a special case of extension by constant specification. (This reduction requires that one is dealing with standard theories in the sense of Section 2.4.3, since although existential quantification is not needed for constant definitions, it is needed to state the mechanism of constant specification.)

Remark   Condition (iii) in the definition of what constitutes a correct constant definition is an important restriction without which consistency could not be guaranteed. To see this, consider the term $\equant{f_{\alpha\fun\alpha}} \OneOne \ f \conj \neg(\Onto \ f)$, which expresses the proposition that (the set of elements denoted by the) type $\alpha$ is infinite. The term contains the type variable $\alpha$, whereas the type of the term, $\ty{bool}$, does not. Thus by (iii)

$$\con{c}_{\ty{bool}} = \equant{f_{\alpha\fun\alpha}} \OneOne \ f \conj \neg(\Onto \ f)$$

is not allowed as a constant definition. The problem is that the meaning of the right hand side of the definition varies with $\alpha$, whereas the meaning of the constant on the left hand side is fixed, since it does not contain $\alpha$. Indeed, if we were allowed to extend the consistent theory INIT by this definition, the result would be an inconsistent theory. For instantiating $\alpha$ to $\ty{ind}$ in the right hand side results in a term that is provable from the axioms of INIT, and hence $\con{c}_{\ty{bool}}=\con{T}$ is provable in the extended theory. But equally, instantiating $\alpha$ to $\ty{bool}$ makes the negation of the right hand side provable from the axioms of INIT, and hence $\con{c}_{\ty{bool}}=\con{F}$ is also provable in the extended theory. Combining these theorems, one has that $\con{T}=\con{F}$, i.e. $\con{F}$ is provable in the extended theory.

Extension by constant specification

Constant specifications introduce constants (or sets of constants) that satisfy arbitrary given (consistent) properties. For example, a theory could be extended by a constant specification to have two new constants $\con{b}_1$ and $\con{b}_2$ of type $\ty{bool}$ such that $\neg(\con{b}_1=\con{b}_2)$. This specification does not uniquely define $\con{b}_1$ and $\con{b}_2$, since it is satisfied by either $\con{b}_1=\con{T}$ and $\con{b}_2=\con{F}$, or $\con{b}_1=\con{F}$ and $\con{b}_2=\con{T}$. To ensure that such specifications are consistent, they can only be made if it has already been proved that the properties which the new constants are to have are consistent. This rules out, for example, introducing three boolean constants $\con{b}_1$, $\con{b}_2$ and $\con{b}_3$ such that $\con{b}_1\neq \con{b}_2$, $\con{b}_1\neq \con{b}_3$ and $\con{b}_2\neq \con{b}_3$.

Suppose $\equant{x_1\cdots x_n}t$ is a formula, with $x_1,\ldots, x_n$ distinct variables. If $\turn \equant{x_1 \cdots x_n}t$, then a constant specification allows new constants $\con{c}_1$, $\ldots$ , $\con{c}_n$ to be introduced satisfying:

$$\turn t[\con{c}_1,\cdots,\con{c}_n/x_1,\cdots,x_n]$$

where $t[\con{c}_1,\cdots,\con{c}_n/x_1,\cdots,x_n]$ denotes the result of simultaneously substituting $\con{c}_1, \ldots, \con{c}_n$ for $x_1, \ldots, x_n$ respectively. Of course the type of each constant $\con{c}_i$ must be the same as the type of the corresponding variable $x_i$. To ensure that this extension mechanism preserves the property of possessing a model, a further more technical requirement is imposed on these types: they must each contain all the type variables occurring in $t$. This condition is discussed further in Section 2.5.3 below.

Formally, a constant specification for a theory ${\cal T}$ is given by

Data

$$\langle(\con{c}_1,\ldots,\con{c}_n), \lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}\rangle$$

Conditions

1. $\con{c}_1,\ldots,\con{c}_n$ are distinct names that are not the names of any constants in $\mathsf{Sig}_{\cal T}$.

2. $\lquant{{x_1}_{\sigma_1} \cdots {x_n}_{\sigma_n}}t_{\ty{bool}}\ \in\ \mathsf{Terms}_{\cal T}$.

3. $tyvars(t_{\ty{bool}})\ =\ tyvars(\sigma_i)$ for $1\leq i\leq n$.

4. $\equant{{x_1}_{\sigma_1}\ \cdots\ {x_n}_{\sigma_n}}t\ \in\ \mathsf{Theorems}_{\cal T}$.

The extension of a standard theory ${\cal T}$ by such a constant specification is denoted by

$${\cal T}{+_{\mathit{spec}}}\langle(\con{c}_1,\ldots,\con{c}_n), \lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} \rangle$$

and is defined to be the theory:

$$\langle \begin{array}{l} \mathsf{Struc}_{\cal T},\\ \mathsf{Sig}_{\cal T} \cup \{{\con{c}_1}_{\sigma_1}, \ldots, {\con{c}_n}_{\sigma_n}\},\\ \mathsf{Axioms}_{\cal T}\cup \{ t[\con{c}_1,\ldots,\con{c}_n/x_1,\ldots,x_n] \},\\ \mathsf{Theorems}_{\cal T} \rangle \end{array}$$

Proposition   The theory ${\cal T}{+_{\mathit{spec}}}\langle(\con{c}_1,\ldots,\con{c}_n), \lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}\rangle$ has a standard model if the theory ${\cal T}$ does.

Proof   Suppose $M$ is a standard model of ${\cal T}$. Let $\mathit{\alpha{}s}=\alpha_{1},\ldots,\alpha_{m}$ be the list of distinct type variables occurring in the formula $t$. Then $\mathit{\alpha{}s},\!\mathit{xs}.t$ is a term-in-context, where $\mathit{xs}=x_{1},\ldots,x_{n}$. (Change any bound variables in $t$ to make them distinct from $\mathit{xs}$ if necessary.) Interpreting this term-in-context in the model $M$ yields

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

Now $\equant{\mathit{xs}}t$ is in $\mathsf{Theorems}_{\cal T}$ and hence by the Soundness Theorem 2.3.2 this sequent is satisfied by $M$. Using the semantics of $\exists$ given in Section 2.4.2, this means that for all $\mathit{xs}\in{\cal U}^{m}$ the set

$$S(\mathit{xs}) = \{\mathit{ys}\in\den{\mathit{\alpha{}s}.\sigma_{1}}_{M}(\mathit{xs}) \times\cdots\times \den{\mathit{\alpha{}s}.\sigma_{n}}_{M}(\mathit{xs})\; : \; \den{\mathit{\alpha{}s},\!\mathit{xs}.t}_{M}(\mathit{xs})(\mathit{ys})=1 \}$$

is non-empty. Since it is also a subset of a finite product of sets in $\cal U$, it follows that it is an element of $\cal U$ (using properties Sub and Prod of the universe). So one can apply the global choice function $\ch\in\prod_{X\in{\cal U}}X$ to select a specific element

$$(s_{1}(\mathit{xs}),\ldots,s_{n}(\mathit{xs})) = \ch(S(\mathit{xs})) \in \prod_{i=1}^{n}\den{\mathit{\alpha{}s}.\sigma_{i}}_{M}(\mathit{xs})$$

at which $\den{\mathit{\alpha{}s},\!\mathit{xs}.t}_{M}(\mathit{xs})$ takes the value $1$. Extend $M$ to a model $M'$ of the signature of ${\cal T}{+_{\mathit{spec}}}\langle(\con{c}_1,\ldots,\con{c}_n), \lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}\rangle$ by defining its value at each new constant $(\con{c}_{i},\sigma_{i})$ to be

$$M'(\con{c}_{i},\sigma_{i}) = s_{i} \in \prod_{\mathit{xs}\in{\cal U}^{m}}\den{\sigma_{i}}_{M}(\mathit{xs}) .$$

Note that the Condition (iii) in the definition of a constant specification ensures that $\mathit{\alpha{}s}$ is the canonical context of each type $\sigma_{i}$, so that $\den{\sigma_{i}}=\den{\mathit{\alpha{}s}.\sigma_{i}}$ and thus $s_{i}$ is indeed an element of the above product.

Since $t$ is a term of the subtheory $\cal T$ of ${\cal T}{+_{\mathit{spec}}}\langle(\con{c}_1,\ldots,\con{c}_n), \lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}\rangle$, as remarked at the beginning of Section 2.5, one has that $\den{\mathit{\alpha{}s},\!\mathit{xs}.t}_{M'} = \den{\mathit{\alpha{}s},\!\mathit{xs}.t}_{M}$. Hence by definition of the $s_{i}$, for all $\mathit{xs}\in{\cal U}^{m}$

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

Then using Lemma 4 in Section 1.3.3 on the semantics of substitution together with the definition of $\den{\con{c}_{i}}_{M'}$, one finally obtains that for all $\mathit{xs}\in{\cal U}^{m}$

$$\den{t[\con{c}_{1},\ldots,\con{c}_{n}/x_{1},\ldots,x_{n}]}_{M'}(\mathit{xs})=1$$

or in other words that $M'$ satisfies $t[\con{c}_{1},\ldots,\con{c}_{n}/x_{1},\ldots,x_{n}]$. Hence $M'$ is a model of ${\cal T}{+_{\mathit{spec}}}\langle(\con{c}_1,\ldots,\con{c}_n), \lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}\rangle$, as required.

The constants which are asserted to exist in a constant specification are not necessarily uniquely determined. Correspondingly, there may be many different models of ${\cal T}{+_{\mathit{spec}}}\langle(\con{c}_1,\ldots,\con{c}_n), \lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}\rangle$ whose restriction to $\cal T$ is $M$; the above construction produces such a model in a uniform manner by making use of the global choice function on the universe.

Extension by a constant definition, $\con{c}_\sigma=t_\sigma$, is a special case of extension by constant specification. For let $t'$ be the formula $x_\sigma=t_\sigma$, where $x_\sigma$ is a variable not occurring in $t_\sigma$. Then clearly $\turn \equant{x_\sigma}t'$ and one can apply the method of constant specification to obtain the theory

$${\cal T}{+_{\mathit{spec}}}\langle \con{c},\lquant{x_\sigma}t'\rangle$$

But since $t'[\con{c}_\sigma/x_\sigma]$ is just $\con{c}_\sigma=t_\sigma$, this extension yields exactly ${\cal T}{+_{\mathit{def}}}\langle \con{c}_{\sigma}=t_{\sigma}\rangle$. So as a corollary of the Proposition, one has that for each standard model $M$ of $\cal T$, there is a standard model $M'$ of ${\cal T}{+_{\mathit{def}}}\langle\con{c}_{\sigma}=t_{\sigma}\rangle$ whose restriction to $\cal T$ is $M$. In contrast with the case of constant specifications, $M'$ is uniquely determined by $M$ and the constant definition.

Remarks about constants in HOL

Note how Condition (iii) in the definition of a constant specification was needed in the proof that the extension mechanism preserves the property of possessing a standard model. Its role is to ensure that the introduced constants have, via their types, the same dependency on type variables as does the formula loosely specifying them. The situation is the same as that discussed in the Remark in Section 2.5.1. In a sense, what is causing the problem in the example given in that Remark is not so much the method of extension by introducing constants, but rather the syntax of HOL which does not allow constants to depend explicitly on type variables (in the way that type operators can). Thus in the example one would like to introduce a ‘polymorphic’ constant $\con{c}_{\ty{bool}}(\alpha)$ explicitly depending upon $\alpha$, and define it to be $\equant{f_{\alpha\fun\alpha}} \OneOne \ f \conj \neg(\Onto \ f)$. Then in the extended theory one could derive $\con{c}_{\ty{bool}}(\ty{ind})=\con{T}$ and $\con{c}_{\ty{bool}}(\ty{bool})=\con{F}$, but now no contradiction results since $\con{c}_{\ty{bool}}(\ty{ind})$ and $\con{c}_{\ty{bool}}(\ty{bool})$ are different.

In the current version of HOL, constants are (name,type)-pairs. One can envision a slight extension of the HOL syntax with ‘polymorphic’ constants, specified by pairs $(\con{c},\mathit{\alpha{}s}.\sigma)$ where now $\mathit{\alpha{}s}.\sigma$ is a type-in-context and the list $\mathit{\alpha{}s}$ may well contain extra type variables not occurring in $\sigma$. Such a pair would give rise to the particular constant term $\con{c}_\sigma(\mathit{\alpha{}s})$, and more generally to constant terms $\con{c}_{\sigma'}(\mathit{\tau{}s})$ obtained from this one by instantiating the type variables $\alpha_i$ with types $\tau_i$ (so $\sigma'$ is the instance of $\sigma$ obtained by substituting $\mathit{\tau{}s}$ for $\mathit{\alpha{}s}$). This new syntax of polymorphic constants is comparable to the existing syntax of compound types (see Section 1.2): an $n$-ary type operator $\mathit{op}$ gives rise to a compound type $(\alpha_1,\ldots,\alpha_n){\mathit{op}}$ depending upon $n$ type variables. Similarly, the above syntax of polymorphic constants records how they depend upon type variables (as well as which generic type the constant has).

However, explicitly recording dependency of constants on type variables makes for a rather cumbersome syntax which in practice one would like to avoid where possible. It is possible to avoid it if the type context $\mathit{\alpha{}s}$ in $(\con{c},\mathit{\alpha{}s}.\sigma)$ is actually the canonical context of $\sigma$, i.e. contains exactly the type variables of $\sigma$. For then one can apply Lemma 1 of Section 1.2.3 to deduce that the polymorphic constant $\con{c}_{\sigma'}(\mathit{\tau{}s})$ can be abbreviated to the ordinary constant $\con{c}_{\sigma'}$ without ambiguity—the missing information $\mathit{\tau{}s}$ can be reconstructed from $\sigma'$ and the information about the constant $\con{c}$ given in the signature. From this perspective, the rather technical side Conditions (iii) in Sections 2.5.1 and 2.5.2 become rather less mysterious: they precisely ensure that in introducing new constants one is always dealing just with canonical contexts, and so can use ordinary constants rather than polymorphic ones without ambiguity. In this way one avoids complicating the existing syntax at the expense of restricting somewhat the applicability of these theory extension mechanisms.

Extension by type definition

Every (monomorphic) type $\sigma$ in the initial theory INIT determines a set $\den{\sigma}$ in the universe $\cal U$. However, there are many more sets in $\cal U$ than there are types in INIT. In particular, whilst $\cal U$ is closed under the operation of taking a non-empty subset of $\den{\sigma}$, there is no corresponding mechanism for forming a ‘subtype’ of $\sigma$. Instead, subsets are denoted indirectly via characteristic functions, whereby a closed term $p$ of type $\sigma\fun\ty{bool}$ determines the subset $\{x\in\den{\sigma} : \den{p}(x)=1\}$ (which is a set in the universe provided it is non-empty). However, it is useful to have a mechanism for introducing new types which are subtypes of existing ones. Such types are defined in HOL by introducing a new type constant and asserting an axiom that characterizes it as denoting a set in bijection (i.e. one-to-one correspondence) with a non-empty subset of an existing type (called the representing type). For example, the type num is defined to be equal to a countable subset of the type ind, which is guaranteed to exist by the axiom INFINITY_AX (see Section 2.4.3).

As well as defining types, it is also convenient to be able to define type operators. An example would be a type operator $\ty{inj}$ which mapped a set to the set of one-to-one (i.e. injective) functions on it. The subset of $\sigma\fun\sigma$ representing $(\sigma)\ty{inj}$ would be defined by the predicate $\OneOne$. Another example would be a binary cartesian product type operator $\ty{prod}$. This is defined by choosing a representing type containing two type variables, say $\sigma[\alpha_1;\alpha_2]$, such that for any types $\sigma_1$ and $\sigma_2$, a subset of $\sigma[\sigma_1;\sigma_2]$ represents the cartesian product of $\sigma_1$ and $\sigma_2$. The details of such a definition are given in DESCRIPTION’s section on the theory of cartesian products.

Types in HOL must denote non-empty sets. Thus it is only consistent to define a new type isomorphic to a subset specified by a predicate $p$, if there is at least one thing for which $p$ holds, i.e. $\turn\equant{x}p\ x$. For example, it would be inconsistent to define a binary type operator $\ty{iso}$ such that $(\sigma_1,\sigma_2)\ty{iso}$ denoted the set of one-to-one functions from $\sigma_1$ onto $\sigma_2$ because for some values of $\sigma_1$ and $\sigma_2$ the set would be empty; for example $(\ty{ind},\ty{bool})\ty{iso}$ would denote the empty set. To avoid this, a precondition of defining a new type is that the representing subset is non-empty.

To summarize, a new type is defined by:

1. Specifying an existing type.
2. Specifying a subset of this type.
3. Proving that this subset is non-empty.
4. Specifying that the new type is isomorphic to this subset.

In more detail, defining a new type $(\alpha_1,\ldots,\alpha_n)\ty{op}$ consists in:

1. Specifying a type-in-context, $\alpha_1,\ldots,\alpha_n.\sigma$ say. The type $\sigma$ is called the representing type, and the type $(\alpha_1,\ldots,\alpha_n)\ty{op}$ is intended to be isomorphic to a subset of $\sigma$.

2. Specifying a closed term-in-context, $\alpha_1,\ldots,\alpha_n,.p$ say, of type $\sigma\fun\ty{bool}$. The term $p$ is called the characteristic function. This defines the subset of $\sigma$ to which $(\alpha_1,\ldots,\alpha_n)\ty{op}$ is to be isomorphic.⁵

3. Proving $\turn \equant{x_{\sigma}} p\ x$.

4. Asserting an axiom saying that $(\alpha_1,\ldots,\alpha_n)\ty{op}$ is isomorphic to the subset of $\sigma$ selected by $p$.

To make this formal, the theory LOG provides the polymorphic constant $\TyDef$ defined in Section 2.4.2. The formula $\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\ p\ f$ asserts that there exists a one-to-one map $f$ from $(\alpha_1,\ldots,\alpha_n)\ty{op}$ onto the subset of elements of $\sigma$ for which $p$ is true. Hence, the axiom that characterizes $(\alpha_1,\ldots,\alpha_n)\ty{op}$ is:

$$\turn \equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\ p\ f$$

Defining a new type $(\alpha_1,\ldots,\alpha_n)\ty{op}$ in a theory ${\cal T}$ thus consists of introducing $\ty{op}$ as a new $n$-ary type operator and the above axiom as a new axiom. Formally, a type definition for a theory ${\cal T}$ is given by

Data

$$\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\ \sigma,\ p_{\sigma\fun\ty{bool}}\rangle$$

Conditions

1. $(\ty{op},n)$ is not the name of a type constant in $\mathsf{Struc}_{\cal T}$.

2. $\alpha_1,\ldots,\alpha_n.\sigma$ is a type-in-context with $\sigma \in\mathsf{Types}_{\cal T}$.

3. $p_{\sigma\fun\ty{bool}}$ is a closed term in $\mathsf{Terms}_{\cal T}$ whose type variables occur in $\alpha_1,\ldots,\alpha_n$.

4. $\equant{x_{\sigma}}p\ x \ \in\ \mathsf{Theorems}_{\cal T}$.

The extension of a standard theory ${\cal T}$ by a such a type definition is denoted by

$${\cal T}{+_{tydef}}\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle$$

and defined to be the theory

$$\langle \begin{array}{l} \mathsf{Struc}_{\cal T}\cup\{(\ty{op},n)\},\\ \mathsf{Sig}_{\cal T},\\ \mathsf{Axioms}_{\cal T}\cup\{ \equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op} \fun\sigma}}\TyDef\ p\ f\},\\ \mathsf{Theorems}_{\cal T}\rangle \end{array}$$

Proposition   The theory ${\cal T}{+_{\mathit{tydef}}}\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle$ has a standard model if the theory ${\cal T}$ does.

Instead of giving a direct proof of this result, it will be deduced as a corollary of the corresponding proposition in the next section.

Extension by type specification

(Note: This theory extension mechanism is not implemented in the HOL4 system. It was proposed by T. Melham and refines a suggestion from R. Jones and R. Arthan.)

The type definition mechanism allows one to introduce new types by giving a concrete representation of the type as a ‘subtype’ of an existing type. One might instead wish to introduce a new type satisfying some property without having to give an explicit representation for the type. For example, one might want to extend INIT with an atomic type $\ty{one}$ satisfying $\turn\uquant{f_{\alpha\fun\ty{one}}\ g_{\alpha\fun\ty{one}}}f=g$ without choosing a specific type in INIT and saying that $\ty{one}$ is in bijection with a one-element subset of it. (The idea being that the choice of representing type is irrelevant to the properties of $\ty{one}$ that can be expressed in HOL.) The mechanism described in this section provides one way of achieving this while at the same time preserving the all-important property of possessing a standard model and hence maintaining consistency.

Each closed formula $q$ involving a single type variable $\alpha$ can be thought of as specifying a property $q[\tau/\alpha]$ of types $\tau$. Its interpretation in a model is of the form

$$\den{\alpha,.q}\in \prod_{X\in{\cal U}}\den{\alpha.\ty{bool}}(X) \;= \prod_{X\in{\cal U}}\two \;=\; {\cal U}\fun\two$$

which is a characteristic function on the universe, determining a subset $\{X\in{\cal U}:\den{\alpha,.q}(X)=1\}$ consisting of those sets in the universe for which the property $q$ holds. The most general way of ensuring the consistency of introducing a new atomic type $\nu$ satisfying $q[\nu/\alpha]$ would be to prove '$\equant{\alpha}q$'. However, such a formula with quantification over types is not⁶ a part of the HOL logic and one must proceed indirectly---replacing the formula by (a logically weaker) one that can be expressed formally with HOL syntax. The formula used is

$$(\equant{f_{\alpha\fun\sigma}}\TyDef\ p\ f)\ \imp\ q$$

where $\sigma$ is a type, $p_{\sigma\fun\ty{bool}}$ is a closed term and neither involve the type variable $\alpha$. This formula says '$q$ holds of any type which is in bijection with the subtype of $\sigma$ determined by $p$'. If this formula is provable and if the subtype is non-empty, i.e. if

$$\equant{x_\sigma}p\ x$$

is provable, then it is consistent to introduce an extension with a new atomic type $\nu$ satisfying $q[\nu/\alpha]$.

In giving the formal definition of this extension mechanism, two refinements will be made. Firstly, $\sigma$ is allowed to be polymorphic and hence a new type constant of appropriate arity is introduced, rather than just an atomic type. Secondly, the above existential formulas are permitted to be proved (in the theory to be extended) from some hypotheses.⁷ Thus a type specification for a theory $\cal T$ is given by

Data

$$\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q\rangle$$

Conditions

1. $(\ty{op},n)$ is a type constant that is not in $\mathsf{Struc}_{\cal T}$.

2. $\alpha_1,\ldots,\alpha_n.\sigma$ is a type-in-context with $\sigma\in\mathsf{Types}_{\cal T}$.

3. $p_{\sigma\fun\ty{bool}}$ is a closed term in $\mathsf{Terms}_{\cal T}$ whose type variables occur in $\mathit{\alpha{}s}=\alpha_1,\ldots,\alpha_n$.

4. $\alpha$ is a type variable distinct from those in $\mathit{\alpha{}s}$.

5. $\Gamma$ is a list of closed formulas in $\mathsf{Terms}_{\cal T}$ not involving the type variable $\alpha$.

6. $q$ is a closed formula in $\mathsf{Terms}_{\cal T}$.

7. The sequents

   $$\begin{array}{rcl} (\Gamma & , & \equant{x_\sigma}p\ x )\\ (\Gamma & , & (\equant{f_{\alpha\fun\sigma}}\TyDef\ p\ f)\ \imp\ q ) \end{array}$$

   are in $\mathsf{Theorems}_{\cal T}$.

The extension of a standard theory $\cal T$ by such a type specification is denoted

$${\cal T}{+_{\mathit{tyspec}}} \langle (\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q\rangle$$

and is defined to be the theory

$$\langle \begin{array}{l} \mathsf{Struc}_{\cal T}\cup\{(\ty{op},n)\},\\ \mathsf{Sig}_{\cal T},\\ \mathsf{Axioms}_{\cal T}\cup\{(\Gamma , q[(\alpha_1,\ldots,\alpha_n)\ty{op}/\alpha])\},\\ \mathsf{Theorems}_{\cal T}\rangle \end{array}$$

Example   To carry out the extension of INIT mentioned at the start of this section, one forms

$$\mathtt{INIT}{+_{\mathit{tyspec}}} \langle ()\ty{one},\ty{bool},p,\alpha,\emptyset,q\rangle$$

where $p$ is the term $\lquant{b_{\ty{bool}}}b$ and $q$ is the formula $\uquant{f_{\beta\fun\alpha}\ g_{\beta\fun\alpha}}f=g$. Thus the result is a theory extending INIT with a new type constant $\ty{one}$ satisfying the axiom $\uquant{f_{\beta\fun\ty{one}}\ g_{\beta\fun\ty{one}}}f=g$.

To verify that this is a correct application of the extension mechanism, one has to check Conditions (i) to (vii) above. Only the last one is non-trivial: it imposes the obligation of proving two sequents from the axioms of INIT. The first sequent says that $p$ defines an inhabited subset of $\ty{bool}$, which is certainly the case since $\con{T}$ witnesses this fact. The second sequent says in effect that any type $\alpha$ that is in bijection with the subset of $\ty{bool}$ defined by $p$ has the property that there is at most one function to it from any given type $\beta$; the proof of this from the axioms of INIT is left as an exercise.

Proposition   The theory ${\cal T}{+_{\mathit{tyspec}}}\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q\rangle$ has a standard model if the theory ${\cal T}$ does.

Proof   Write $\mathit{\alpha{}s}$ for $\alpha_1,\ldots,\alpha_n$, and suppose that $\mathit{\alpha{}s}'={\alpha'}_1,\ldots,{\alpha'}_m$ is the list of type variables occurring in $\Gamma$ and $q$, but not already in the list $\mathit{\alpha{}s},\alpha$.

Suppose $M$ is a standard model of ${\cal T}$. Since $\mathit{\alpha{}s},.p$ is a term-in-context of type $\sigma\fun\ty{bool}$, interpreting it in $M$ yields

$$\den{\mathit{\alpha{}s},.p}_{M} \in \prod_{\mathit{xs}\in{\cal U}^{n}}\den{\mathit{\alpha{}s}.\sigma\fun\ty{bool}}_M(\mathit{xs}) = \prod_{\mathit{xs}\in{\cal U}^{n}} \den{\mathit{\alpha{}s}.\sigma}_M(\mathit{xs})\fun\two .$$

There is no loss of generality in assuming that $\Gamma$ consists of a single formula $\gamma$. (Just replace $\Gamma$ by the conjunction of the formulas it contains, with the convention that this conjunction is $\con{T}$ if $\Gamma$ is empty.) By assumption on $\mathit{\alpha{}s}'$ and by Condition (iv), $\mathit{\alpha{}s},\mathit{\alpha{}s}',.\gamma$ is a term-in-context.⁸ Interpreting it in $M$ yields

$$\den{\mathit{\alpha{}s},\mathit{\alpha{}s}',.\gamma}_{M} \in \prod_{(\mathit{xs},\mathit{xs}')\in {\cal U}^{n+m}}\den{\mathit{\alpha{}s},\mathit{\alpha{}s}'.\ty{bool}}_M(\mathit{xs},\mathit{xs}') ={\cal U}^{n+m}\fun\two$$

Now $(\gamma,\equant{x_{\sigma}}p\ x)$ is in $\mathsf{Theorems}_{\cal T}$ and hence by the Soundness Theorem 2.3.2 this sequent is satisfied by $M$. Using the semantics of $\exists$ given in Section 2.4.2 and the definition of satisfaction of a sequent from Section 2.2, this means that for all $(\mathit{xs},\mathit{xs}')\in{\cal U}^{n+m}$ if $\den{\mathit{\alpha{}s},\mathit{\alpha{}s}',.\gamma}_M(\mathit{xs},\mathit{xs}')=1$, then the set

$$\{y\in\den{\mathit{\alpha{}s}.\sigma}_{M}\: :\: \den{\mathit{\alpha{}s},.p}(\mathit{xs})(y)=1\}$$

is non-empty. (This uses the fact that $p$ does not involve the type variables $\mathit{\alpha{}s}'$, so that by Lemma 4 in Section 1.3.3 $\den{\mathit{\alpha{}s},\mathit{\alpha{}s}',.p}_M(\mathit{xs},\mathit{xs}')=\den{\mathit{\alpha{}s},.p}_M(\mathit{xs})$.) Since it is also a subset of a set in $\cal U$, it follows by property Sub of the universe that this set is an element of $\cal U$. So defining

$$S(\mathit{xs}) = \left\{ \begin{array}{ll} \{y\in\den{\mathit{\alpha{}s}.\sigma}_{M} : \den{\mathit{\alpha{}s},.p}(\mathit{xs})(y)=1\} & \text{if } \den{\mathit{\alpha{}s},.\gamma}_M(\mathit{xs},\mathit{xs}')=1, \text{ some } \mathit{xs}'\\ 1 & \text{otherwise} \end{array} \right.$$

one has that $S$ is a function ${\cal U}^n\fun{\cal U}$. Extend $M$ to a model of the signature of ${\cal T}'$ by defining its value at the new $n$-ary type constant $\ty{op}$ to be this function $S$. Note that the values of $\sigma$, $p$, $\gamma$ and $q$ in $M'$ are the same as in $M$, since these expressions do not involve the new type constant $\ty{op}$.

For each $\mathit{xs}\in{\cal U}^{n}$ define $i_{\mathit{xs}}$ to be the inclusion function for the subset $S(\mathit{xs})\subseteq\den{\mathit{\alpha{}s}.\sigma}_{M}$ if $\den{\mathit{\alpha{}s},\mathit{\alpha{}s}',.\gamma}_M(\mathit{xs},\mathit{xs}')=1$ for some $\mathit{xs}'$, and otherwise to be the function $1\fun\den{\mathit{\alpha{}s}.\sigma}_{M}$ sending $0\in 1$ to $\ch(\den{\mathit{\alpha{}s}.\sigma}_{M})$. Then $i_{\mathit{xs}}\in(S(\mathit{xs})\fun\den{\mathit{\alpha{}s}.\sigma}_{M'}(\mathit{xs}))$ because $\den{\mathit{\alpha{}s}.\sigma}_{M'}=\den{\mathit{\alpha{}s}.\sigma}_M$. Using the semantics of $\TyDef$ given in Section 2.4.2, one has that for any $(\mathit{xs},\mathit{xs}')\in{\cal U}^{n+m}$, if $\den{\mathit{\alpha{}s},\mathit{\alpha{}s}',.\gamma}_{M'}(\mathit{xs},\mathit{xs}')=1$ then

$$\den{\TyDef}_{M'}(\den{\mathit{\alpha{}s}.\sigma}_{M'} , S(\mathit{xs}))(\den{\mathit{\alpha{}s},.p}_{M'})(i_{\mathit{xs}}) = 1.$$

Thus $M'$ satisfies the sequent

$$(\gamma\ ,\ \equant{f_{(\mathit{\alpha{}s})\ty{op}\fun\sigma}}\TyDef\ p\ f).$$

But since the sequent $(\gamma,(\equant{f_{\alpha\fun\sigma}}\TyDef\ p\ f)\ \imp\ q )$ is in $\mathsf{Theorems}_{\cal T}$, it is satisfied by the model $M$ and hence also by the model $M'$ (since the sequent does not involve the new type constant $\ty{op}$). Instantiating $\alpha$ to $(\mathit{\alpha{}s})\ty{op}$ in this sequent (which is permissible since by Condition (iv) $\alpha$ does not occur in $\gamma$), one thus has that $M'$ satisfies the sequent

$$(\gamma\ ,\ (\equant{f_{(\mathit{\alpha{}s})\ty{op}\fun\sigma}}\TyDef\ p\ f)\imp q[(\mathit{\alpha{}s})\ty{op}/\alpha]).$$

Applying Modus Ponens, one concludes that $M'$ satisfies $(\gamma\ ,\ q[(\mathit{\alpha{}s})\ty{op}/\alpha])$ and therefore $M'$ is a model of ${\cal T}'$, as required.

An extension by type definition is in fact a special case of extension by type specification. To see this, suppose $\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\ \sigma,\ p_{\sigma\fun\ty{bool}}\rangle$ is a type definition for a theory $\cal T$. Choosing a type variable $\alpha$ different from $\alpha_1,\ldots,\alpha_n$, let $q$ denote the formula

$$\equant{f_{\alpha\fun\sigma}}\TyDef\ p\ f$$

Then $\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\emptyset,q\rangle$ satisfies all the conditions necessary to be a type specification for $\cal T$. Since $q[(\alpha_1,\ldots,\alpha_n)\ty{op}/\alpha]$ is just $\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\ p\ f$, one has that

$$\begin{array}{l} {\cal T}{+_{tydef}} \langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle\\ \quad ={\cal T}{+_{\mathit{tyspec}}} \langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\emptyset,q\rangle \end{array}$$

Thus the Proposition in Section 2.5.4 is a special case of the above Proposition.

In an extension by type specification, the property $q$ which is asserted of the newly introduced type constant need not determine the type constant uniquely (even up to bijection). Correspondingly there may be many different standard models of the extended theory whose restriction to $\cal T$ is a given model $M$. By contrast, a type definition determines the new type constant uniquely up to bijection, and any two models of the extended theory which restrict to the same model of the original theory will be isomorphic.

1. Note that the type subscript is omitted from terms when it is clear from the context that they are formulas, i.e. have type $\ty{bool}$. ↩

2. Note in particular that the second restriction on INST_TYPE enables the result on the semantics of substituting types for type variables in terms to be applied. ↩

3. This theory extension mechanism is not implemented in the HOL4 system. ↩

4. See page 71 of Russell’s book Introduction to Mathematical Philosophy. ↩

5. The reason for restricting $p$ to be closed, i.e. to have no free variables, is that otherwise for consistency the defined type operator would have to depend upon (i.e. be a function of) those variables. Such dependent types are not (yet!) a part of the HOL system. ↩

6. yet! ↩

7. This refinement increases the applicability of the extension mechanism without increasing its expressive power. A similar refinement could have be made to the other theory extension mechanisms. ↩

8. Note the two commas in $\mathit{\alpha{}s},\mathit{\alpha{}s}',.\gamma$. The first separates the two lists of type variables; the second splits type variables from term variables. ↩

References