xref: /seL4-l4v-master/HOL4/Manual/Logic/semantics.tex

% Revised version of Part II, Chapter 10 of HOL DESCRIPTION
% Incorporates material from both of chapters 9 and 10 of the old
% version of DESCRIPTION
% Written by Andrew Pitts
% 8 March 1991
% revised August 1991
\chapter{Theories}\label{semantics}

\section{Introduction}

The result, if any, of a session with the \HOL{} system is an object
called a {\it theory\/}.  This object is closely related to what a
logician would call a theory\index{theories, in HOL logic@theories, in \HOL{} logic!abstract form of}, 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 {\it 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 {\em
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, \ie\ 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.


\section{Sequents}
\label{sequents}

The \HOL{} logic is phrased in terms of hypothetical assertions called
{\em sequents}.\index{sequents!in natural deduction} 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$.\footnote{Note that
the type subscript is omitted from terms when it is clear from the
context that they are formulas, \ie\ have type \ty{bool}.} The set of
formulas $\Gamma$ forming the first component of a sequent is called
its set of {\it assumptions\/}\index{assumptions!of sequents} and the
term $t$ forming the second component is called its {\it
conclusion\/}\index{conclusions!of sequents}. When it is not ambiguous
to do so, a sequent $(\{\},t)$ is written as just $t$.


Intuitively, a model $M$ of $\Sigma_\Omega$ {\em
satisfies}\index{satisfaction of sequents, by model}  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  $\alpha\!s,\!x\!s$ 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
$\alpha\!s$ has length $n$, that $x\!s=x_{1},\ldots,x_{m}$ and that the
type of $x_{j}$ is $\sigma_{j}$. Since formulas are terms of type
$\bool$, the semantics of terms defined in the previous chapter gives
rise to elements $\den{\alpha\!s,\!x\!s.t}_M$ and
$\den{\alpha\!s,\!x\!s.t_{k}}_M$ ($k=1,\ldots,p$) in
\[
\prod_{X\!s\in{\cal U}^{n}} \left(
\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}_M(X\!s)\right) \fun \:\two  \]
Say that the model $M$ {\em satisfies\/} the sequent $(\Gamma,t)$ and
write
\[
\Gamma \models_{M} t
\]
if for all $X\!s\in{\cal U}^{n}$ and
all $y\!s\in\den{\alpha\!s.\sigma_{1}}_M(X\!s)\times\cdots\times
\den{\alpha\!s.\sigma_{m}}_M(X\!s)$ with
\[
\den{\alpha\!s,\!x\!s.t_{k}}_M(X\!s)(y\!s)=1
\]
for all $k=1,\ldots,p$, it is also the case that
\[
\den{\alpha\!s,\!x\!s.t}_M(X\!s)(y\!s)=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_{X\!s\in{\cal U}^{n}}
\left(\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}_M(X\!s)\right) \fun \:\two
\]
is constant with value $1\in\two$.

\section{Logic}

A deductive system\index{deductive systems}
${\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\index{follows from, in natural deduction}
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:
\begin{enumerate}
\item $(\Gamma,t) = (\Gamma_n,t_n)$, and
\item for all $i$ such that $1\leq i\leq n$
\begin{enumerate}
\item either
$(\Gamma_i,t_i)\in \Delta$ or
\item $(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})\}$.
\end{enumerate}
\end{enumerate}
The sequence $(\Gamma_1,t_1),\cdots,(\Gamma_n,t_n)$
is called a {\it proof\/}\index{proof!in natural deduction} 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 {\it monotonicity\/}\index{monotonicity, in deductive systems}.

The notation\index{turnstile 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\index{hypotheses!of sequents} (\ie\ $n=0$),
just $\vdash t$ is written.

In practice, a particular deductive system is usually specified by a
number of (schematic) \emph{rules of inference},
\index{inference rules, of HOL logic@inference rules, of \HOL{} logic!abstract form of primitive}
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 {\it
hypotheses\/}\index{hypotheses!of inference rules} of the rule and the
sequent below the line is called its {\it
conclusion}.\index{conclusions!of inference rules} 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 {\em side condition\/} on the rule.


\subsection{The \HOL{} deductive system}
\label{HOLrules}

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.

\bigskip

\subsubsection*{Assumption introduction [{\small\tt
ASSUME}]}\index{assumption introduction, in HOL logic@assumption introduction, in \HOL{} logic!abstract form of}
\[
\overline{t \turn t}
\]

\subsubsection*{Reflexivity [{\small\tt
REFL}]}\index{REFL@\ml{REFL}}\index{reflexivity, in HOL logic@reflexivity, in \HOL{} logic!abstract form of}
\[
\overline{\turn t = t}
\]

\subsubsection*{Beta-conversion [{\small\tt BETA\_CONV}]}
\index{beta-conversion, in HOL logic@beta-conversion, in \HOL{} logic!abstract form of}\index{BETA_CONV@\ml{BETA\_CONV}}
\[
\overline{\turn (\lquant{x}t_1)t_2 = t_1[t_2/x]}
\]
\begin{itemize}
\item 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.
\end{itemize}

\subsubsection*{Substitution [{\small\tt
SUBST}]}\index{SUBST@\ml{SUBST}} \index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!abstract form of}
\[
\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']}
\]
\begin{itemize}
\item 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.
\end{itemize}

\subsubsection*{Abstraction [{\small\tt ABS}]}
\index{ABS@\ml{ABS}}\index{abstraction rule, in HOL logic@abstraction rule, in \HOL{} logic!abstract form of}
\[
\frac{\Gamma\turn t_1 = t_2}
{\Gamma\turn (\lquant{x}t_1) = (\lquant{x}t_2)}
\]
\begin{itemize}
\item Provided $x$ is not free in $\Gamma$.
\end{itemize}

\subsubsection*{Type instantiation [{\small\tt INST\_TYPE}]}
\index{type instantiation, in HOL logic@type instantiation, in \HOL{} logic!abstract form of}
\newcommand{\insttysub}{[\sigma_1,\ldots,\sigma_n/\alpha_1,\ldots,\alpha_n]}
\[
\frac{\Gamma\turn t}
{\Gamma\insttysub\turn t\insttysub}
\]
\begin{itemize}
\item Where $t\insttysub$ 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\insttysub$
  is the result of performing the same substitution across all of the
  theorem's hypotheses.
