1 % Revised version of Part II, Chapter 9 of HOL DESCRIPTION
2 % Incorporates material from both of chapters 9 and 10 of the old
3 % version of DESCRIPTION
12 This chapter describes the syntax and set-theoretic semantics of the
13 logic supported by the \HOL{} system, which is a variant of
14 Church's\index{Church, A.} simple theory of types \cite{Church} and
18 of this description is the \HOL{} logic.  Note that there is a
21 to manipulate the \HOL{} logic by users of the system.  It is hoped
22 that because of context, no confusion results from these two uses of
23 the word `meta-language'.  When \ML\ is the object of study (as in
27 The \HOL{} syntax contains syntactic categories of types and terms whose
29 of sets. This set theoretic interpretation will be developed alongside
30 the description of the \HOL{} syntax, and in the next chapter the \HOL\
32 of the set theoretic model.\footnote{There are other, `non-standard'
33 models of \HOL, which will not concern us here.} This model is given in
34 terms of a fixed set of sets $\cal U$, which will be called the {\em
35 universe\/}\index{universe, in semantics of HOL logic@universe, in
36 semantics of \HOL{} logic} and which is assumed to have the following
40 \item[Inhab] Each element of $\cal U$ is a non-empty set.
47 consisting of ordered pairs $(x,y)$ with $x\in X$ and $y\in Y$, with
48 the usual set-theoretic coding of ordered pairs, \viz\
52 $P(X)=\{Y:Y\subseteq X\}$ is also an element of $\cal U$.
57 U}}X$. The elements of the product $\prod_{X\in{\cal U}}X$ are
62 There are some consequences of these assumptions which will be needed.
64 certain sets of ordered pairs. Thus the set $X\fun Y$ of all functions
65 from a set $X$ to a set $Y$ is a subset of $P(X\times Y)$; and it is a
73 By iterating {\bf Prod}, one has that the cartesian product of any
74 finite, non-zero number of sets in $\cal U$ is again in $\cal U$.
75 $\cal U$ also contains the cartesian product of no sets, which is to
76 say that it contains a one-element set (by virtue of {\bf Sub} applied
84 Similarly, because of {\bf Sub} and {\bf Infty}, $\cal U$ contains
85 two-element sets, one of which will be singled out.
94 universe of sets by the axioms of
96 Axiom of Choice (\theory{ZFC})\index{axiom of choice}\index{ZFC@\ml{ZFC}},
98 required to satisfy any form of the Axiom of
99 Replacement\index{axiom of replacement}.
100 Indeed, it is possible to prove the existence of a set
101 $\cal U$ with the above properties from the axioms of \theory{ZFC}.
102 (For example one could take $\cal U$ to consist of all non-empty sets
104 $\omega+\omega$.) Thus, as with many other pieces of mathematics, it is
106 \theory{ZFC} set theory of the semantics of the \HOL{} logic to be given
112 The types\index{type constraint!in HOL logic@in \HOL{} logic} of the
118 There are four kinds of types in the \HOL{} logic. These can be described
149 \noindent In more detail, the four kinds of types are as follows.
153 \item {\bf Type variables:}\index{type variables, in HOL logic@type variables, in \HOL{} logic!abstract form of} these stand for arbitrary
154 sets in the universe.  In Church's original formulation of simple type
155 theory, type variables are part of the meta-language and are used to
157 were understood as proof schemes (\ie\ families of proofs). To support
160 was invented by Robin Milner for the object logic \PPL\ of his \LCF\
164 theory determines a particular collection of atomic types.  For
169 \item {\bf Compound types:}\index{compound types, in HOL logic@compound types, in \HOL{} logic!abstract form of} These have the
172 of arity $n$.  Type operators denote operations for constructing sets.
177 of forming all finite lists of elements from a given set.  Another
178 example is the type operator \ty{prod} of arity 2 which denotes the
182 \item {\bf Function types:}\index{function types, in HOL logic@function types, in \HOL{} logic!abstract form of} If $\sigma_1$
185 denotes the set of all (total) functions from the set denoted by its
189 $\fun$ is simply a distinguished type operator of arity 2 written with
190 infix notation. It is singled out in the definition of \HOL{} types
192 model of a \HOL{} theory---in contrast to the other type operators which
194 Section~\ref{semantics of types}.)
201 the atomic type \ty{bool} of truth-values can be regarded as being an
213 TyNames} of the {\em names of type constants\/} is given.  The greek
214 letter $\nu$ is used to range over arbitrary members of {\sf TyNames},
215 \textsl{c} will continue to be used to range over the names of atomic
217 over the names of type operators (\ie\ $n$-ary type constants, where
220 It is assumed that an infinite set {\sf TyVars} of {\em type
226 A {\it type structure\/} is a set $\Omega$ of type constants. A {\it
228 name of the constant and $n$ is its arity.  Thus $\Omega\subseteq{\sf
229 TyNames}\times\natnums$ (where $\natnums$ is the set of natural
235 The set {\sf Types}$_{\Omega}$ of types over a structure ${\Omega}$
253 The type operator $\fun$ is assumed to associate\index{type operators, in HOL logic@type operators, in \HOL{} logic!associativity of} to the
262 The notation $tyvars(\sigma)$ is used to denote the set of type
265 \subsection{Semantics of types}
266 \label{semantics of types}
269 A {\em model} $M$ of a type structure $\Omega$ is specified by giving
281 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
286 assignment of sets to the relevant type variables. The arity $n$
287 corresponds to the number of type variables involved. It is convenient
289 involved in the semantics of a type $\sigma$ whether or not it
290 actually occurs in $\sigma$, leading to the notion of a
294 finite (possibly empty) list of {\em distinct\/} type variables
305 in which the type variables of $\sigma$ are listed in $\alpha\!s$. In
308 canonical}\index{canonical contexts, in HOL logic@canonical contexts, in \HOL{} logic!of types} context of the type $\sigma$ to consist of
312 complicates the definition of the semantics to be given
315 Let $M$ be a model of a type structure $\Omega$. For each
321 (where $n$ is the length of the context) by induction on the structure
322 of $\sigma$ as follows.
330 \item If $\sigma$ is a function type\index{function types, in HOL logic@function types, in \HOL{} logic!formal semantics of}
332 $X\!s\in{\cal U}^n$ to the set of all functions
335 use of the property {\bf Fun} of $\cal U$.)
343 One can now define the meaning of a type $\sigma$ in a model $M$ to be
349 canonical context of $\sigma$. If $\sigma$ is monomorphic, then $n=0$
351 $\den{\sigma}_{M}()$ of $\cal U$. When the particular model $M$ is
354 To summarize, given a model in $\cal U$ of a type structure $\Omega$,
356 $\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
382 meanings to types in the presence of `environments' assigning sets in
383 $\cal U$ to all type variables. The use of types-in-contexts is almost
386 finite (ordered) set of type variables. At the level of types there is
388 and semantics of terms to be given below, where there is a dependency
401 each $i=1,\ldots,p$ of
403 The resulting type is called an {\it instance\/}\index{types, in HOL logic@types, in \HOL{} logic!instantiation of} of $\sigma$. The
405 induction on the structure of $\sigma$.
413 an instance of $\sigma$.  Then the types $\tau_1,\ldots,\tau_p$ are
418 We also need to know how the semantics of types behaves with respect
425 length of $\beta\!s$), let $\sigma'$ be the instance
427 type-in-context and its meaning in any model $M$ is related to that of
429 is the length of $\alpha\!s$)
436 Once again, the lemma can be proved by induction on the structure of
442 The terms of the \HOL{} logic are expressions that denote elements of the sets
447 There are four kinds of terms in the \HOL{} logic. These can be
450 \index{combinations, in HOL logic@combinations, in \HOL{} logic!abstract form of}
476 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
477 a function $v\mapsto t[v/x]$, where $t[v/x]$ denotes the result of
478 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
482 The {\small BNF} grammar just given omits mention of types. In fact, each
486 traditionally used to range over terms of type $\sigma$. A
487 more accurate grammar of
495 _{\sigma_1\fun\sigma_2}$$\index{constants, in HOL logic@constants, in \HOL{} logic!abstract form of}
497 In fact, just as the definition of types was relative to a particular
498 type structure $\Omega$, the formal definition of terms is relative to
499 a given collection of typed constants over $\Omega$.  Assume that an
500 infinite set {\sf Names} of names is given. A {\em constant\/} over
503 is just a set $\Sigma_\Omega$ of such constants.
505 The set {\sf Terms}$_{\Sigma_{\Omega}}$ of terms over
507 following rules of formation:
512 is an instance of $\sigma$, then $(\con{c},{\sigma'})\in{\sf
514 constants\/}\index{constants, in HOL logic@constants, in \HOL{} logic!abstract form of} and are written $\con{c}_{\sigma'}$.
519 variables}\index{variables, in HOL logic@variables, in \HOL{} logic!abstract form of}.  The marker {\tt var}\ is purely a device to
544 structure of the term or the context in which it occurs what its type
547 Function application\index{function application, in HOL logic@function application, in \HOL{} logic!associativity of} is assumed to associate
559 $tyvars(t_{\sigma})$ denotes the set of type variables occurring in
562 An occurrence of a variable $x_{\sigma}$ is called {\it
563 bound\/}\index{bound variables, in HOL logic@bound variables, in \HOL{} logic}\index{variables, in HOL logic@variables, in \HOL{} logic!abstract form of}
564  if it occurs within the scope of a textually enclosing
566 free\/}\index{free variables, in HOL logic@free variables, in \HOL{} logic!abstract form of}. Note that $\lambda x_{\sigma}$ does not bind
568 of variables are bound is called {\it closed\/}.
573 A {\em context\/}\index{contexts, in semantics of HOL logic@contexts, in semantics of \HOL{} logic} $\alpha\!s,\!x\!s$ consists of a type
574 context $\alpha\!s$ together with a list $x\!s=x_{1},\ldots,x_{m}$ of
583 names. This aspect of the syntax means that one has to proceed with
584 caution when defining the meaning of type variable instantiation,
589 $\alpha\!s,\!x\!s.t$ consists of a context together with a term
602 not appear in $t$.  Note that the combination of the second and third
608 names of their bound variables.} In the semantics of terms to be given
609 below we will restrict attention to such terms. Then the meaning of an
610 arbitrary term is taken to be the meaning of some $\alpha$-variant of
618 canonical}\index{canonical contexts, in HOL logic@canonical contexts, in \HOL{} logic!of terms} context of the term $t$.
620 \subsection{Semantics of terms}
621 \label{semantics of terms}
623 Let $\Sigma_{\Omega}$ be a signature\index{signatures, of HOL logic@signatures, of \HOL{} logic!formal semantics of} over a type
624 structure $\Omega$ (see Section~\ref{terms}). A {\em model\/} $M$ of
625 $\Sigma_{\Omega}$ is specified by a model of the type structure plus
626 for each constant\index{primitive constants, of HOL logic@primitive constants, of \HOL{} logic} $(\con{c},\sigma)\in\Sigma_{\Omega}$ an
632 of the indicated cartesian product, where $n$ is the number of type
635 assigning to each $X\!s\in{\cal U}^{n}$ an element of
639 identified with an element of that set.
641 The meaning of \HOL{} terms in such a model will now be described. The
643 elements of sets in $\cal U$ (the particular set involved being derived
644 from the type of the term as in Section~\ref{semantics of types}). More
646 interpreted as an element of a product $\prod_{X\!s\in{\cal
648 U}$ is derived from the type of the term (in a type context derived
649 from the term). Thus the meaning of the term is a (dependently typed)
651 variables in the term, yields a meaning for the term as an element of a
655 $\cal U$ are the interpretations of the types of the free variables in
656 the term and the set $Y\in{\cal U}$ is the interpretation of the type
657 of the term; thus the meaning of the term is a function which, when
659 yields a meaning for the term. Finally, the most general case is of a
661 interpreted as an element of a product
667 U}^{n}\longrightarrow{\cal U}$ are determined by the types of the free
668 variables and the type of the term (in a type context derived from the
686 section~\ref{semantics of types}. The meaning of $\alpha\!s,\!x\!s.t$
699 one gets an element $\den{\alpha\!s,\!x\!s.t}_{M}(X\!s)(y\!s)$ of
700 $\den{\alpha\!s.\tau}_{M}(X\!s)$. The definition of
701 $\den{\alpha\!s,\!x\!s.t}_{M}$ proceeds by induction on the structure of
708 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
713 Suppose $t$ is a constant\index{constants, in HOL logic@constants, in \HOL{} logic!formal semantics of} $\con{c}_{\sigma'}$, where
714 $(\con{c},\sigma)\in\Sigma_{\Omega}$ and $\sigma'$ is an instance of
715 $\sigma$.  Then by Lemma~1 of \ref{instances-and-substitution},
722 which is an element of $\den{\alpha\!s.\tau}(X\!s)$ by Lemma~2 of
726 Suppose $t$ is a function application\index{combinations, in HOL logic@combinations, in \HOL{} logic!formal semantics of} term $(t_{1}\
727 t_{2})$\index{function application, in HOL logic@function application, in \HOL{} logic!formal semantics of} where $t_{1}$ is of type
728 $\tau'\fun\tau$ and $t_{2}$ is of type $\tau'$. Then
729 $f=\den{\alpha\!s,\!x\!s.t_{1}}(X\!s)(y\!s)$, being an element of
736 \item Suppose $t$ is the abstraction\index{function abstraction, in HOL logic@function abstraction, in \HOL{} logic!formal semantics of}
737 term $\lambda x.t_{2}$where $x$ is of type $\tau_{1}$ and $t_{2}$ of
741 Define $\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ to be the element of
749 Now define the meaning of a term $t_{\tau}$ in a model $M$ to be the
756 canonical context of $t_{\tau}$. So $n$ is the number of type variables in
757 $t_{\tau}$, $\alpha\!s$ is a list of those type variables, $m$ is the
758 number of ordinary variables occurring freely in $t_{\tau}$ (assumed to be
759 distinct from the bound variables of $t_{\tau}$) and the $\sigma_{j}$ are
760 the types of those variables. (It is important to note that the list
761 $\alpha\!s$, which is part of the canonical context of $t$, may be strictly
762 bigger than the canonical type contexts of $\sigma_{j}$ or $\tau$. So it
773 where $\alpha\!s$ is the list of type variables occurring in $t_{\tau}$ and
774 $n$ is the length of that list. If moreover, no type variables occur in
776 element $\den{t_{\tau}}()$ of the set $\den{\tau}\in{\cal U}$.
778 The semantics of terms appears somewhat complicated because of the
779 possible dependency of a term upon both type variables and ordinary
780 variables. Examples of how the definition of the semantics
782 of several terms denoting logical constants is given.
788 ordinary variables, there are two different operations of substitution
789 on terms which have to be considered---substitution of types for type
790 variables and substitution of terms for variables.
793 \index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!formal semantics of}
797 and where for $j=1,\ldots,m$ the type of the variable $x_j$ is
799 types-in-context, then substituting\index{type substitution, in HOL logic@type substitution, in \HOL{} logic!formal semantics of} the types
801 obtains a new list of variables $x\!s'$. Thus the $j$\/th entry of
805 In instantiating\index{types, in HOL logic@types, in \HOL{} logic!instantiation of} the type variables $\alpha\!s$ with the types
807 the list $x\!s'$.\footnote{Such an identification of variables could
814 variables $\alpha\!s$ in $t$ (with suitable renaming of bound
815 occurrences of variables to make them distinct from the variables in
825 The meaning of $\alpha\!s',\!x\!s'.t'$ in a model is  related to that
826 of $t$ as follows. For all $X\!s'\in{\cal U}^{n'}$ (where $n'$ is the
827 length of $\alpha\!s'$)}
837 sides of the above equation are elements of the same set of functions.
838 The validity of the equation is proved by induction on the structure
839 of the term $t$.
842 \index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!formal semantics of}
846 and where for $j=1,\ldots,m$ the type of the variable $x_j$ is
848 $j=1,\ldots,m$ with $t_{j}$ of the same type as $x_{j}$, say
852 renaming of bound occurrences of variables to prevent the free
853 variables of the $t_{j}$ becoming bound after substitution). The
863 The meaning of $\alpha\!s,\!x\!s'.t''$ in a model is related to that of
866 \den{\alpha\!s.\sigma'_{m'}}$ (where $\sigma'_{j}$ is the type of
876 Once again, this result is proved by induction on the structure of
882 Up to now the syntax of types and terms  has been  very general.   To
883 represent the standard  formulas  of  logic  it  is  necessary  to
887 of  truth-values.  Logical formulas are then identified with
888 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
890 requirements are  formalized  by  defining  the  notion  of  a
897 atomic types \ty{bool} (of booleans or truth-values) and \ty{ind} (of
899 instead of  \ty{bool} and $\iota$ instead of \ty{ind}.)
901 A model $M$ of $\Omega$ is {\em standard\/} if $M(\bool)$ and $M(\ind)$ are
910 \index{signatures, of HOL logic@signatures, of \HOL{} logic!standard}\index{standard signatures, of HOL logic@standard signatures, of \HOL{} logic}
913 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}:
923 The intended interpretation of these constants is that  $\imp$ denotes
927 on the set denoted by $\sigma$. More precisely, a model $M$ of
928 $\Sigma_{\Omega}$ will be called {\em standard\/}\index{standard models, of HOL logic@standard models, of \HOL{} logic} if
933 standard implication\index{implication, in HOL logic@implication, in \HOL{} logic!formal semantics of} function, sending $b,b'\in\two$ to
945 equality\index{equality, in HOL logic@equality, in \HOL{} logic!formal semantics of} test function, sending $x,x'\in X$ to
957 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
967 $\cal U$ when it is non-empty, by the property {\bf Sub} of the
979 This particular choice of primitive constants is arbitrary.  The
980 standard collection of logical constants includes $\T$ (`true'), $\F$
981 (`false')\index{truth values, in HOL logic@truth values, in \HOL{} logic!abstract form of}, $\imp$ (`implies'), $\wedge$ (`and'), $\vee$
986 necessary to work with the full set of logical constants, and the
993 Terms of type \ty{bool} are  called {\it formulas\/}\index{formulas as terms, in HOL logic@formulas as terms, in \HOL{} logic}.
998 \index{equality, in HOL logic@equality, in \HOL{} logic!abstract form of}
999 \index{implication, in HOL logic@implication, in \HOL{} logic!abstract form of}
1000 \index{choice operator, in HOL logic@choice operator, in \HOL{} logic!abstract form of}
1001 \index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abstract form of}
1002 \index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!abstract form of}
1016 These notations are special cases of general abbreviatory conventions

Indexes created Sun Jun 23 19:15:37 MDT 2024