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