% Revised version of Part II, Chapter 9 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{Syntax and Semantics}\label{logic}

\section{Introduction}
\label{introduction}

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

The \HOL{} syntax contains syntactic categories of types and terms whose
elements are intended to denote respectively certain sets and elements
of sets. This set theoretic interpretation will be developed alongside
the description of the \HOL{} syntax, and in the next chapter the \HOL\
proof system will be shown to be sound for reasoning about properties
of the set theoretic model.\footnote{There are other, `non-standard'
models of \HOL, which will not concern us here.} This model is given in
terms of a fixed set of sets $\cal U$, which will be called the {\em
universe\/}\index{universe, in semantics of HOL logic@universe, in
semantics of \HOL{} logic} and which is assumed to have the following
properties.
\begin{description}

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

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

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

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

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

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

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

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

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

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

\end{description}
Similarly, because of {\bf Sub} and {\bf Infty}, $\cal U$ contains
two-element sets, one of which will be singled out.
\begin{description}

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

\end{description}

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

\section{Types}
\label{types}

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

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

\newlength{\ttX}
\settowidth{\ttX}{\tt X}
\newcommand{\tyvar}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,0){\makebox(0,0)[b]{\footnotesize type variables}}
\put(0,1.5){\vector(0,1){4.5}}
\end{picture}}
\newcommand{\tyatom}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,2.3){\makebox(0,0)[b]{\footnotesize atomic types}}
\put(.5,3.3){\vector(0,1){2.6}}
\end{picture}}
\newcommand{\funty}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,1.5){\makebox(0,0)[b]{\footnotesize function types}}
\put(.5,0){\makebox(0,0)[b]{\footnotesize (domain $\sigma_1$, codomain $\sigma_2$)}}
\put(1,2.5){\vector(0,1){3.5}}
\end{picture}}
\newcommand{\cmpty}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(2,3.3){\makebox(0,0)[b]{\footnotesize compound types}}
\put(1.9,4.5){\vector(0,1){1.5}}
\end{picture}}
%
$$\sigma\quad ::=\quad {\mathord{\mathop{\alpha}\limits_{\tyvar}}}
        \quad\mid\quad{\mathord{\mathop{c}\limits_{\tyatom}}}
        \quad\mid\quad\underbrace{(\sigma_1, \ldots , \sigma_n){op}}_{\cmpty}
        \quad\mid\quad\underbrace{\sigma_1\fun\sigma_2}_{\funty}$$

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

\begin{enumerate}

\item {\bf Type variables:}\index{type variables, in HOL logic@type variables, in \HOL{} logic!abstract form of} these stand for arbitrary
sets in the universe.  In Church's original formulation of simple type
theory, type variables are part of the meta-language and are used to
range over object language types.  Proofs containing type variables
were understood as proof schemes (\ie\ families of proofs). To support
such proof schemes {\it within} the \HOL{} logic, type variables have
been added to the object language type system.\footnote{This technique
was invented by Robin Milner for the object logic \PPL\ of his \LCF\
system.}

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

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

\item {\bf Function types:}\index{function types, in HOL logic@function types, in \HOL{} logic!abstract form of} If $\sigma_1$
and $\sigma_2$ are types, then $\sigma_1\fun\sigma_2$ is the function
type with {\it domain\/} $\sigma_1$ and {\it codomain} $\sigma_2$. It
denotes the set of all (total) functions from the set denoted by its
domain to the set denoted by its codomain. (In the literature
$\sigma_1\fun\sigma_2$ is written without the arrow and
backwards---\ie\ as $\sigma_2\sigma_1$.) Note that syntactically
$\fun$ is simply a distinguished type operator of arity 2 written with
infix notation. It is singled out in the definition of \HOL{} types
because it will always denote the same operation in any
model of a \HOL{} theory---in contrast to the other type operators which
may be interpreted differently in different models. (See
Section~\ref{semantics of types}.)


\end{enumerate}

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

\subsection{Type structures}
\label{type structures}
\index{type structure, in HOL logic@type structure, in \HOL{} logic}

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

It is assumed that an infinite set {\sf TyVars} of {\em type
variables\/}\index{type variables, in HOL logic@type variables, in \HOL{} logic}
 is given.  Greek letters $\alpha,\beta,\ldots$, possibly with
subscripts or primes, are used to range over {\sf Tyvars}.  The sets
{\sf TyNames} and {\sf TyVars} are assumed disjoint.

A {\it type structure\/} is a set $\Omega$ of type constants. A {\it
type constant\/}\index{type constants, in HOL logic@type constants, in \HOL{} logic} is a pair $(\nu,n)$ where $\nu\in{\sf TyNames}$ is the
name of the constant and $n$ is its arity.  Thus $\Omega\subseteq{\sf
TyNames}\times\natnums$ (where $\natnums$ is the set of natural
numbers).  It is assumed that no two distinct type constants have the
same name,
\ie\ whenever $(\nu, n_1)\in\Omega$ and
$(\nu, n_2)\in\Omega$, then $n_1 = n_2$.

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

\begin{itemize}

\item {\sf TyVars}$\ \subseteq\ ${\sf Types}$_{\Omega}$.

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

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

\item If $\sigma_1\in{\sf Types}_{\Omega}$ and $\sigma_2\in{\sf
Types}_{\Omega}$ then $\sigma_1\fun\sigma_2\in{\sf Types}_{\Omega}$.


\end{itemize}
The type operator $\fun$ is assumed to associate\index{type operators, in HOL logic@type operators, in \HOL{} logic!associativity of} to the
right, so that
\[
\sigma_1\fun\sigma_2\fun\ldots\fun \sigma_n\fun\sigma
\]
abbreviates
\[
\sigma_1\fun(\sigma_2\fun\ldots\fun (\sigma_n\fun\sigma)\ldots)
\]
The notation $tyvars(\sigma)$ is used to denote the set of type
variables occurring in $\sigma$.

\subsection{Semantics of types}
\label{semantics of types}


A {\em model} $M$ of a type structure $\Omega$ is specified by giving
for each type constant $(\nu,n)$ an $n$-ary function
\[
M(\nu):{\cal U}^{n}\longrightarrow{\cal U}
\]
Thus given sets $X_1,\ldots,X_n$ in the universe $\cal U$,
$M(\nu)(X_1,\ldots,X_n)$ is also a set in the universe.  In case $n=0$,
this amounts to specifying an element $M(\nu)\in{\cal U}$ for the
atomic type $\nu$.

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

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

For each $\sigma$ there are minimal contexts $\alpha\!s$ for which
$\alpha\!s.\sigma$ is a type-in-context, which only differ by the order
in which the type variables of $\sigma$ are listed in $\alpha\!s$. In
order to select one such context, let us assume that  {\sf TyVars}
comes with a fixed total order and define the {\em
canonical}\index{canonical contexts, in HOL logic@canonical contexts, in \HOL{} logic!of types} context of the type $\sigma$ to consist of
exactly the type variables it contains, listed in order.\footnote{It is
possible to work with unordered contexts, specified by finite sets
rather than lists, but we choose not to do that since it mildly
complicates the definition of the semantics to be given
below.}

Let $M$ be a model of a type structure $\Omega$. For each
type-in-context
$\alpha\!s.\sigma$ over $\Omega$, define a function
\[
\den{\alpha\!s.\sigma}_{M}:{\cal U}^{n}\longrightarrow{\cal U}
\]
(where $n$ is the length of the context) by induction on the structure
of $\sigma$ as follows.
\begin{itemize}

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

\item If $\sigma$ is a function type\index{function types, in HOL logic@function types, in \HOL{} logic!formal semantics of}
$\sigma_{1}\fun\sigma_{2}$, then $\den{\alpha\!s.\sigma}_M$ sends
$X\!s\in{\cal U}^n$ to the set of all functions
from $\den{\alpha\!s.\sigma_1}_M(X\!s)$ to
$\den{\alpha\!s.\sigma_2}_M(X\!s)$. (This makes
use of the property {\bf Fun} of $\cal U$.)

\item If $\sigma$ is a
compound type $(\sigma_{1},\ldots,\sigma_{m})\nu$, then
$\den{\alpha\!s.\sigma}_{M}$ sends $X\!s$ to
$M(\nu)(S_{1},\ldots,S_{m})$ where each $S_{j}$ is
$\den{\alpha\!s.\sigma_{j}}_{M}(X\!s)$.
\end{itemize}
One can now define the meaning of a type $\sigma$ in a model $M$ to be
the function
\[
\den{\sigma}_{M}:{\cal U}^{n}\longrightarrow{\cal U}
\]
given by $\den{\alpha\!s.\sigma}_{M}$, where $\alpha\!s$ is the
canonical context of $\sigma$. If $\sigma$ is monomorphic, then $n=0$
and $\den{\sigma}_{M}$ can be identified with the element
$\den{\sigma}_{M}()$ of $\cal U$. When the particular model $M$ is
clear from the context, $\den{\_}_{M}$ will be written $\den{\_}$.

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

\medskip

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

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

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

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

\end{enumerate}

\medskip

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

\subsection{Instances and substitution}
\label{instances-and-substitution}

If $\sigma$ and $\tau_1,\ldots,\tau_n$ are types over a type structure
$\Omega$,
\[
\sigma[\tau_{1},\ldots,\tau_{p}/\beta_{1},\ldots,\beta_{p}]
\]
will denote the type resulting from the simultaneous substitution for
each $i=1,\ldots,p$ of
$\tau_i$ for the type variable $\beta_i$ in $\sigma$.
The resulting type is called an {\it instance\/}\index{types, in HOL logic@types, in \HOL{} logic!instantiation of} of $\sigma$. The
following lemma about instances will be useful later; it is proved by
induction on the structure of $\sigma$.

\medskip

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

\medskip

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

\medskip

\noindent{\bf Lemma 2\ }{\it Given types-in-context $\beta\!s.\sigma$ and
$\alpha\!s.\tau_i$ ($i=1,\ldots,p$, where $p$ is the
length of $\beta\!s$), let $\sigma'$ be the instance
$\sigma[\tau\!s/\beta\!s]$. Then $\alpha\!s.\sigma'$ is also a
type-in-context and its meaning in any model $M$ is related to that of
$\beta\!s.\sigma$ as follows. For all $X\!s\in{\cal U}^n$ (where $n$
is the length of $\alpha\!s$)
\[
\den{\alpha\!s.\sigma'}(X\!s) =
\den{\beta\!s.\sigma}(\den{\alpha\!s.\tau_{1}}(X\!s),
    \ldots ,\den{\alpha\!s.\tau_{p}}(X\!s))
\]
}
Once again, the lemma can be proved by induction on the structure of
$\sigma$.

\section{Terms}
\label{terms}

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

There are four kinds of terms in the \HOL{} logic. These can be
described approximately by the following {\small BNF} grammar, in
which $x$ ranges over variables and $c$ ranges over constants.
\index{combinations, in HOL logic@combinations, in \HOL{} logic!abstract form of}

\settowidth{\ttX}{\tt X}
\newcommand{\var}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,0){\makebox(0,0)[b]{\footnotesize variables}}
\put(0,1.5){\vector(0,1){4.5}}
\end{picture}}
\newcommand{\const}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,2.3){\makebox(0,0)[b]{\footnotesize constants}}
\put(.5,3.5){\vector(0,1){2.4}}
\end{picture}}
\newcommand{\app}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(.5,1.5){\makebox(0,0)[b]{\footnotesize function applications}}
\put(.5,0){\makebox(0,0)[b]{\footnotesize (function $t$, argument $t'$)}}
\put(0.5,2.5){\vector(0,1){3.5}}
\end{picture}}
\newcommand{\abs}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6)
\put(1,3.3){\makebox(0,0)[b]{\footnotesize $\lambda$-abstractions}}
\put(0.7,4.5){\vector(0,1){1.5}}
\end{picture}}
%
$$ t \quad ::=\quad {\mathord{\mathop{x}\limits_{\var}}}
        \quad\mid\quad{\mathord{\mathop{\con{c}}\limits_{\const}}}
        \quad\mid\quad\underbrace{t\ t'}_{\app}
        \quad\mid\quad\underbrace{\lambda x .\ t}_{\abs}$$

Informally, a $\lambda$-term\index{lambda terms, in HOL logic@lambda terms, in \HOL{} logic}\index{function abstraction, in HOL logic@function abstraction, in \HOL{} logic!abstract form of} $\lambda x.\ t$ denotes
a function $v\mapsto t[v/x]$, where $t[v/x]$ denotes the result of
substituting $v$ for $x$ in $t$. An application\index{function application, in HOL logic@function application, in \HOL{} logic!abstract form of} $t\ t'$ denotes the result of applying the
function denoted by $t$ to the value denoted by $t'$. This will be
made more precise below.

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

$$ t_{\sigma} \quad ::=\quad {\mathord{\mathop{x_{\sigma}}\limits_{}}}
\quad\mid\quad
{\mathord{\mathop{\con{c}_{\sigma}}\limits_{}}}
\quad\mid\quad (t_{\sigma'\fun\sigma}\ t'_{\sigma'})_{\sigma}
\quad\mid\quad(\lambda x_{\sigma_1} .\ t_{\sigma_2})
_{\sigma_1\fun\sigma_2}$$\index{constants, in HOL logic@constants, in \HOL{} logic!abstract form of}

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

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

\item {\bf Constants:} If $(\con{c},\sigma)\in{\Sigma_{\Omega}}$ and
$\sigma'\in{\sf Types}_{\Omega}$
is an instance of $\sigma$, then $(\con{c},{\sigma'})\in{\sf
Terms}_{\Sigma_{\Omega}}$.  Terms formed in this way are called {\it
constants\/}\index{constants, in HOL logic@constants, in \HOL{} logic!abstract form of} and are written $\con{c}_{\sigma'}$.

\item {\bf Variables:}  If  $x\in{\sf  Names}$  and  $\sigma\in{\sf
Types}_{\Omega}$, then ${\tt var}\ x_{\sigma}\in{\sf
Terms}_{\Sigma_{\Omega}}$. Terms formed in this way are called {\it
variables}\index{variables, in HOL logic@variables, in \HOL{} logic!abstract form of}.  The marker {\tt var}\ is purely a device to
distinguish variables from constants with the same name.  A variable
${\tt var}\ x_{\sigma}$ will usually be written as $x_{\sigma}$, if it
is clear from the context that $x$ is a variable rather than a
constant.

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

\item {\bf $\lambda$-Abstractions:} If ${\tt var}\ x_{\sigma_1}
\in{\sf Terms}_{\Sigma_{\Omega}}$  and $t_{\sigma_2}\in{\sf
Terms}_{\Sigma_{\Omega}}$, then $(\lambda x_{\sigma_1}.\
t_{\sigma_2})_{\sigma_1\fun\sigma_2}
\in{\sf Terms}_{\Sigma_{\Omega}}$.

\end{enumerate}

Note that it is possible for constants and variables\index{variables, in HOL logic@variables, in \HOL{} logic!with same names} to have the
same name.  It is also possible for different variables to have the
same name, if they have different types.

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

Function application\index{function application, in HOL logic@function application, in \HOL{} logic!associativity of} is assumed to associate
to the left, so that $t\ t_1\ t_2\ \ldots\ t_n$ abbreviates $(\
\ldots\ ((t\ t_1)\ t_2)\ \ldots\ t_n)$.

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

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

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

\subsection{Terms-in-context}
\label{terms-in-context}

A {\em context\/}\index{contexts, in semantics of HOL logic@contexts, in semantics of \HOL{} logic} $\alpha\!s,\!x\!s$ consists of a type
context $\alpha\!s$ together with a list $x\!s=x_{1},\ldots,x_{m}$ of
distinct variables whose types only contain type variables from the
list $\alpha\!s$.

The condition that $x\!s$ contains {\em distinct\/} variables needs
some comment. Since a variable is specified by both a name and a
type,  it is permitted for $x\!s$ to contain repeated
names\index{variables, in HOL logic@variables, in \HOL{} logic!with same names},
 so long as different types are attached to the
names. This aspect of the syntax means that one has to proceed with
caution when defining the meaning of type variable instantiation,
since instantiation may cause variables to become equal
`accidentally': see Section~\ref{term-substitution}.

A {\em term-in-context\/}\index{term-in-context}
$\alpha\!s,\!x\!s.t$ consists of a context together with a term
$t$ satisfying the following conditions.
\begin{itemize}

\item $\alpha\!s$ contains any type variable that occurs in $x\!s$ and $t$.

\item $x\!s$ contains any variable that occurs freely in $t$.

\item $x\!s$ does not contain any variable that occurs
bound in $t$.

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

\subsection{Semantics of terms}
\label{semantics of terms}

Let $\Sigma_{\Omega}$ be a signature\index{signatures, of HOL logic@signatures, of \HOL{} logic!formal semantics of} over a type
structure $\Omega$ (see Section~\ref{terms}). A {\em model\/} $M$ of
$\Sigma_{\Omega}$ is specified by a model of the type structure plus
for each constant\index{primitive constants, of HOL logic@primitive constants, of \HOL{} logic} $(\con{c},\sigma)\in\Sigma_{\Omega}$ an
element
\[
M(\con{c},\sigma) \in
\prod_{X\!s\in{\cal U}^{n}}\den{\sigma}_{M}(X\!s)
\]
of the indicated cartesian product, where $n$ is the number of type
variables occurring in $\sigma$. In other words
$M(\con{c},\sigma)$ is a (dependently typed) function
assigning to each $X\!s\in{\cal U}^{n}$ an element of
$\den{\sigma}_{M}(X\!s)$. In the case that $n=0$ (so that
$\sigma$ is monomorphic), $\den{\sigma}_{M}$ was identified
with a set in $\cal U$ and then $M(c,\sigma)$ can be
identified with an element of that set.

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

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

\item $t$ has type $\tau$

\item $x\!s=x_{1},\ldots,x_{m}$ and each $x_{j}$ has type $\sigma_{j}$

\item $\alpha\!s=\alpha_{1},\ldots,\alpha_{n}$.

\end{itemize}
Then since $\alpha\!s,\!x\!s.t$ is a term-in-context, $\alpha\!s.\tau$
and $\alpha\!s.\sigma_{j}$ are types-in-context, and hence give rise
to functions $\den{\alpha\!s.\tau}_{M}$ and
$\den{\alpha\!s.\sigma_{j}}_{M}$ from ${\cal U}^{n}$ to $\cal U$ as in
section~\ref{semantics of types}. The meaning of $\alpha\!s,\!x\!s.t$
in the model $M$ will be given by an element
\[
\den{\alpha\!s,\!x\!s.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 \den{\alpha\!s.\tau}_{M}(X\!s) .
\]
In other words, given
\begin{eqnarray*}
X\!s & = & (X_{1},\ldots,X_{n})\in{\cal U}^{n} \\
y\!s & = & (y_{1},\ldots,y_{m})\in\den{\alpha\!s.\sigma_{1}}_{M}(X\!s)
           \times\cdots\times \den{\alpha\!s.\sigma_{m}}_{M}(X\!s)
\end{eqnarray*}
one gets an element $\den{\alpha\!s,\!x\!s.t}_{M}(X\!s)(y\!s)$ of
$\den{\alpha\!s.\tau}_{M}(X\!s)$. The definition of
$\den{\alpha\!s,\!x\!s.t}_{M}$ proceeds by induction on the structure of
the term $t$, as follows. (As before, the subscript $M$ will be dropped from
the semantic brackets $\den{ \_ }$ when the particular model involved is
clear from the context.)
\begin{itemize}

\item
If $t$ is a variable\index{variables, in HOL logic@variables, in \HOL{} logic!formal semantics of}, it must be $x_{j}$ for some unique
$j=1,\ldots,m$, so $\tau=\sigma_{j}$ and then
$\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ is defined to be $y_{j}$.

\item
Suppose $t$ is a constant\index{constants, in HOL logic@constants, in \HOL{} logic!formal semantics of} $\con{c}_{\sigma'}$, where
$(\con{c},\sigma)\in\Sigma_{\Omega}$ and $\sigma'$ is an instance of
$\sigma$.  Then by Lemma~1 of \ref{instances-and-substitution},
$\sigma'=\sigma[\tau_{1},\ldots,\tau_{p}/\beta_{1},\ldots,\beta_{p}]$
for uniquely determined types $\tau_{1},\ldots,\tau_{p}$ (where
$\beta_{1},\ldots,\beta_{p}$ are the type variables occurring in
$\sigma$). Then define $\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ to be
$M(\con{c},\sigma)(\den{\alpha\!s.\tau_{1}}(X\!s),
\ldots,\den{\alpha\!s.\tau_{p}}(X\!s))$,
which is an element of $\den{\alpha\!s.\tau}(X\!s)$ by Lemma~2 of
\ref{instances-and-substitution} (since $\tau$ is $\sigma'$).

\item
Suppose $t$ is a function application\index{combinations, in HOL logic@combinations, in \HOL{} logic!formal semantics of} term $(t_{1}\
t_{2})$\index{function application, in HOL logic@function application, in \HOL{} logic!formal semantics of} where $t_{1}$ is of type
$\tau'\fun\tau$ and $t_{2}$ is of type $\tau'$. Then
$f=\den{\alpha\!s,\!x\!s.t_{1}}(X\!s)(y\!s)$, being an element of
$\den{\alpha\!s.\tau'\fun\tau}(X\!s)$, is a function from the set
$\den{\alpha\!s.\tau'}(X\!s)$ to the set $\den{\alpha\!s.\tau}(X\!s)$
which one can apply to the element
$y=\den{\alpha\!s,\!x\!s.t_{2}}(X\!s)(y\!s)$. Define
$\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ to be $f(y)$.

\item Suppose $t$ is the abstraction\index{function abstraction, in HOL logic@function abstraction, in \HOL{} logic!formal semantics of}
term $\lambda x.t_{2}$where $x$ is of type $\tau_{1}$ and $t_{2}$ of
type $\tau_{2}$. Thus $\tau=\tau_{1}\fun\tau_{2}$ and
$\den{\alpha\!s.\tau}(X\!s)$ is the function set
$\den{\alpha\!s.\tau_{1}}(X\!s)\fun\den{\alpha\!s.\tau_{2}}(X\!s)$.
Define $\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ to be the element of
this set which is the function sending
$y\in\den{\alpha\!s.\tau_{1}}(X\!s)$ to
$\den{\alpha\!s,\!x\!s,\!x.t_{2}}(X\!s)(y\!s,y)$. (Note that since
$\alpha\!s,\!x\!s.t$ is a term-in-context, by convention the bound
variable $x$ does not occur in $x\!s$ and thus
$\alpha\!s,\!x\!s,\!x.t_{2}$ is also a term-in-context.)
\end{itemize}
Now define the meaning of a term $t_{\tau}$ in a model $M$ to be the
dependently typed function
\[ \den{t_{\tau}} \in \prod_{X\!s\in{\cal U}^{n}}
   \left(\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}(X\!s)\right)
   \fun \den{\alpha\!s.\tau}(X\!s)
\]
given by $\den{\alpha\!s,\!x\!s.t_{\tau}}$, where $\alpha\!s,\!x\!s$ is the
canonical context of $t_{\tau}$. So $n$ is the number of type variables in
$t_{\tau}$, $\alpha\!s$ is a list of those type variables, $m$ is the
number of ordinary variables occurring freely in $t_{\tau}$ (assumed to be
distinct from the bound variables of $t_{\tau}$) and the $\sigma_{j}$ are
the types of those variables. (It is important to note that the list
$\alpha\!s$, which is part of the canonical context of $t$, may be strictly
bigger than the canonical type contexts of $\sigma_{j}$ or $\tau$. So it
would not make sense to write just $\den{\sigma_{j}}$ or $\den{\tau}$ in
the above definition.)

If $t_{\tau}$ is a closed term, then $m=0$ and for each $X\!s\in{\cal
U}^{n}$ one can identify $\den{t_{\tau}}$ with the element
$\den{t_{\tau}}(X\!s)()\in\den{\alpha\!s.\tau}(X\!s)$. So for closed terms
one gets
\[ \den{t_{\tau}} \in \prod_{X\!s\in{\cal U}^{n}}
\den{\alpha\!s.\tau}(X\!s)
\]
where $\alpha\!s$ is the list of type variables occurring in $t_{\tau}$ and
$n$ is the length of that list. If moreover, no type variables occur in
$t_{\tau}$, then $n=0$ and $\den{t_{\tau}}$ can be identified with the
element $\den{t_{\tau}}()$ of the set $\den{\tau}\in{\cal U}$.

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

\subsection{Substitution}
\label{term-substitution}

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

\subsubsection*{Substituting types for type variables in terms}
\index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!formal semantics of}

Suppose $t$ is a term, with canonical context $\alpha\!s,\!x\!s$ say,
where $\alpha\!s = \alpha_1,\ldots,\alpha_n$, $x\!s = x_1,\ldots,x_m$
and where for $j=1,\ldots,m$ the type of the variable $x_j$ is
$\sigma_j$. If $\alpha\!s'.\tau_{i}$ ($i=1,\ldots,n$) are
types-in-context, then substituting\index{type substitution, in HOL logic@type substitution, in \HOL{} logic!formal semantics of} the types
$\tau_{i}$ for the type variables $\alpha_{i}$ in the list $x\!s$, one
obtains a new list of variables $x\!s'$. Thus the $j$\/th entry of
$x\!s'$ has type $\sigma'_{j} = \sigma_{j}[\tau\!s/\alpha\!s]$. Only
substitutions with the following property will be considered.
\begin{quote}
In instantiating\index{types, in HOL logic@types, in \HOL{} logic!instantiation of} the type variables $\alpha\!s$ with the types
$\tau\!s$, no two distinct variables in the list $x\!s$ become equal in
the list $x\!s'$.\footnote{Such an identification of variables could
occur if the variables had the same name component and their types
became equal on instantiation.}
\end{quote}
This condition ensures that $\alpha\!s',x\!s'$ really is a context. Then
one obtains a new term-in-context $\alpha\!s',\!x\!s'.t'$ by
substituting the types $\tau\!s=\tau_{1},\ldots,\tau_{n}$ for the type
variables $\alpha\!s$ in $t$ (with suitable renaming of bound
occurrences of variables to make them distinct from the variables in
$x\!s'$). The notation
\[
t[\tau\!s/\alpha\!s]
\]
is used for the term $t'$.

\medskip

\noindent{\bf Lemma 3\ }{\it
The meaning of $\alpha\!s',\!x\!s'.t'$ in a model is  related to that
of $t$ as follows. For all $X\!s'\in{\cal U}^{n'}$ (where $n'$ is the
length of $\alpha\!s'$)}
\[
\den{\alpha\!s',\!x\!s'.t'}(X\!s') =
   \den{t}(\den{\alpha\!s'.\tau_{1}}(X\!s'),\ldots,
   \den{\alpha\!s'.\tau_{n}}(X\!s')).
\]

\medskip

Lemma~2 in \ref{instances-and-substitution} is needed to see that both
sides of the above equation are elements of the same set of functions.
The validity of the equation is proved by induction on the structure
of the term $t$.

\subsubsection*{Substituting terms for variables in terms}
\index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!formal semantics of}

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

\medskip

\noindent{\bf Lemma 4\ }{\it
The meaning of $\alpha\!s,\!x\!s'.t''$ in a model is related to that of
$t$ as follows. For all $X\!s\in{\cal U}^{n}$ and all
$y\!s'\in\den{\alpha\!s.\sigma'_{1}} \times\cdots\times
\den{\alpha\!s.\sigma'_{m'}}$ (where $\sigma'_{j}$ is the type of
$x'_{j}$)}
\[
\den{\alpha\!s,\!x\!s'.t''}(X\!s)(y\!s') = \den{t}(X\!s)(
\den{\alpha\!s,\!x\!s'.t_{1}}(X\!s)(y\!s'),\ldots,
\den{\alpha\!s,\!x\!s'.t_{m}}(X\!s)(y\!s'))
\]

\medskip

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


\section{Standard notions}

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

\subsection{Standard type structures}
\label{standard-type-structures}

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

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

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

\subsection{Standard signatures}
\label{standard-signatures}
\index{signatures, of HOL logic@signatures, of \HOL{} logic!standard}\index{standard signatures, of HOL logic@standard signatures, of \HOL{} logic}

A signature $\Sigma_{\Omega}$ is {\em standard\/} if it contains the
following three primitive constants\index{primitive constants, of HOL logic@primitive constants, of \HOL{} logic}\index{constants, in HOL logic@constants, in \HOL{} logic!primitive, abstract form of}:
\[
{\imp}_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}
\]
\[
{=}_{\alpha\fun\alpha\fun\ty{bool}}
\]
\[
\hilbert_{(\alpha\fun\ty{bool})\fun\alpha}
\]
The intended interpretation of these constants is that  $\imp$ denotes
implication, $=_{\sigma\fun\sigma\fun\ty{bool}}$ denotes equality on
the set denoted by $\sigma$, and
$\hilbert_{(\sigma\fun\ty{bool})\fun\sigma}$ denotes a choice function
on the set denoted by $\sigma$. More precisely, a model $M$ of
$\Sigma_{\Omega}$ will be called {\em standard\/}\index{standard models, of HOL logic@standard models, of \HOL{} logic} if
\begin{itemize}

\item
$M({\imp},\bool\fun\bool\fun\bool)\in(\two\fun\two\fun\two)$ is the
standard implication\index{implication, in HOL logic@implication, in \HOL{} logic!formal semantics of} function, sending $b,b'\in\two$ to
\[
(b\imp b') = \left\{ \begin{array}{ll}
                           0 & \mbox{if $b=1$ and $b'=0$} \\
                           1 & \mbox{otherwise}
                          \end{array}
             \right.%}
\]

\item
$M({=},\alpha\fun\alpha\fun\bool)\in\prod_{X\in{\cal U}}.X\fun
X\fun\two$ is the function assigning to each $X\in{\cal U}$ the
equality\index{equality, in HOL logic@equality, in \HOL{} logic!formal semantics of} test function, sending $x,x'\in X$ to
\[
(x=_{X}x') = \left\{ \begin{array}{ll}
                           1 & \mbox{if $x=x'$} \\
                           0 & \mbox{otherwise}
                          \end{array}
             \right.%}
\]

\item
\index{epsilon operator}$M(\hilbert,(\alpha\fun\bool)\fun\alpha)\in\prod_{X\in{\cal
U}}.(X\fun\two)\fun X$ is the function assigning to each $X\in{\cal
U}$ the choice\index{choice operator, in HOL logic@choice operator, in \HOL{} logic!formal semantics of} function sending $f\in(X\fun\two)$ to
\[
\ch_{X}(f) = \left\{ \begin{array}{ll}
                           \ch(f^{-1}\{1\})
                             & \mbox{if $f^{-1}\{1\}\not=\emptyset$}\\
                           \ch(X) & \mbox{otherwise}
                          \end{array}
             \right.%}
\]
where $f^{-1}\{1\}=\{x\in X : f(x)=1\}$. (Note that $f^{-1}\{1\}$ is in
$\cal U$ when it is non-empty, by the property {\bf Sub} of the
universe $\cal U$ given in Section~\ref{introduction}. The function
$\ch$ is given by property {\bf Choice}.)

\end{itemize}

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

\medskip

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

\medskip

Terms of type \ty{bool} are  called {\it formulas\/}\index{formulas as terms, in HOL logic@formulas as terms, in \HOL{} logic}.

The following notational abbreviations are used:

\begin{center}
\index{equality, in HOL logic@equality, in \HOL{} logic!abstract form of}
\index{implication, in HOL logic@implication, in \HOL{} logic!abstract form of}
\index{choice operator, in HOL logic@choice operator, in \HOL{} logic!abstract form of}
\index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abstract form of}
\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!abstract form of}
\index{epsilon operator}
\begin{tabular}{|l|l|}\hline
{\rm Notation} & {\rm Meaning}\\ \hline
$t_{\sigma}=t'_{\sigma}$ &
  $=_{\sigma\fun\sigma\fun\ty{bool}}\ t_{\sigma}\ t'_{\sigma}$\\ \hline
$t\imp t'$ &
  $\imp_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}\ t_\ty{bool}\
t'_\ty{bool}$\\ \hline
$\hilbert x_{\sigma}.\ t$ &
  $ \hilbert_{(\sigma\fun\ty{bool})\fun\sigma}
(\lambda x_{\sigma}.\ t)$\\ \hline
\end{tabular}
\end{center}
These notations are special cases of general abbreviatory conventions
supported by the \HOL{} system. The first two are infixes and the
third is a binder (see \DESCRIPTION's sections on parsing and
pretty-printing).



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