\item After the instantiation, variables free in the input can not
  become bound, but distinct free variables in the input may become
  identified.
\end{itemize}

\subsubsection*{Discharging an assumption [{\small\tt
DISCH}]}\index{discharging assumptions, in HOL logic@discharging assumptions, in \HOL{} logic!abstract form of}\index{DISCH@\ml{DISCH}}
\[
\frac{\Gamma\turn t_2}
{\Gamma -\{t_1\} \turn t_1 \imp t_2}
\]
\begin{itemize}
\item Where $\Gamma -\{t_1\}$ is the set subtraction of $\{t_1\}$
from $\Gamma$.
\end{itemize}

\subsubsection*{Modus Ponens [{\small\tt
MP}]}\index{MP@\ml{MP}}\index{Modus Ponens, in HOL logic@Modus Ponens, in \HOL{} logic!abstract form of}
\[
\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 {\it
axioms\/}\index{axioms!as inference rules} 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~\ref{INIT} and
the definitions of the extra logical constants they involve are given in
Section~\ref{LOG}.

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\index{LCF@\LCF}\ logic
\PPL\index{PPlambda (same as PPLAMBDA), of LCF system@\ml{PP}$\lambda$ (same as \ml{PPLAMBDA}), of \ml{LCF} system}, since \HOL{} was
implemented by modifying the \LCF\ system. In particular, the
substitution\index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!implementation of} rule {\small\tt 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.

\subsection{Soundness theorem}
\index{soundness!of HOL deductive system@of \HOL{} deductive system}
\label{soundness}

\index{inference rules, of HOL logic@inference rules, of \HOL{} logic!formal semantics of}
\emph{The rules of the \HOL{} deductive system are {\em sound} for
  the notion of satisfaction defined in Section~\ref{sequents}: for
  any instance of the rules of inference, if a (standard) model
  satisfies the hypotheses of the rule it also satisfies the
  conclusion.}

\medskip

\noindent{\bf 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~\ref{term-substitution} are needed for rules
\ml{BETA\_CONV}, \ml{SUBST} and
\ml{INST\_TYPE}\index{INST_TYPE@\ml{INST\_TYPE}}.\footnote{Note in
  particular that the second restriction on \ml{INST\_TYPE} enables
  the result on the semantics of substituting types for type variables
  in terms to be applied.}  The fact that $=$ and $\imp$ are
interpreted standardly (as in Section~\ref{standard-signatures}) is
needed for rules \ml{REFL}\index{REFL@\ml{REFL}},
\ml{BETA\_CONV}\index{BETA_CONV@\ml{BETA\_CONV}},
\ml{SUBST}\index{SUBST@\ml{SUBST}}, \ml{ABS}\index{ABS@\ml{ABS}},
\ml{DISCH}\index{DISCH@\ml{DISCH}} and \ml{MP}\index{MP@\ml{MP}}.

\section{\HOL{} Theories}
\label{theories}

A \HOL{} {\it theory\/}\index{theories, in HOL logic@theories, in \HOL{} logic!abstract form of} ${\cal T}$ is a $4$-tuple:
\begin{eqnarray*}
{\cal T} & = & \langle{\sf Struc}_{\cal T},{\sf Sig}_{\cal T},
               {\sf Axioms}_{\cal T},{\sf Theorems}_{\cal T}\rangle
\end{eqnarray*}
where
\begin{myenumerate}

\item ${\sf Struc}_{\cal T}$ is a type structure\index{type structures, of HOL theories@type structures, of \HOL{} theories}  called the type
structure of ${\cal T}$;

\item ${\sf Sig}_{\cal T}$ is a signature\index{signatures, of HOL logic@signatures, of \HOL{} logic!of HOL theories@of \HOL{} theories}
over ${\sf Struc}_{\cal T}$ called the signature of ${\cal T}$;

\item ${\sf Axioms}_{\cal T}$ is a set of sequents over ${\sf Sig}_{\cal T}$
called the  axioms\index{axioms, in a HOL theory@axioms, in a \HOL{} theory}
 of  ${\cal T}$;

\item ${\sf Theorems}_{\cal T}$ is a set of sequents over
${\sf Sig}_{\cal T}$ called the theorems
%
\index{theorems, in HOL logic@theorems, in \HOL{} logic!abstract form of}
%
of ${\cal T}$, with
the property that every member follows from ${\sf Axioms}_{\cal T}$ by
the \HOL{} deductive system.

\end{myenumerate}

The sets ${\sf Types}_{\cal T}$ and ${\sf 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}$, \ie:
\begin{eqnarray*}
{\sf Types}_{\cal T} & = & {\sf Types}_{{\sf Struc}_{\cal T}}\\
{\sf Terms}_{\cal T} & = & {\sf Terms}_{{\sf Sig}_{\cal T}}
\end{eqnarray*}
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~\ref{soundness}, it follows that $M$ also
satisfies any sequents in the set of given  theorems, ${\sf
Theorems}_{\cal T}$.

\subsection{The theory {\tt MIN}}
\label{sec:min-thy}

The {\it minimal theory\/}\index{MIN@\ml{MIN}}\index{minimal theory, of HOL logic@minimal theory, of \HOL{} logic} \theory{MIN} is defined by:
\[
\theory{MIN} =
\langle\{(\bool,0),\ (\ind,0)\},\
 \{\imp_{\bool\fun\bool\fun\bool},
=_{\alpha\fun\alpha\fun\bool},
\hilbert_{(\alpha\fun\bool)\fun\alpha}\},\
\{\},\ \{\}\rangle
\]
Since the theory \theory{MIN} has a signature consisting only of
standard items and has no axioms, it possesses a unique standard model,
which will be denoted {\em Min}.

Although the theory \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 {\em Min}.

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

\subsection{The theory {\tt LOG}}
\index{LOG@\ml{LOG}}
\label{LOG}

The theory \theory{LOG} has the same type
structure as \theory{MIN}. Its signature contains the constants in
\theory{MIN} and the following constants:
\[
\T_\ty{bool}
\index{T@\holtxt{T}!abstract form of}
\index{truth values, in HOL logic@truth values, in \HOL{} logic!abstract form of}
\]
\[
\forall_{(\alpha\fun\ty{bool})\fun\ty{bool}}
\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!abstract form of}
\]
\[
\exists_{(\alpha\fun\ty{bool})\fun\ty{bool}}
\index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abstract form of}
\]
\[
\F_\ty{bool}
\index{F@\holtxt{F}!abstract form of}
\]
\[
\neg_{\ty{bool}\fun\ty{bool}}
\index{negation, in HOL logic@negation, in \HOL{} logic!abstract form of}
\]
\[
\wedge_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}
\index{conjunction, in HOL logic@conjunction, in \HOL{} logic!abstract form of}
\]
\[
\vee_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}
\index{disjunction, in HOL logic@disjunction, in \HOL{} logic!abstract form of}
\]
\[
\OneOne_{(\alpha\fun\beta)\fun\ty\bool}
\index{one-to-one predicate, in HOL logic@one-to-one predicate, in \HOL{} logic!abstract form of}
\]
\[
\Onto_{(\alpha\fun\beta)\fun\ty\bool}
\index{onto predicate, in HOL logic@onto predicate, in \HOL{} logic!abstract form of}
\]
\[
\TyDef_{(\alpha\fun\ty{bool})\fun(\beta\fun\alpha)\fun\ty{bool}}
\]
The following special notation is used in connection with these constants:
\begin{center}
\index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abbreviation for multiple}
\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!abbreviation for multiple}
\begin{tabular}{|l|l|}\hline
{\rm Notation} & {\rm Meaning}\\ \hline $\uquant{x_{\sigma}}t$ &
$\forall(\lambda x_{\sigma}.\ t)$\\ \hline $\uquant{x_1\ x_2\ \cdots\
x_n}t$ & $\uquant{x_1}(\uquant{x_2} \cdots\ (\uquant{x_n}t)
\ \cdots\ )$\\ \hline
$\equant{x_{\sigma}}t$
  & $\exists(\lambda x_{\sigma}.\ t)$\\ \hline
$\equant{x_1\ x_2\ \cdots\ x_n}t$
  & $\equant{x_1}(\equant{x_2} \cdots\ (\equant{x_n}t)
\ \cdots\ )$\\ \hline
$t_1\ \wedge\ t_2$  & $\wedge\ t_1\ t_2$\\ \hline
$t_1\ \vee\ t_2$  & $\vee\ t_1\ t_2$\\ \hline
\end{tabular}\end{center}

The axioms of the theory \theory{LOG} consist of the following
sequents:
\[
\begin{array}{l}

\turn \T       =  ((\lquant{x_{\ty{bool}}}x) =
               (\lquant{x_{\ty{bool}}}x))    \\
\turn \forall  =  \lquant{P_{\alpha\fun\ty{bool}}}\ P =
                    (\lquant{x}\T ) \\
\turn \exists  =  \lquant{P_{\alpha\fun\ty{bool}}}\
                    P({\hilbert}\ P) \\
\turn \F       =  \uquant{b_{\ty{bool}}}\ b  \\
\turn \neg    =  \lquant{b}\ b \imp \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  =   \begin{array}[t]{l}
                  \lambda P_{\alpha\fun\ty{bool}}\
                  rep_{\beta\fun\alpha}.
                  \OneOne\ rep\ \ \wedge{}\\
                  \quad(\uquant{x}P\ x \ =\ (\equant{y} x = rep\ y))
                  \end{array}
\end{array}
\]
Finally, as for the theory \theory{MIN}, the set ${\sf
Theorems}_{\theory{LOG}}$ is taken to be empty.

Note that the axioms of the theory \theory{LOG} are essentially {\em
definitions\/} of the new constants of \theory{LOG} as terms in the
original theory \theory{MIN}. (The mechanism for making such
extensions of theories by definitions of new constants will be set out
in general in Section~\ref{defs}.) 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~\ref{INIT}), amongst other things. The last axiom defines a
constant used for type definitions (see Section~\ref{tydefs}).

The unique standard model {\em Min\/} of \theory{MIN} gives rise to a
unique standard model of
\theory{LOG}\index{LOG@\ml{LOG}!formal semantics of}. This is
because, given the semantics of terms set out in
Section~\ref{semantics of terms}, to satisfy the above equations one
is forced to interpret the new constants in the following way:
\index{axioms!formal semantics of HOL logic's@formal semantics of \HOL{} logic's|(}
\begin{itemize}

\item $\den{\T_{\bool}}\index{T@\holtxt{T}!formal semantics of} = 1 \in \two$

\item \index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!formal semantics of}
$\den{\forall_{(\alpha\fun\bool)\fun\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 & \mbox{if
$f^{-1}\{1\}=X$} \\ 0 & \mbox{otherwise} \end{array} \right.
\]
\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!formal semantics of}

\item \index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!formal semantics of}
$\den{\exists_{(\alpha\fun\bool)\fun\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 & \mbox{if $f^{-1}\{1\}\not=\emptyset$} \\
                                   0 & \mbox{otherwise}
                                  \end{array}
                          \right. \]

\item $\den{\F_{\bool}} = 0 \in \two$\index{F@\holtxt{F}!formal semantics of}

\item $\den{\neg_{\bool\fun\bool}}\in\two\fun\two$ sends $b\in\two$ to
 \[ \den{\neg}(b) = \left\{ \begin{array}{ll}
                             1 & \mbox{if $b=0$} \\
                             0 & \mbox{otherwise}
                            \end{array}
                    \right. \]\index{negation, in HOL logic@negation, in \HOL{} logic!formal semantics of}

\item $\den{\wedge_{\bool\fun\bool\fun\bool}}\in\two\fun\two\fun\two$ sends
$b,b'\in\two$ to
 \[ \den{\wedge}(b)(b') = \left\{ \begin{array}{ll}
                                   1 & \mbox{if $b=1=b'$} \\
                                    0 & \mbox{otherwise}
                                  \end{array}
                           \right. \]\index{conjunction, in HOL logic@conjunction, in \HOL{} logic!formal semantics of}

\item $\den{\vee_{\bool\fun\bool\fun\bool}}\in\two\fun\two\fun\two$ sends
$b,b'\in\two$ to
 \[ \den{\vee}(b)(b') = \left\{ \begin{array}{ll}
                                 0 & \mbox{if $b=0=b'$} \\
                                 1 & \mbox{otherwise}
                                \end{array}
                        \right. \]\index{disjunction, in HOL logic@disjunction, in \HOL{} logic!formal semantics of}

\item $\den{\OneOne_{(\alpha\fun\beta)\fun\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 & \mbox{if $f(x)=f(x')$
                                               for some $x\not=x'$ in $X$} \\
                                     1 & \mbox{otherwise}
                                    \end{array}
                            \right. \]\index{one-to-one predicate, in HOL logic@one-to-one predicate, in \HOL{} logic!formal semantics of}

\item $\den{\Onto_{(\alpha\fun\beta)\fun\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 & \mbox{if $\{f(x):x\in X\}=Y$} \\
                                   0 & \mbox{otherwise}
                                  \end{array}
                           \right. \]\index{onto predicate, in HOL logic@onto predicate, in \HOL{} logic!formal semantics of}

\item $\den{\TyDef_{(\alpha\fun\bool)\fun(\beta\fun\alpha)\fun\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 & \mbox{if
                                            $\den{\OneOne}(Y,X)(g)=1$}\\
                                          & \mbox{and $f^{-1}\{1\}=
                                            \{g(y) : y\in Y\}$} \\
                                        0 & \mbox{otherwise.}
                                       \end{array}
                               \right.
\]
\end{itemize}
\index{axioms!formal semantics of HOL logic's@formal semantics of \HOL{} logic's|)}
Since these definitions were obtained by applying the semantics of
terms to the left hand sides of the equations which form the axioms of
\theory{LOG}, these axioms are satisfied and one obtains a model of
the theory \theory{LOG}.


\subsection{The theory {\tt INIT}}
\label{INIT}

The theory \theory{INIT}\index{INIT@\ml{INIT}!abstract form of} is
obtained by adding the following four axioms\index{axioms!abstract form of HOL logic's@abstract form of \HOL{} logic's} to the theory
\theory{LOG}.
\[
\index{BOOL_CASES_AX@\ml{BOOL\_CASES\_AX}!abstract form of}
\index{ETA_AX@\ml{ETA\_AX}!abstract form of}
\index{SELECT_AX@\ml{SELECT\_AX}!abstract form of}
\index{INFINITY_AX@\ml{INFINITY\_AX}!abstract form of}
\index{choice axiom!abstract form of}
\index{axiom of infinity!abstract form of}
\begin{array}{@{}l@{\qquad}l}
\mbox{\small\tt BOOL\_CASES\_AX}&\vdash \uquant{b} (b = \T ) \vee (b = \F )\\
 \\
\mbox{\small\tt ETA\_AX}&
\vdash \uquant{f_{\alpha\fun\beta}}(\lquant{x}f\ x) = f\\
 \\
\mbox{\small\tt SELECT\_AX}&
\vdash \uquant{P_{\alpha\fun\ty{bool}}\ x} P\ x \imp
P({\hilbert}\ P)\\
  \\
\mbox{\small\tt INFINITY\_AX}&
\vdash \equant{f_{\ind\fun \ind}} \OneOne \ f \conj \neg(\Onto \ f)\\
\end{array}
\]

The unique standard model of \theory{LOG} satisfies these four axioms
and hence is the unique standard model of the theory
\theory{INIT}.\index{INIT@\ml{INIT}!formal semantics of} (For axiom
{\small\tt SELECT\_AX} one needs to use the definition of
$\den{\hilbert}$ given in Section~\ref{standard-signatures}; for axiom
{\small\tt INFINITY\_AX} one needs the fact that $\den{\ind}=\inds$ is
an infinite set.)

The theory \theory{INIT} is the initial theory\index{initial theory,
  of HOL logic@initial theory, of \HOL{} logic!abstract form of} of the
\HOL{} logic. A theory which extends \theory{INIT} will be called a
{\em standard theory}\index{standard theory}.

\subsection{Implementing theories \texttt{LOG} and \texttt{INIT}}
\label{sec:implementing-log-init}

The implementation combines the theories \theory{LOG} and
\theory{INIT} into a theory \theoryimp{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 \theoryimp{bool} theory, see \DESCRIPTION.

\subsection{Consistency}
\label{consistency}

A (standard) theory is {\em consistent\/}\index{consistent theory} 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\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~\ref{soundness}, any sequent that can be derived from the
theory's axioms will be satisfied by the model, whereas the sequent
$\turn\F$ is never satisfied in any standard model.  So in particular,
the initial theory \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 {\em
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\"odel ensures that there
are sequents which are satisfied in all standard models (\ie\ which are
`true'), but which are not provable in the \HOL{} logic.





\section{Extensions of theories}
\index{extension, of HOL logic@extension, of \HOL{} logic!abstract form of}
\label{extensions}

A theory ${\cal T}'$ is said to be an {\em
extension\/}\index{extension, of theory} of a theory ${\cal T}$ if:
\begin{myenumerate}
\item ${\sf Struc}_{{\cal T}}\subseteq{\sf Struc}_{{\cal T}'}$.
\item ${\sf Sig}_{{\cal T}}\subseteq{\sf Sig}_{{\cal T}'}$.
\item ${\sf Axioms}_{{\cal T}}\subseteq{\sf Axioms}_{{\cal T}'}$.
\item ${\sf Theorems}_{{\cal T}}\subseteq{\sf Theorems}_{{\cal T}'}$.
\end{myenumerate}
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 ${\sf Struc}_{\cal T}$ or ${\sf Sig}_{\cal T}$. Denoting this model
by $M$, one has for all $\sigma\in{\sf Types}_{\cal T}$, $t\in{\sf
Terms}_{\cal T}$ and for all suitable contexts that
\begin{eqnarray*}
\den{\alpha\!s.\sigma}_{M}   & = & \den{\alpha\!s.\sigma}_{M'} \\
\den{\alpha\!s,\!x\!s.t}_{M} & = & \den{\alpha\!s,\!x\!s.t}_{M'}.
\end{eqnarray*}
Consequently if $(\Gamma,t)$ is a sequent over ${\sf Sig}_{\cal T}$
(and hence also over ${\sf Sig}_{{\cal T}'}$), then $\Gamma
\models_{M} t$ if and only if $\Gamma \models_{M'} t$. Since ${\sf
Axioms}_{\cal T}\subseteq{\sf 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 {\em restriction}\index{restrictions, of models} of the
model $M'$ of the theory ${\cal T}'$ to the subtheory $\cal T$.

\bigskip

There are two main mechanisms for making extensions of theories in \HOL:
\begin{itemize}

\item Extension by a constant specification   (see Section~\ref{specs}).

\item Extension by a type specification (see
Section~\ref{tyspecs}).\footnote{This theory extension mechanism is
not implemented in the \HOL{}4 system.}

\end{itemize}
The first mechanism allows `loose specification' of constants (as in
the {\bf Z} notation~\cite{Z}, 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:
\begin{itemize}

\item Extension by a constant definition (see Section~\ref{defs}).

\item Extension by a type definition (see Section~\ref{tydefs}).

\end{itemize}
These mechanisms are described in the following sections. They all
produce {\it 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
\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\index{axioms!dispensibility of adding}, 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.\footnote{See page 71 of Russell's book {\sl
Introduction to Mathematical Philosophy\/}.} 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.





\subsection{Extension by constant definition}
\index{extension, of HOL logic@extension, of \HOL{} logic!by constant definition|(}
\label{defs}

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

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

\item
$t_{\sigma}$ a closed term in ${\sf Terms}_{\Sigma_{\Omega}}$;

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

\end{myenumerate}

Given a theory $\cal T$ and such a constant definition over ${\sf
Sig}_{\cal T}$, then the {\em definitional extension\/}\index{constant definition extension, of HOL logic@constant definition extension, of \HOL{} logic!abstract form of} of ${\cal T}$
by $\con{c}_{\sigma}=t_{\sigma}$ is the theory ${\cal T}{+_{\it
def}}\langle
\con{c}_{\sigma}=t_{\sigma}\rangle$ defined by:
\[
{\cal T}{+_{\it def}}\langle
\con{c}_{\sigma}=t_{\sigma}\rangle\  =\ \langle
\begin{array}[t]{l}
{\sf Struc}_{\cal T},\
{\sf Sig}_{\cal T}\cup\{(\con{c},\sigma)\},\\
{\sf Axioms}_{\cal T}\cup\{
\con{c}_{\sigma}=t_{\sigma} \},\
{\sf Theorems}_{\cal T}\rangle
\end{array}
\]

Note that the mechanism of extension by constant definition has
already been used implicitly in forming the theory \theory{LOG} from
the theory \theory{MIN} in Section~\ref{LOG}. Thus with the notation
of this section one has
\[
\theory{LOG}\; =\; \theory{MIN}\;\begin{array}[t]{@{}l}
   {+_{\it def}} \langle \T\index{T@\holtxt{T}!abstract form of}\index{truth values, in HOL logic@truth values, in \HOL{} logic!abstract form of} \ =\
     ((\lquant{x_{\ty{bool}}}x) = (\lquant{x_{\ty{bool}}}x))\rangle\\
   {+_{\it def}}\langle {\forall}\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!abstract form of}\ =\ \lquant{P_{\alpha\fun\ty{bool}}}\ P =
     (\lquant{x}\T )\rangle\\
   {+_{\it def}}\langle {\exists}\index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abstract form of}\ =\
     \lquant{P_{\alpha\fun\ty{bool}}}\ P({\hilbert}\ P)\rangle\\
   {+_{\it def}}\langle \F\index{F@\holtxt{F}!abstract form of}
 \ =\ \uquant{b_{\ty{bool}}}\ b\rangle\\
   {+_{\it def}}\langle \neg\ =\ \lquant{b}\ b \imp \F \rangle\index{negation, in HOL logic@negation, in \HOL{} logic!abstract form of}\\
   {+_{\it def}}\langle {\wedge}\index{conjunction, in HOL logic@conjunction, in \HOL{} logic!abstract form of}\ =\ \lquant{b_1\ b_2}\uquant{b}
     (b_1\imp (b_2 \imp b)) \imp b\rangle\\
   {+_{\it def}}\langle {\vee}\index{disjunction, in HOL logic@disjunction, in \HOL{} logic!abstract form of}\ =\ \lquant{b_1\ b_2}\uquant{b}
     (b_1 \imp b)\imp ((b_2 \imp b) \imp b)\rangle\\
   {+_{\it 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\index{one-to-one predicate, in HOL logic@one-to-one predicate, in \HOL{} logic!abstract form of}\\
   {+_{\it def}}\langle\Onto \  =\ \lquant{f_{\alpha\fun\beta}}\index{onto predicate, in HOL logic@onto predicate, in \HOL{} logic!abstract form of}
     \uquant{y}\equant{x} y = f\ x\rangle\\
   {+_{\it def}}\langle\TyDef \  =\
        \begin{array}[t]{@{}l}
          \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}\end{array}
\]

If $\cal T$ possesses a standard model then so does the extension
${\cal T}{+_{\it def}}\langle\con{c}_{\sigma}=t_{\sigma}\rangle$. This
will be proved as a corollary of the corresponding result in
Section~\ref{specs} 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 {\em standard\/}
theories in the sense of section~\ref{INIT}, since although
existential quantification is not needed for constant definitions, it
is needed to state the mechanism of constant specification.)

\medskip

\noindent{\bf 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 $\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 $\theory{INIT}$, and hence $\con{c}_\ty{bool}=\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 $\theory{INIT}$, and hence $\con{c}_\ty{bool}=\F$ is
also provable in the extended theory. Combining these theorems, one
has that $\T=\F$, \ie\ $\F$ is provable in the extended theory.
\index{extension, of HOL logic@extension, of \HOL{} logic!by constant definition|)}

\subsection{Extension by constant specification}
\index{extension, of HOL logic@extension, of \HOL{} logic!by constant specification|(}
\label{specs}

Constant specifications\index{constant specification extension, of HOL logic@constant specification extension, of \HOL{} logic!abstract form
of} 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=\T$ and $\con{b}_2=\F$, or $\con{b}_1=\F$ and
$\con{b}_2=\T$.  To ensure that such specifications are
consistent\index{consistency, of HOL logic@consistency, of \HOL{} logic!under constant specification}, 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~\ref{constants} below.

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

\medskip
\noindent{\bf Data}
\[
\langle(\con{c}_1,\ldots,\con{c}_n),
\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}\rangle
\]

\noindent{\bf Conditions}
\begin{myenumerate}

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

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

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

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

\end{myenumerate}
The extension of a standard theory ${\cal T}$ by such a constant
specification is denoted by
\[
{\cal T}{+_{\it 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}[t]{@{}l}
{\sf Struc}_{\cal T},\\
{\sf Sig}_{\cal T} \cup
\{{\con{c}_1}_{\sigma_1}, \ldots,
{\con{c}_n}_{\sigma_n}\},\\
{\sf Axioms}_{\cal T}\cup
\{ t[\con{c}_1,\ldots,\con{c}_n/x_1,\ldots,x_n] \},\\
{\sf Theorems}_{\cal T}
\rangle
\end{array}
\]

\noindent{\bf Proposition\ }{\em
The theory ${\cal
T}{+_{\it 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.}

\medskip

\noindent{\bf Proof\ }
Suppose $M$ is a standard model of ${\cal T}$.  Let
$\alpha\!s=\alpha_{1},\ldots,\alpha_{m}$ be the list of distinct type
variables occurring in the formula $t$. Then $\alpha\!s,\!x\!s.t$ is a
term-in-context, where $x\!s=x_{1},\ldots,x_{n}$. (Change any bound
variables in $t$ to make them distinct from $x\!s$ if necessary.)
Interpreting this term-in-context in the model $M$ yields
\[
\den{\alpha\!s,\!x\!s.t}_{M} \in \prod_{X\!s\in{\cal U}^{m}}
\left(\prod_{i=1}^{n}\den{\alpha\!s.\sigma_{i}}_{M}(X\!s)\right)
\fun \two
\]
Now $\equant{x\!s}t$ is in ${\sf Theorems}_{\cal T}$ and hence by the
Soundness Theorem \ref{soundness}\index{consistency, of HOL logic@consistency, of \HOL{} logic!under constant specification} this
sequent is satisfied by $M$. Using the semantics of $\exists$ given in
Section~\ref{LOG}, this means that for all $X\!s\in{\cal
U}^{m}$ the set
\[
S(X\!s) = \{y\!s\in\den{\alpha\!s.\sigma_{1}}_{M}(X\!s) \times\cdots\times
          \den{\alpha\!s.\sigma_{n}}_{M}(X\!s)\; : \;
          \den{\alpha\!s,\!x\!s.t}_{M}(X\!s)(y\!s)=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
{\bf Sub} and {\bf 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}(X\!s),\ldots,s_{n}(X\!s)) =
\ch(S(X\!s)) \in \prod_{i=1}^{n}\den{\alpha\!s.\sigma_{i}}_{M}(X\!s)
\]
at which  $\den{\alpha\!s,\!x\!s.t}_{M}(X\!s)$ takes the value $1$. Extend
$M$ to a model $M'$ of the signature of ${\cal
T}{+_{\it 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_{X\!s\in{\cal U}^{m}}\den{\sigma_{i}}_{M}(X\!s) .
\]
Note that the Condition (iii) in the definition of a constant
specification ensures that $\alpha\!s$ is the canonical context of each
type $\sigma_{i}$, so that
$\den{\sigma_{i}}=\den{\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}{+_{\it 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~\ref{extensions}, one has that
$\den{\alpha\!s,\!x\!s.t}_{M'} = \den{\alpha\!s,\!x\!s.t}_{M}$. Hence by
definition of the $s_{i}$, for all $X\!s\in{\cal U}^{m}$
\[
\den{\alpha\!s,\!x\!s.t}_{M'}(X\!s)(s_{1}(X\!s),\ldots,s_{n}(X\!s)) = 1
\]
Then using Lemma~4 in Section
\ref{term-substitution} on the semantics of substitution together with
the definition of $\den{\con{c}_{i}}_{M'}$, one finally obtains that
for all $X\!s\in{\cal U}^{m}$
\[
\den{t[\con{c}_{1},\ldots,\con{c}_{n}/x_{1},\ldots,x_{n}]}_{M'}(X\!s)=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}{+_{\it
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.

\medskip

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}{+_{\it
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}{+_{\it 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}{+_{\it 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}{+_{\it 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.
\index{extension, of HOL logic@extension, of \HOL{} logic!by constant specification|)}

\subsection{Remarks about constants in \HOL{}}
\label{constants}

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~\ref{defs}. 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})=\T$ and
$\con{c}_\ty{bool}(\ty{bool})=\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},\alpha\!s.\sigma)$ where now $\alpha\!s.\sigma$ is a
type-in-context and the list $\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(\alpha\!s)$, and more generally to
constant terms $\con{c}_{\sigma'}(\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 $\tau\!s$ for $\alpha\!s$). This new syntax of polymorphic
constants is comparable to the existing syntax of compound types (see
section~\ref{types}): an $n$-ary type operator $\textsl{op}$ gives rise to a
compound type $(\alpha_1,\ldots,\alpha_n){\textsl{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 $\alpha\!s$ in $(\con{c},\alpha\!s.\sigma)$ is actually the
{\em canonical\/} context of $\sigma$, \ie\ contains exactly the type
variables of $\sigma$.  For then one can apply Lemma~1 of
Section~\ref{instances-and-substitution} to deduce that the
polymorphic constant $\con{c}_{\sigma'}(\tau\!s)$ can be abbreviated
to the ordinary constant $\con{c}_{\sigma'}$ without ambiguity---the
missing information $\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~\ref{defs} and \ref{specs} 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.


\subsection{Extension by type definition}
\index{extension, of HOL logic@extension, of \HOL{} logic!by type definition|(}
\index{representing types, in HOL logic@representing types, in \HOL{} logic!abstract form of|(}
\label{tydefs}

Every (monomorphic) type $\sigma$ in the initial theory \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
\theory{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\index{extension, of HOL logic@extension, of \HOL{} logic!by type definition} in \HOL{} by introducing a new type
constant and asserting an axiom that characterizes it as denoting a
set in bijection (\ie\ one-to-one correspondence) with a non-empty
subset of an existing type (called the {\it representing type\/}).
For example, the type \ml{num} is defined to be equal to a countable
subset of the type \ml{ind}, which is guaranteed to exist by the axiom
{\small\tt INFINITY\_AX} (see Section~\ref{INIT}).

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 (\ie\ 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\index{consistency, of HOL logic@consistency, of \HOL{} logic!under type definition} 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, \ie\ $\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$ {\em 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:
\begin{enumerate}
\item Specifying an existing type.
\item Specifying a subset of this type.
\item Proving that this subset is non-empty.
\item Specifying that the new type is isomorphic to this subset.
\end{enumerate}

\noindent In more detail,
defining a new type $(\alpha_1,\ldots,\alpha_n)\ty{op}$ consists in:
\begin{enumerate}
\item
Specifying a type-in-context, $\alpha_1,\ldots,\alpha_n.\sigma$ say.
The type
$\sigma$ is called the {\it representing type\/}, and the type
$(\alpha_1,\ldots,\alpha_n)\ty{op}$ is intended to be isomorphic to a
subset of $\sigma$.

\item
Specifying a closed term-in-context, $\alpha_1,\ldots,\alpha_n,.p$
say, of type $\sigma\fun\bool$. The term $p$ is called the {\it
characteristic function\/}\index{characteristic function, of type definitions}.  This defines the subset of $\sigma$ to which
$(\alpha_1,\ldots,\alpha_n)\ty{op}$ is to be isomorphic.\footnote{The
reason for restricting $p$ to be closed, \ie\ to have no free
variables, is that otherwise for consistency the defined type operator
would have to {\em depend\/} upon (\ie\ be a function of) those
variables. Such dependent types are not (yet!) a part of the \HOL{} system.}

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

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

\end{enumerate}

To make this formal, the theory \theory{LOG} provides
the polymorphic constant \TyDef\ defined in Section~\ref{LOG}.
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 {\em
type definition\/}\index{type definitions, in HOL logic@type definitions, in \HOL{} logic!abstract structure of} for a theory ${\cal
T}$ is given by

\medskip

\noindent{\bf Data}
\[
\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\ \sigma,\
p_{\sigma\fun\ty{bool}}\rangle
\]

\noindent{\bf Conditions}

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

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

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

\item
$\equant{x_{\sigma}}p\ x \ \in\ {\sf Theorems}_{\cal T}$.
\end{myenumerate}

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}[t]{@{}l}
{\sf Struc}_{\cal T}\cup\{(\ty{op},n)\},\\
  {\sf Sig}_{\cal T},\\
  {\sf Axioms}_{\cal T}\cup\{
\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}
\fun\sigma}}\TyDef\ p\ f\},\\
  {\sf Theorems}_{\cal T}\rangle\\
\end{array}
\]

\medskip

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

\medskip

Instead of giving a direct proof of this result, it will be deduced as
a corollary of the corresponding proposition in the next section.
\index{extension, of HOL logic@extension, of \HOL{} logic!by type definition|)}
\index{representing types, in HOL logic@representing types, in \HOL{} logic!abstract form of|)}


\subsection{Extension by type specification}
\index{extension, of HOL logic@extension, of \HOL{} logic!by type specification|(}
\label{tyspecs}
\noindent
(\textbf{Note:} This theory extension mechanism is \emph{not}
implemented in the HOL4 system. It was proposed by T.~Melham and
refines a suggestion from R.~Jones and R.~Arthan.)

\smallskip
\noindent 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 \theory{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
$\theory{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.\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\footnote{yet!} 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}}{\sf Type\_Definition}\ 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, \ie\ 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.\footnote{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.} Thus a {\em type
specification\/}\index{type specification} for a theory $\cal T$ is
given by

\medskip

\noindent{\bf Data}
\[
\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q\rangle
\]

\noindent{\bf Conditions}

\begin{myenumerate}
\item
$(\ty{op},n)$ is a type constant that is not in
${\sf Struc}_{\cal T}$.

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

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

\item $\alpha$ is a type variable distinct from those in
$\alpha\!s$.

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

\item $q$  is a closed formula in ${\sf Terms}_{\cal T}$.

\item The sequents
\begin{eqnarray*}
(\Gamma & , & \equant{x_\sigma}p\ x )\\
(\Gamma & , & (\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\
                 p\ f)\ \imp\ q )
\end{eqnarray*}
are in ${\sf Theorems}_{\cal T}$.

\end{myenumerate}
The extension of a standard theory $\cal T$ by such a type
specification is denoted
\[
{\cal T}{+_{\it 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}[t]{@{}l}
{\sf Struc}_{\cal T}\cup\{(\ty{op},n)\},\\
  {\sf Sig}_{\cal T},\\
  {\sf Axioms}_{\cal
  T}\cup\{(\Gamma , q[(\alpha_1,\ldots,\alpha_n)\ty{op}/\alpha])\},\\
  {\sf Theorems}_{\cal T}\rangle
\end{array}
\]

\noindent{\bf Example\ } To carry out the extension of \theory{INIT}
mentioned at the start of this section, one forms
\[
\theory{INIT}{+_{\it tyspec}} \langle
()\ty{one},\ty{bool},p,\alpha,\emptyset,q\rangle
\]
where $p$ is the term $\lquant{b_\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 \theory{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 \theory{INIT}. The first sequent says
that $p$ defines an inhabited subset of $\bool$, which is certainly
the case since $\T$ witnesses this fact. The second sequent says in
effect that any type $\alpha$ that is in bijection with the subset of
$\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 \theory{INIT} is left as an exercise.

\medskip

\noindent{\bf Proposition\ }{\em
The theory ${\cal T}{+_{\it 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.}

\medskip

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

Suppose $M$ is a standard model of ${\cal T}$. Since $\alpha\!s,.p$ is
a term-in-context of type $\sigma\fun\ty{bool}$, interpreting it in
$M$ yields
\[
\den{\alpha\!s,.p}_{M}
\in \prod_{X\!s\in{\cal U}^{n}}\den{\alpha\!s.\sigma\fun\ty{bool}}_M(X\!s)
= \prod_{X\!s\in{\cal U}^{n}}
   \den{\alpha\!s.\sigma}_M(X\!s)\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
$\T$ if $\Gamma$ is empty.) By assumption on $\alpha\!s'$ and by
Condition~(iv), $\alpha\!s,\alpha\!s',.\gamma$ is a term-in-context.\footnote{Note the two commas in $\alpha\!s,\alpha\!s',.\gamma$. The first separates the two lists of type variables; the second splits type variables from term variables.}
Interpreting it in $M$ yields
\[
\den{\alpha\!s,\alpha\!s',.\gamma}_{M}
\in \prod_{(X\!s,X\!s')\in
{\cal U}^{n+m}}\den{\alpha\!s,\alpha\!s'.\ty{bool}}_M(X\!s,X\!s')
={\cal U}^{n+m}\fun\two
\]

Now $(\gamma,\equant{x_{\sigma}}p\ x)$ is in ${\sf Theorems}_{\cal T}$
and hence by the Soundness Theorem~\ref{soundness} this sequent is
satisfied by $M$. Using the semantics of $\exists$ given in
Section~\ref{LOG} and the definition of satisfaction of a sequent from
Section~\ref{sequents}, this means that for all $(X\!s,X\!s')\in{\cal U}^{n+m}$
if $\den{\alpha\!s,\alpha\!s',.\gamma}_M(X\!s,X\!s')=1$, then
the set
\[
\{y\in\den{\alpha\!s.\sigma}_{M}\: :\: \den{\alpha\!s,.p}(X\!s)(y)=1\}
\]
is non-empty. (This uses the fact that $p$ does not involve
the type variables $\alpha\!s'$, so that by Lemma~4 in
Section~\ref{term-substitution}
$\den{\alpha\!s,\alpha\!s',.p}_M(X\!s,X\!s')=\den{\alpha\!s,.p}_M(X\!s)$.)
Since it is also a subset of a set in $\cal U$, it
follows by property {\bf Sub} of the universe that this set is an element of
$\cal U$. So defining
\[
S(X\!s) = \left\{\hspace{-1mm}
\begin{array}{ll}
\{y\in\den{\alpha\!s.\sigma}_{M} : \den{\alpha\!s,.p}(X\!s)(y)=1\}
  & \mbox{\rm if $\den{\alpha\!s,.\gamma}_M(X\!s,X\!s')=1$, some $X\!s'$}\\
1 & \mbox{\rm 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 $X\!s\in{\cal U}^{n}$ define $i_{X\!s}$ to be the inclusion
function for the subset $S(X\!s)\subseteq\den{\alpha\!s.\sigma}_{M}$
if $\den{\alpha\!s,\alpha\!s',.\gamma}_M(X\!s,X\!s')=1$ for some
$X\!s'$, and otherwise to be the function
$1\fun\den{\alpha\!s.\sigma}_{M}$ sending $0\in 1$ to
$\ch(\den{\alpha\!s.\sigma}_{M})$. Then
$i_{X\!s}\in(S(X\!s)\fun\den{\alpha\!s.\sigma}_{M'}(X\!s))$ because
$\den{\alpha\!s.\sigma}_{M'}=\den{\alpha\!s.\sigma}_M$. Using the
semantics of $\TyDef$ given in Section~\ref{LOG}, one has that for any
$(X\!s,X\!s')\in{\cal U}^{n+m}$, if
$\den{\alpha\!s,\alpha\!s',.\gamma}_{M'}(X\!s,X\!s')=1$ then
\[
\den{\TyDef}_{M'}(\den{\alpha\!s.\sigma}_{M'} ,
   S(X\!s))(\den{\alpha\!s,.p}_{M'})(i_{X\!s}) = 1.
\]
Thus $M'$ satisfies the sequent
\[
(\gamma\ ,\ \equant{f_{(\alpha\!s)\ty{op}\fun\sigma}}\TyDef\ p\ f).
\]
But since the sequent $(\gamma,(\equant{f_{\alpha\fun\sigma}}{\sf
Type\_Definition}\ p\ f)\ \imp\ q )$ is in ${\sf 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 $(\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_{(\alpha\!s)\ty{op}\fun\sigma}}\TyDef\ p\ f)\imp
q[(\alpha\!s)\ty{op}/\alpha]).
\]
Applying Modus Ponens, one concludes that $M'$ satisfies
$(\gamma\ ,\ q[(\alpha\!s)\ty{op}/\alpha])$ and
therefore $M'$ is a model of ${\cal T}'$, as required.

\medskip

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}}{\sf Type\_Definition}\ 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}}{\sf
Type\_Definition}\ p\ f$, one has that
\[
{\cal T}{+_{tydef}}
\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle
={\cal T}{+_{\it tyspec}}
\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\emptyset,q\rangle
\]
Thus the Proposition in Section~\ref{tydefs} 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.
\index{extension, of HOL logic@extension, of \HOL{} logic!by type specification|)}



%%% Local Variables:
%%% mode: latex
%%% TeX-master: "logic"
%%% End: