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 4% Written by Andrew Pitts 5% 8 March 1991 6% revised August 1991 7\chapter{Syntax and Semantics}\label{logic} 8 9\section{Introduction} 10\label{introduction} 11 12This chapter describes the syntax and set-theoretic semantics of the 13logic supported by the \HOL{} system, which is a variant of 14Church's\index{Church, A.} simple theory of types \cite{Church} and 15will henceforth be called the \HOL{} logic, or just \HOL. The 16meta-language for this description will be English, enhanced with 17various mathematical notations and conventions. The object language 18of this description is the \HOL{} logic. Note that there is a 19`meta-language', in a different sense, associated with the \HOL\ 20logic, namely the programming language \ML. This is the language used 21to manipulate the \HOL{} logic by users of the system. It is hoped 22that because of context, no confusion results from these two uses of 23the word `meta-language'. When \ML\ is the object of study (as in 24\cite{sml}), \ML\ is the object language under consideration---and 25English is again the meta-language! 26 27The \HOL{} syntax contains syntactic categories of types and terms whose 28elements are intended to denote respectively certain sets and elements 29of sets. This set theoretic interpretation will be developed alongside 30the description of the \HOL{} syntax, and in the next chapter the \HOL\ 31proof system will be shown to be sound for reasoning about properties 32of the set theoretic model.\footnote{There are other, `non-standard' 33models of \HOL, which will not concern us here.} This model is given in 34terms of a fixed set of sets $\cal U$, which will be called the {\em 35universe\/}\index{universe, in semantics of HOL logic@universe, in 36semantics of \HOL{} logic} and which is assumed to have the following 37properties. 38\begin{description} 39 40\item[Inhab] Each element of $\cal U$ is a non-empty set. 41 42\item[Sub] If $X\in{\cal U}$ and $\emptyset\not=Y\subseteq X$, then 43$Y\in{\cal U}$. 44 45\item[Prod] If $X\in{\cal U}$ and $Y\in{\cal U}$, then $X\times 46Y\in{\cal U}$. The set $X\times Y$ is the cartesian product, 47consisting of ordered pairs $(x,y)$ with $x\in X$ and $y\in Y$, with 48the usual set-theoretic coding of ordered pairs, \viz\ 49$(x,y)=\{\{x\},\{x,y\}\}$. 50 51\item[Pow] If $X\in{\cal U}$, then the powerset 52$P(X)=\{Y:Y\subseteq X\}$ is also an element of $\cal U$. 53 54\item[Infty] $\cal U$ contains a distinguished infinite set $\inds$. 55 56\item[Choice] There is a distinguished element $\ch\in\prod_{X\in{\cal 57U}}X$. The elements of the product $\prod_{X\in{\cal U}}X$ are 58(dependently typed) functions: thus for all $X\in{\cal U}$, $X$ is 59non-empty by {\bf Inhab} and $\ch(X)\in X$ witnesses this. 60 61\end{description} 62There are some consequences of these assumptions which will be needed. 63In set theory functions are identified with their graphs, which are 64certain sets of ordered pairs. Thus the set $X\fun Y$ of all functions 65from a set $X$ to a set $Y$ is a subset of $P(X\times Y)$; and it is a 66non-empty set when $Y$ is non-empty. So {\bf Sub}, {\bf Prod} and {\bf 67Pow} together imply that $\cal U$ also satisfies 68\begin{description} 69 70\item[Fun] If $X\in{\cal U}$ and $Y\in{\cal U}$, then $X\fun Y\in{\cal U}$. 71 72\end{description} 73By iterating {\bf Prod}, one has that the cartesian product of any 74finite, 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 76say that it contains a one-element set (by virtue of {\bf Sub} applied 77to any set in ${\cal U}$---{\bf Infty} guarantees there is one); for 78definiteness, a particular one-element set will be singled out. 79\begin{description} 80 81\item[Unit] $\cal U$ contains a distinguished one-element set $1=\{0\}$. 82 83\end{description} 84Similarly, because of {\bf Sub} and {\bf Infty}, $\cal U$ contains 85two-element sets, one of which will be singled out. 86\begin{description} 87 88\item[Bool] $\cal U$ contains a distinguished two-element set 89$\two=\{0,1\}$. 90 91\end{description} 92 93The above assumptions on $\cal U$ are weaker than those imposed on a 94universe of sets by the axioms of 95Zermelo-Fraenkel\index{Zermelo-Fraenkel set theory} set theory with the 96Axiom of Choice (\theory{ZFC})\index{axiom of choice}\index{ZFC@\ml{ZFC}}, 97principally because $\cal U$ is not 98required to satisfy any form of the Axiom of 99Replacement\index{axiom of replacement}. 100Indeed, 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 103in the von~Neumann cumulative hierarchy formed before stage 104$\omega+\omega$.) Thus, as with many other pieces of mathematics, it is 105possible in principal to give a completely formal version within 106\theory{ZFC} set theory of the semantics of the \HOL{} logic to be given 107below. 108 109\section{Types} 110\label{types} 111 112The types\index{type constraint!in HOL logic@in \HOL{} logic} of the 113\HOL{} logic are expressions that denote sets (in the universe $\cal U$). 114Following tradition, 115$\sigma$, possibly decorated with subscripts or primes, is used to 116range over arbitrary types. 117 118There are four kinds of types in the \HOL{} logic. These can be described 119informally by the following {\small BNF} grammar, 120in which $\alpha$ ranges 121over type variables, \textsl{c} ranges over atomic types and \textsl{op} ranges over 122type operators. 123 124\newlength{\ttX} 125\settowidth{\ttX}{\tt X} 126\newcommand{\tyvar}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 127\put(.5,0){\makebox(0,0)[b]{\footnotesize type variables}} 128\put(0,1.5){\vector(0,1){4.5}} 129\end{picture}} 130\newcommand{\tyatom}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 131\put(.5,2.3){\makebox(0,0)[b]{\footnotesize atomic types}} 132\put(.5,3.3){\vector(0,1){2.6}} 133\end{picture}} 134\newcommand{\funty}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 135\put(.5,1.5){\makebox(0,0)[b]{\footnotesize function types}} 136\put(.5,0){\makebox(0,0)[b]{\footnotesize (domain $\sigma_1$, codomain $\sigma_2$)}} 137\put(1,2.5){\vector(0,1){3.5}} 138\end{picture}} 139\newcommand{\cmpty}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 140\put(2,3.3){\makebox(0,0)[b]{\footnotesize compound types}} 141\put(1.9,4.5){\vector(0,1){1.5}} 142\end{picture}} 143% 144$$\sigma\quad ::=\quad {\mathord{\mathop{\alpha}\limits_{\tyvar}}} 145 \quad\mid\quad{\mathord{\mathop{c}\limits_{\tyatom}}} 146 \quad\mid\quad\underbrace{(\sigma_1, \ldots , \sigma_n){op}}_{\cmpty} 147 \quad\mid\quad\underbrace{\sigma_1\fun\sigma_2}_{\funty}$$ 148 149\noindent In more detail, the four kinds of types are as follows. 150 151\begin{enumerate} 152 153\item {\bf Type variables:}\index{type variables, in HOL logic@type variables, in \HOL{} logic!abstract form of} these stand for arbitrary 154sets in the universe. In Church's original formulation of simple type 155theory, type variables are part of the meta-language and are used to 156range over object language types. Proofs containing type variables 157were understood as proof schemes (\ie\ families of proofs). To support 158such proof schemes {\it within} the \HOL{} logic, type variables have 159been added to the object language type system.\footnote{This technique 160was invented by Robin Milner for the object logic \PPL\ of his \LCF\ 161system.} 162 163\item {\bf Atomic types:}\index{atomic types, in HOL logic@atomic types, in \HOL{} logic} these denote fixed sets in the universe. Each 164theory determines a particular collection of atomic types. For 165example, the standard atomic types \ty{bool} and \ty{ind} denote, 166respectively, the distinguished two-element set $\two$ and the 167distinguished infinite set $\inds$. 168 169\item {\bf Compound types:}\index{compound types, in HOL logic@compound types, in \HOL{} logic!abstract form of} These have the 170form $(\sigma_1,\ldots,\sigma_n)\ty{op}$, where $\sigma_1$, $\dots$, 171$\sigma_n$ are the argument types and $op$ is a {\it type operator\/} 172of arity $n$. Type operators denote operations for constructing sets. 173The type $(\sigma_1,\ldots,\sigma_n)\ty{op}$ denotes the set resulting 174from applying the operation denoted by $op$ to the sets denoted by 175$\sigma_1$, $\dots$, $\sigma_n$. For example, 176\ty{list} is a type operator with arity 1. It denotes the operation 177of forming all finite lists of elements from a given set. Another 178example is the type operator \ty{prod} of arity 2 which denotes the 179cartesian product operation. The type $(\sigma_1,\sigma_2)\ty{prod}$ 180is written as $\sigma_1\times\sigma_2$. 181 182\item {\bf Function types:}\index{function types, in HOL logic@function types, in \HOL{} logic!abstract form of} If $\sigma_1$ 183and $\sigma_2$ are types, then $\sigma_1\fun\sigma_2$ is the function 184type with {\it domain\/} $\sigma_1$ and {\it codomain} $\sigma_2$. It 185denotes the set of all (total) functions from the set denoted by its 186domain to the set denoted by its codomain. (In the literature 187$\sigma_1\fun\sigma_2$ is written without the arrow and 188backwards---\ie\ as $\sigma_2\sigma_1$.) Note that syntactically 189$\fun$ is simply a distinguished type operator of arity 2 written with 190infix notation. It is singled out in the definition of \HOL{} types 191because it will always denote the same operation in any 192model of a \HOL{} theory---in contrast to the other type operators which 193may be interpreted differently in different models. (See 194Section~\ref{semantics of types}.) 195 196 197\end{enumerate} 198 199It turns out to be convenient to identify atomic types with 200compound types constructed with $0$-ary type operators. For example, 201the atomic type \ty{bool} of truth-values can be regarded as being an 202abbreviation for $()\ty{bool}$. This identification will be made in 203the technical details that follow, but in the informal presentation 204atomic types will continue to be distinguished from compound types, 205and $()c$ will still be written as $c$. 206 207\subsection{Type structures} 208\label{type structures} 209\index{type structure, in HOL logic@type structure, in \HOL{} logic} 210 211The term `type constant' is used to cover both atomic types and type 212operators. It is assumed that an infinite set {\sf 213TyNames} of the {\em names of type constants\/} is given. The greek 214letter $\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 216types (\ie\ $0$-ary type constants), and \textsl{op} is used to range 217over the names of type operators (\ie\ $n$-ary type constants, where 218$n>0$). 219 220It is assumed that an infinite set {\sf TyVars} of {\em type 221variables\/}\index{type variables, in HOL logic@type variables, in \HOL{} logic} 222 is given. Greek letters $\alpha,\beta,\ldots$, possibly with 223subscripts or primes, are used to range over {\sf Tyvars}. The sets 224{\sf TyNames} and {\sf TyVars} are assumed disjoint. 225 226A {\it type structure\/} is a set $\Omega$ of type constants. A {\it 227type constant\/}\index{type constants, in HOL logic@type constants, in \HOL{} logic} is a pair $(\nu,n)$ where $\nu\in{\sf TyNames}$ is the 228name of the constant and $n$ is its arity. Thus $\Omega\subseteq{\sf 229TyNames}\times\natnums$ (where $\natnums$ is the set of natural 230numbers). It is assumed that no two distinct type constants have the 231same name, 232\ie\ whenever $(\nu, n_1)\in\Omega$ and 233$(\nu, n_2)\in\Omega$, then $n_1 = n_2$. 234 235The set {\sf Types}$_{\Omega}$ of types over a structure ${\Omega}$ 236can now be defined as the smallest set such that: 237 238\begin{itemize} 239 240\item {\sf TyVars}$\ \subseteq\ ${\sf Types}$_{\Omega}$. 241 242\item If $(\nu,0)\in\Omega$ then $()\nu\in{\sf Types}_{\Omega}$. 243 244\item If $(\nu,n)\in\Omega$ and $\sigma_i\in{\sf Types}_{\Omega}$ for 245$1\leq i\leq n$, then $(\sigma_1,\ \ldots\ ,\sigma_n)\nu\in{\sf 246Types}_{\Omega}$. 247 248\item If $\sigma_1\in{\sf Types}_{\Omega}$ and $\sigma_2\in{\sf 249Types}_{\Omega}$ then $\sigma_1\fun\sigma_2\in{\sf Types}_{\Omega}$. 250 251 252\end{itemize} 253The type operator $\fun$ is assumed to associate\index{type operators, in HOL logic@type operators, in \HOL{} logic!associativity of} to the 254right, so that 255\[ 256\sigma_1\fun\sigma_2\fun\ldots\fun \sigma_n\fun\sigma 257\] 258abbreviates 259\[ 260\sigma_1\fun(\sigma_2\fun\ldots\fun (\sigma_n\fun\sigma)\ldots) 261\] 262The notation $tyvars(\sigma)$ is used to denote the set of type 263variables occurring in $\sigma$. 264 265\subsection{Semantics of types} 266\label{semantics of types} 267 268 269A {\em model} $M$ of a type structure $\Omega$ is specified by giving 270for each type constant $(\nu,n)$ an $n$-ary function 271\[ 272M(\nu):{\cal U}^{n}\longrightarrow{\cal U} 273\] 274Thus given sets $X_1,\ldots,X_n$ in the universe $\cal U$, 275$M(\nu)(X_1,\ldots,X_n)$ is also a set in the universe. In case $n=0$, 276this amounts to specifying an element $M(\nu)\in{\cal U}$ for the 277atomic type $\nu$. 278 279Types containing no type variables are called {\it monomorphic}, 280whereas those that do contain type variables are called {\it 281polymorphic}\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 282only say what set a polymorphic type denotes once one has instantiated 283its type variables to particular sets. So its overall meaning is not a 284single set, but is rather a set-valued function, ${\cal 285U}^{n}\longrightarrow{\cal U}$, assigning a set for each particular 286assignment of sets to the relevant type variables. The arity $n$ 287corresponds to the number of type variables involved. It is convenient 288in this connection to be able to consider a type variable to be 289involved in the semantics of a type $\sigma$ whether or not it 290actually occurs in $\sigma$, leading to the notion of a 291type-in-context. 292 293A {\em type context}\index{type context}, $\alpha\!s$, is simply a 294finite (possibly empty) list of {\em distinct\/} type variables 295$\alpha_{1},\ldots,\alpha_{n}$. A {\em 296type-in-context\/}\index{type-in-context} is a pair, written 297$\alpha\!s.\sigma$, where $\alpha\!s$ is a type context, $\sigma$ is a 298type (over some given type structure) and all the type variables 299occurring in $\sigma$ appear somewhere in the list $\alpha\!s$. The 300list $\alpha\!s$ may also contain type variables which do not occur in 301$\sigma$. 302 303For each $\sigma$ there are minimal contexts $\alpha\!s$ for which 304$\alpha\!s.\sigma$ is a type-in-context, which only differ by the order 305in which the type variables of $\sigma$ are listed in $\alpha\!s$. In 306order to select one such context, let us assume that {\sf TyVars} 307comes with a fixed total order and define the {\em 308canonical}\index{canonical contexts, in HOL logic@canonical contexts, in \HOL{} logic!of types} context of the type $\sigma$ to consist of 309exactly the type variables it contains, listed in order.\footnote{It is 310possible to work with unordered contexts, specified by finite sets 311rather than lists, but we choose not to do that since it mildly 312complicates the definition of the semantics to be given 313below.} 314 315Let $M$ be a model of a type structure $\Omega$. For each 316type-in-context 317$\alpha\!s.\sigma$ over $\Omega$, define a function 318\[ 319\den{\alpha\!s.\sigma}_{M}:{\cal U}^{n}\longrightarrow{\cal U} 320\] 321(where $n$ is the length of the context) by induction on the structure 322of $\sigma$ as follows. 323\begin{itemize} 324 325\item If $\sigma$ is a type variable, it must be $\alpha_{i}$ for some unique 326$i=1,\ldots,n$ and then $\den{\alpha\!s.\sigma}_{M}$ is the $i$\/th 327projection function, which sends $(X_{1},\ldots,X_{n})\in{\cal U}^{n}$ 328to $X_{i}\in{\cal U}$. 329 330\item If $\sigma$ is a function type\index{function types, in HOL logic@function types, in \HOL{} logic!formal semantics of} 331$\sigma_{1}\fun\sigma_{2}$, then $\den{\alpha\!s.\sigma}_M$ sends 332$X\!s\in{\cal U}^n$ to the set of all functions 333from $\den{\alpha\!s.\sigma_1}_M(X\!s)$ to 334$\den{\alpha\!s.\sigma_2}_M(X\!s)$. (This makes 335use of the property {\bf Fun} of $\cal U$.) 336 337\item If $\sigma$ is a 338compound type $(\sigma_{1},\ldots,\sigma_{m})\nu$, then 339$\den{\alpha\!s.\sigma}_{M}$ sends $X\!s$ to 340$M(\nu)(S_{1},\ldots,S_{m})$ where each $S_{j}$ is 341$\den{\alpha\!s.\sigma_{j}}_{M}(X\!s)$. 342\end{itemize} 343One can now define the meaning of a type $\sigma$ in a model $M$ to be 344the function 345\[ 346\den{\sigma}_{M}:{\cal U}^{n}\longrightarrow{\cal U} 347\] 348given by $\den{\alpha\!s.\sigma}_{M}$, where $\alpha\!s$ is the 349canonical context of $\sigma$. If $\sigma$ is monomorphic, then $n=0$ 350and $\den{\sigma}_{M}$ can be identified with the element 351$\den{\sigma}_{M}()$ of $\cal U$. When the particular model $M$ is 352clear from the context, $\den{\_}_{M}$ will be written $\den{\_}$. 353 354To summarize, given a model in $\cal U$ of a type structure $\Omega$, 355the semantics interprets monomorphic types over $\Omega$ as sets in 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 357U}^{n}\longrightarrow{\cal U}$ on the universe. Function types are 358interpreted by full function sets. 359 360\medskip 361 362\noindent{\bf Examples\ } 363Suppose that $\Omega$ contains a type constant $(\textsl{b},0)$ and that 364the model $M$ assigns the set $\two$ to $\textsl{b}$. Then: 365\begin{enumerate} 366 367\item $\den{\textsl{b}\fun\textsl{b}\fun\textsl{b}}=\two\fun\two\fun\two\in{\cal U}$. 368 369\item $\den{(\alpha\fun\textsl{b})\fun\alpha}:{\cal U}\longrightarrow{\cal U}$ 370is the function sending $X\in{\cal U}$ to $(X\fun\two)\fun X\in{\cal U}$. 371 372\item $\den{\alpha,\beta . (\alpha\fun\textsl{b})\fun\alpha}:{\cal 373U}^{2}\longrightarrow{\cal U}$ is the function sending $(X,Y)\in{\cal 374U}^{2}$ to $(X\fun\two)\fun X\in{\cal U}$. 375 376\end{enumerate} 377 378\medskip 379 380\noindent{\bf Remark\ } 381A more traditional approach to the semantics would involve giving 382meanings 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 384the same as using partial environments with finite domains---it is 385just that the context ties down the admissible domain to a particular 386finite (ordered) set of type variables. At the level of types there is 387not much to choose between the two approaches. However for the syntax 388and semantics of terms to be given below, where there is a dependency 389both on type variables and on individual variables, the approach used 390here seems best. 391 392\subsection{Instances and substitution} 393\label{instances-and-substitution} 394 395If $\sigma$ and $\tau_1,\ldots,\tau_n$ are types over a type structure 396$\Omega$, 397\[ 398\sigma[\tau_{1},\ldots,\tau_{p}/\beta_{1},\ldots,\beta_{p}] 399\] 400will denote the type resulting from the simultaneous substitution for 401each $i=1,\ldots,p$ of 402$\tau_i$ for the type variable $\beta_i$ in $\sigma$. 403The resulting type is called an {\it instance\/}\index{types, in HOL logic@types, in \HOL{} logic!instantiation of} of $\sigma$. The 404following lemma about instances will be useful later; it is proved by 405induction on the structure of $\sigma$. 406 407\medskip 408 409\noindent{\bf Lemma 1\ }{\it 410Suppose that $\sigma$ is a type containing distinct type variables 411$\beta_1,\ldots,\beta_p$ and that 412$\sigma'=\sigma[\tau_{1},\ldots,\tau_{n}/\beta_1,\ldots,\beta_p]$ is 413an instance of $\sigma$. Then the types $\tau_1,\ldots,\tau_p$ are 414uniquely determined by $\sigma$ and $\sigma'$.} 415 416\medskip 417 418We also need to know how the semantics of types behaves with respect 419to substitution: 420 421\medskip 422 423\noindent{\bf Lemma 2\ }{\it Given types-in-context $\beta\!s.\sigma$ and 424$\alpha\!s.\tau_i$ ($i=1,\ldots,p$, where $p$ is the 425length of $\beta\!s$), let $\sigma'$ be the instance 426$\sigma[\tau\!s/\beta\!s]$. Then $\alpha\!s.\sigma'$ is also a 427type-in-context and its meaning in any model $M$ is related to that of 428$\beta\!s.\sigma$ as follows. For all $X\!s\in{\cal U}^n$ (where $n$ 429is the length of $\alpha\!s$) 430\[ 431\den{\alpha\!s.\sigma'}(X\!s) = 432\den{\beta\!s.\sigma}(\den{\alpha\!s.\tau_{1}}(X\!s), 433 \ldots ,\den{\alpha\!s.\tau_{p}}(X\!s)) 434\] 435} 436Once again, the lemma can be proved by induction on the structure of 437$\sigma$. 438 439\section{Terms} 440\label{terms} 441 442The terms of the \HOL{} logic are expressions that denote elements of the sets 443denoted by types. The meta-variable $t$ 444is used to range over arbitrary terms, possibly decorated 445with subscripts or primes. 446 447There are four kinds of terms in the \HOL{} logic. These can be 448described approximately by the following {\small BNF} grammar, in 449which $x$ ranges over variables and $c$ ranges over constants. 450\index{combinations, in HOL logic@combinations, in \HOL{} logic!abstract form of} 451 452\settowidth{\ttX}{\tt X} 453\newcommand{\var}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 454\put(.5,0){\makebox(0,0)[b]{\footnotesize variables}} 455\put(0,1.5){\vector(0,1){4.5}} 456\end{picture}} 457\newcommand{\const}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 458\put(.5,2.3){\makebox(0,0)[b]{\footnotesize constants}} 459\put(.5,3.5){\vector(0,1){2.4}} 460\end{picture}} 461\newcommand{\app}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 462\put(.5,1.5){\makebox(0,0)[b]{\footnotesize function applications}} 463\put(.5,0){\makebox(0,0)[b]{\footnotesize (function $t$, argument $t'$)}} 464\put(0.5,2.5){\vector(0,1){3.5}} 465\end{picture}} 466\newcommand{\abs}{\setlength{\unitlength}{\ttX}\begin{picture}(1,6) 467\put(1,3.3){\makebox(0,0)[b]{\footnotesize $\lambda$-abstractions}} 468\put(0.7,4.5){\vector(0,1){1.5}} 469\end{picture}} 470% 471$$ t \quad ::=\quad {\mathord{\mathop{x}\limits_{\var}}} 472 \quad\mid\quad{\mathord{\mathop{\con{c}}\limits_{\const}}} 473 \quad\mid\quad\underbrace{t\ t'}_{\app} 474 \quad\mid\quad\underbrace{\lambda x .\ t}_{\abs}$$ 475 476Informally, 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 477a function $v\mapsto t[v/x]$, where $t[v/x]$ denotes the result of 478substituting $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 479function denoted by $t$ to the value denoted by $t'$. This will be 480made more precise below. 481 482The {\small BNF} grammar just given omits mention of types. In fact, each 483term in 484the \HOL{} logic is associated with a unique type. 485The notation $t_{\sigma}$ is 486traditionally used to range over terms of type $\sigma$. A 487more accurate grammar of 488terms is: 489 490$$ t_{\sigma} \quad ::=\quad {\mathord{\mathop{x_{\sigma}}\limits_{}}} 491\quad\mid\quad 492{\mathord{\mathop{\con{c}_{\sigma}}\limits_{}}} 493\quad\mid\quad (t_{\sigma'\fun\sigma}\ t'_{\sigma'})_{\sigma} 494\quad\mid\quad(\lambda x_{\sigma_1} .\ t_{\sigma_2}) 495_{\sigma_1\fun\sigma_2}$$\index{constants, in HOL logic@constants, in \HOL{} logic!abstract form of} 496 497In fact, just as the definition of types was relative to a particular 498type structure $\Omega$, the formal definition of terms is relative to 499a given collection of typed constants over $\Omega$. Assume that an 500infinite set {\sf Names} of names is given. A {\em constant\/} over 501$\Omega$ is a pair $(\con{c}, \sigma)$, where $\con{c}\in{\sf Names}$ 502and $\sigma\in{\sf Types}_{\Omega}$. A {\em signature} over $\Omega$ 503is just a set $\Sigma_\Omega$ of such constants. 504 505The set {\sf Terms}$_{\Sigma_{\Omega}}$ of terms over 506$\Sigma_{\Omega}$ is defined to be the smallest set closed under the 507following rules of formation: 508\begin{enumerate} 509 510\item {\bf Constants:} If $(\con{c},\sigma)\in{\Sigma_{\Omega}}$ and 511$\sigma'\in{\sf Types}_{\Omega}$ 512is an instance of $\sigma$, then $(\con{c},{\sigma'})\in{\sf 513Terms}_{\Sigma_{\Omega}}$. Terms formed in this way are called {\it 514constants\/}\index{constants, in HOL logic@constants, in \HOL{} logic!abstract form of} and are written $\con{c}_{\sigma'}$. 515 516\item {\bf Variables:} If $x\in{\sf Names}$ and $\sigma\in{\sf 517Types}_{\Omega}$, then ${\tt var}\ x_{\sigma}\in{\sf 518Terms}_{\Sigma_{\Omega}}$. Terms formed in this way are called {\it 519variables}\index{variables, in HOL logic@variables, in \HOL{} logic!abstract form of}. The marker {\tt var}\ is purely a device to 520distinguish variables from constants with the same name. A variable 521${\tt var}\ x_{\sigma}$ will usually be written as $x_{\sigma}$, if it 522is clear from the context that $x$ is a variable rather than a 523constant. 524 525\item {\bf Function applications:} If $t_{\sigma'{\fun}\sigma}\in{\sf 526Terms}_{\Sigma_{\Omega}}$ and $t'_{\sigma'}\in{\sf 527Terms}_{\Sigma_{\Omega}}$, then $(t_{\sigma'\fun\sigma}\ 528t'_{\sigma'})_{\sigma}\in {\sf Terms}_{\Sigma_{\Omega}}$. 529(Terms formed in this way are sometimes called {\it combinations}.) 530 531\item {\bf $\lambda$-Abstractions:} If ${\tt var}\ x_{\sigma_1} 532\in{\sf Terms}_{\Sigma_{\Omega}}$ and $t_{\sigma_2}\in{\sf 533Terms}_{\Sigma_{\Omega}}$, then $(\lambda x_{\sigma_1}.\ 534t_{\sigma_2})_{\sigma_1\fun\sigma_2} 535\in{\sf Terms}_{\Sigma_{\Omega}}$. 536 537\end{enumerate} 538 539Note that it is possible for constants and variables\index{variables, in HOL logic@variables, in \HOL{} logic!with same names} to have the 540same name. It is also possible for different variables to have the 541same name, if they have different types. 542 543The type subscript on a term may be omitted if it is clear from the 544structure of the term or the context in which it occurs what its type 545must be. 546 547Function application\index{function application, in HOL logic@function application, in \HOL{} logic!associativity of} is assumed to associate 548to the left, so that $t\ t_1\ t_2\ \ldots\ t_n$ abbreviates $(\ 549\ldots\ ((t\ t_1)\ t_2)\ \ldots\ t_n)$. 550 551The notation $\lambda x_1\ x_2\ \cdots\ x_n.\ t$ abbreviates $\lambda 552x_1.\ (\lambda x_2.\ \cdots\ (\lambda x_n.\ t)\ \cdots\ )$. 553 554A term is called polymorphic\index{polymorphic terms, in HOL logic@polymorphic terms, in \HOL{} logic} if it contains a type 555variable. Otherwise it is called monomorphic. Note that a term 556$t_{\sigma}$ may be polymorphic even though $\sigma$ is 557monomorphic --- for example, 558$(f_{\alpha\fun\textsl{b}}\ x_{\alpha})_{\textsl{b}}$, where $\textsl{b}$ is an atomic type. The expression 559$tyvars(t_{\sigma})$ denotes the set of type variables occurring in 560$t_{\sigma}$. 561 562An occurrence of a variable $x_{\sigma}$ is called {\it 563bound\/}\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 565$\lambda x_{\sigma}$, otherwise the occurrence is called {\it 566free\/}\index{free variables, in HOL logic@free variables, in \HOL{} logic!abstract form of}. Note that $\lambda x_{\sigma}$ does not bind 567$x_{\sigma'}$ if $\sigma\neq \sigma'$. A term in which all occurrences 568of variables are bound is called {\it closed\/}. 569 570\subsection{Terms-in-context} 571\label{terms-in-context} 572 573A {\em context\/}\index{contexts, in semantics of HOL logic@contexts, in semantics of \HOL{} logic} $\alpha\!s,\!x\!s$ consists of a type 574context $\alpha\!s$ together with a list $x\!s=x_{1},\ldots,x_{m}$ of 575distinct variables whose types only contain type variables from the 576list $\alpha\!s$. 577 578The condition that $x\!s$ contains {\em distinct\/} variables needs 579some comment. Since a variable is specified by both a name and a 580type, it is permitted for $x\!s$ to contain repeated 581names\index{variables, in HOL logic@variables, in \HOL{} logic!with same names}, 582 so long as different types are attached to the 583names. This aspect of the syntax means that one has to proceed with 584caution when defining the meaning of type variable instantiation, 585since instantiation may cause variables to become equal 586`accidentally': see Section~\ref{term-substitution}. 587 588A {\em term-in-context\/}\index{term-in-context} 589$\alpha\!s,\!x\!s.t$ consists of a context together with a term 590$t$ satisfying the following conditions. 591\begin{itemize} 592 593\item $\alpha\!s$ contains any type variable that occurs in $x\!s$ and $t$. 594 595\item $x\!s$ contains any variable that occurs freely in $t$. 596 597\item $x\!s$ does not contain any variable that occurs 598bound in $t$. 599 600\end{itemize} 601The context $\alpha\!s,\!x\!s$ may contain (type) variables which do 602not appear in $t$. Note that the combination of the second and third 603conditions implies that a variable cannot have both free and bound 604occurrences in $t$. For an arbitrary term, there is always an 605$\alpha$-equivalent term which satisfies this condition, obtained by 606renaming the bound variables as necessary.\footnote{Recall that two 607terms are said to be $\alpha$-equivalent if they differ only in the 608names of their bound variables.} In the semantics of terms to be given 609below we will restrict attention to such terms. Then the meaning of an 610arbitrary term is taken to be the meaning of some $\alpha$-variant of 611it having no variable both free and bound. (The semantics will equate 612$\alpha$-variants, so it does not matter which is chosen.) Evidently 613for such a term there is a minimal context $\alpha\!s,\!x\!s$, unique 614up to the order in which variables are listed, for which 615$\alpha\!s,\!x\!s.t$ is a term-in-context. As for type variables, we 616will assume given a fixed total order on variables. Then the unique 617minimal context with variables listed in order will be called the {\em 618canonical}\index{canonical contexts, in HOL logic@canonical contexts, in \HOL{} logic!of terms} context of the term $t$. 619 620\subsection{Semantics of terms} 621\label{semantics of terms} 622 623Let $\Sigma_{\Omega}$ be a signature\index{signatures, of HOL logic@signatures, of \HOL{} logic!formal semantics of} over a type 624structure $\Omega$ (see Section~\ref{terms}). A {\em model\/} $M$ of 625$\Sigma_{\Omega}$ is specified by a model of the type structure plus 626for each constant\index{primitive constants, of HOL logic@primitive constants, of \HOL{} logic} $(\con{c},\sigma)\in\Sigma_{\Omega}$ an 627element 628\[ 629M(\con{c},\sigma) \in 630\prod_{X\!s\in{\cal U}^{n}}\den{\sigma}_{M}(X\!s) 631\] 632of the indicated cartesian product, where $n$ is the number of type 633variables occurring in $\sigma$. In other words 634$M(\con{c},\sigma)$ is a (dependently typed) function 635assigning to each $X\!s\in{\cal U}^{n}$ an element of 636$\den{\sigma}_{M}(X\!s)$. In the case that $n=0$ (so that 637$\sigma$ is monomorphic), $\den{\sigma}_{M}$ was identified 638with a set in $\cal U$ and then $M(c,\sigma)$ can be 639identified with an element of that set. 640 641The meaning of \HOL{} terms in such a model will now be described. The 642semantics interprets closed terms involving no type variables as 643elements of sets in $\cal U$ (the particular set involved being derived 644from the type of the term as in Section~\ref{semantics of types}). More 645generally, if the closed term involves $n$ type variables then it is 646interpreted as an element of a product $\prod_{X\!s\in{\cal 647U}^{n}}Y(X\!s)$, where the function $Y:{\cal U}^{n}\longrightarrow{\cal 648U}$ is derived from the type of the term (in a type context derived 649from the term). Thus the meaning of the term is a (dependently typed) 650function which, when applied to any meanings chosen for the type 651variables in the term, yields a meaning for the term as an element of a 652set in $\cal U$. On the other hand, if the term involves $m$ free 653variables but no type variables, then it is interpreted as a function 654$Y_1\times\cdots\times Y_m\fun Y$ where the sets $Y_1,\ldots,Y_m$ in 655$\cal U$ are the interpretations of the types of the free variables in 656the term and the set $Y\in{\cal U}$ is the interpretation of the type 657of the term; thus the meaning of the term is a function which, when 658applied to any meanings chosen for the free variables in the term, 659yields a meaning for the term. Finally, the most general case is of a 660term involving $n$ type variables and $m$ free variables: it is 661interpreted as an element of a product 662\[ 663\prod_{X\!s\in{\cal 664U}^{n}}Y_{1}(X\!s)\times\cdots\times Y_{m}(X\!s) \;\fun\; Y(X\!s) 665\] 666where the functions $Y_{1},\ldots,Y_{m},Y:{\cal 667U}^{n}\longrightarrow{\cal U}$ are determined by the types of the free 668variables and the type of the term (in a type context derived from the 669term). 670 671More precisely, given a term-in-context $\alpha\!s,\!x\!s.t$ 672over $\Sigma_{\Omega}$ suppose 673\begin{itemize} 674 675\item $t$ has type $\tau$ 676 677\item $x\!s=x_{1},\ldots,x_{m}$ and each $x_{j}$ has type $\sigma_{j}$ 678 679\item $\alpha\!s=\alpha_{1},\ldots,\alpha_{n}$. 680 681\end{itemize} 682Then since $\alpha\!s,\!x\!s.t$ is a term-in-context, $\alpha\!s.\tau$ 683and $\alpha\!s.\sigma_{j}$ are types-in-context, and hence give rise 684to functions $\den{\alpha\!s.\tau}_{M}$ and 685$\den{\alpha\!s.\sigma_{j}}_{M}$ from ${\cal U}^{n}$ to $\cal U$ as in 686section~\ref{semantics of types}. The meaning of $\alpha\!s,\!x\!s.t$ 687in the model $M$ will be given by an element 688\[ 689\den{\alpha\!s,\!x\!s.t}_{M} \in \prod_{X\!s\in{\cal U}^{n}} 690\left(\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}_{M}(X\!s)\right) 691\fun \den{\alpha\!s.\tau}_{M}(X\!s) . 692\] 693In other words, given 694\begin{eqnarray*} 695X\!s & = & (X_{1},\ldots,X_{n})\in{\cal U}^{n} \\ 696y\!s & = & (y_{1},\ldots,y_{m})\in\den{\alpha\!s.\sigma_{1}}_{M}(X\!s) 697 \times\cdots\times \den{\alpha\!s.\sigma_{m}}_{M}(X\!s) 698\end{eqnarray*} 699one 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 702the term $t$, as follows. (As before, the subscript $M$ will be dropped from 703the semantic brackets $\den{ \_ }$ when the particular model involved is 704clear from the context.) 705\begin{itemize} 706 707\item 708If $t$ is a variable\index{variables, in HOL logic@variables, in \HOL{} logic!formal semantics of}, it must be $x_{j}$ for some unique 709$j=1,\ldots,m$, so $\tau=\sigma_{j}$ and then 710$\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ is defined to be $y_{j}$. 711 712\item 713Suppose $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}, 716$\sigma'=\sigma[\tau_{1},\ldots,\tau_{p}/\beta_{1},\ldots,\beta_{p}]$ 717for uniquely determined types $\tau_{1},\ldots,\tau_{p}$ (where 718$\beta_{1},\ldots,\beta_{p}$ are the type variables occurring in 719$\sigma$). Then define $\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ to be 720$M(\con{c},\sigma)(\den{\alpha\!s.\tau_{1}}(X\!s), 721\ldots,\den{\alpha\!s.\tau_{p}}(X\!s))$, 722which is an element of $\den{\alpha\!s.\tau}(X\!s)$ by Lemma~2 of 723\ref{instances-and-substitution} (since $\tau$ is $\sigma'$). 724 725\item 726Suppose $t$ is a function application\index{combinations, in HOL logic@combinations, in \HOL{} logic!formal semantics of} term $(t_{1}\ 727t_{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 730$\den{\alpha\!s.\tau'\fun\tau}(X\!s)$, is a function from the set 731$\den{\alpha\!s.\tau'}(X\!s)$ to the set $\den{\alpha\!s.\tau}(X\!s)$ 732which one can apply to the element 733$y=\den{\alpha\!s,\!x\!s.t_{2}}(X\!s)(y\!s)$. Define 734$\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ to be $f(y)$. 735 736\item Suppose $t$ is the abstraction\index{function abstraction, in HOL logic@function abstraction, in \HOL{} logic!formal semantics of} 737term $\lambda x.t_{2}$where $x$ is of type $\tau_{1}$ and $t_{2}$ of 738type $\tau_{2}$. Thus $\tau=\tau_{1}\fun\tau_{2}$ and 739$\den{\alpha\!s.\tau}(X\!s)$ is the function set 740$\den{\alpha\!s.\tau_{1}}(X\!s)\fun\den{\alpha\!s.\tau_{2}}(X\!s)$. 741Define $\den{\alpha\!s,\!x\!s.t}(X\!s)(y\!s)$ to be the element of 742this set which is the function sending 743$y\in\den{\alpha\!s.\tau_{1}}(X\!s)$ to 744$\den{\alpha\!s,\!x\!s,\!x.t_{2}}(X\!s)(y\!s,y)$. (Note that since 745$\alpha\!s,\!x\!s.t$ is a term-in-context, by convention the bound 746variable $x$ does not occur in $x\!s$ and thus 747$\alpha\!s,\!x\!s,\!x.t_{2}$ is also a term-in-context.) 748\end{itemize} 749Now define the meaning of a term $t_{\tau}$ in a model $M$ to be the 750dependently typed function 751\[ \den{t_{\tau}} \in \prod_{X\!s\in{\cal U}^{n}} 752 \left(\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}(X\!s)\right) 753 \fun \den{\alpha\!s.\tau}(X\!s) 754\] 755given by $\den{\alpha\!s,\!x\!s.t_{\tau}}$, where $\alpha\!s,\!x\!s$ is the 756canonical 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 758number of ordinary variables occurring freely in $t_{\tau}$ (assumed to be 759distinct from the bound variables of $t_{\tau}$) and the $\sigma_{j}$ are 760the 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 762bigger than the canonical type contexts of $\sigma_{j}$ or $\tau$. So it 763would not make sense to write just $\den{\sigma_{j}}$ or $\den{\tau}$ in 764the above definition.) 765 766If $t_{\tau}$ is a closed term, then $m=0$ and for each $X\!s\in{\cal 767U}^{n}$ one can identify $\den{t_{\tau}}$ with the element 768$\den{t_{\tau}}(X\!s)()\in\den{\alpha\!s.\tau}(X\!s)$. So for closed terms 769one gets 770\[ \den{t_{\tau}} \in \prod_{X\!s\in{\cal U}^{n}} 771\den{\alpha\!s.\tau}(X\!s) 772\] 773where $\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 775$t_{\tau}$, then $n=0$ and $\den{t_{\tau}}$ can be identified with the 776element $\den{t_{\tau}}()$ of the set $\den{\tau}\in{\cal U}$. 777 778The semantics of terms appears somewhat complicated because of the 779possible dependency of a term upon both type variables and ordinary 780variables. Examples of how the definition of the semantics 781works in practice can be found in Section~\ref{LOG}, where the meaning 782of several terms denoting logical constants is given. 783 784\subsection{Substitution} 785\label{term-substitution} 786 787Since terms may involve both type variables and 788ordinary variables, there are two different operations of substitution 789on terms which have to be considered---substitution of types for type 790variables and substitution of terms for variables. 791 792\subsubsection*{Substituting types for type variables in terms} 793\index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!formal semantics of} 794 795Suppose $t$ is a term, with canonical context $\alpha\!s,\!x\!s$ say, 796where $\alpha\!s = \alpha_1,\ldots,\alpha_n$, $x\!s = x_1,\ldots,x_m$ 797and where for $j=1,\ldots,m$ the type of the variable $x_j$ is 798$\sigma_j$. If $\alpha\!s'.\tau_{i}$ ($i=1,\ldots,n$) are 799types-in-context, then substituting\index{type substitution, in HOL logic@type substitution, in \HOL{} logic!formal semantics of} the types 800$\tau_{i}$ for the type variables $\alpha_{i}$ in the list $x\!s$, one 801obtains a new list of variables $x\!s'$. Thus the $j$\/th entry of 802$x\!s'$ has type $\sigma'_{j} = \sigma_{j}[\tau\!s/\alpha\!s]$. Only 803substitutions with the following property will be considered. 804\begin{quote} 805In instantiating\index{types, in HOL logic@types, in \HOL{} logic!instantiation of} the type variables $\alpha\!s$ with the types 806$\tau\!s$, no two distinct variables in the list $x\!s$ become equal in 807the list $x\!s'$.\footnote{Such an identification of variables could 808occur if the variables had the same name component and their types 809became equal on instantiation.} 810\end{quote} 811This condition ensures that $\alpha\!s',x\!s'$ really is a context. Then 812one obtains a new term-in-context $\alpha\!s',\!x\!s'.t'$ by 813substituting the types $\tau\!s=\tau_{1},\ldots,\tau_{n}$ for the type 814variables $\alpha\!s$ in $t$ (with suitable renaming of bound 815occurrences of variables to make them distinct from the variables in 816$x\!s'$). The notation 817\[ 818t[\tau\!s/\alpha\!s] 819\] 820is used for the term $t'$. 821 822\medskip 823 824\noindent{\bf Lemma 3\ }{\it 825The meaning of $\alpha\!s',\!x\!s'.t'$ in a model is related to that 826of $t$ as follows. For all $X\!s'\in{\cal U}^{n'}$ (where $n'$ is the 827length of $\alpha\!s'$)} 828\[ 829\den{\alpha\!s',\!x\!s'.t'}(X\!s') = 830 \den{t}(\den{\alpha\!s'.\tau_{1}}(X\!s'),\ldots, 831 \den{\alpha\!s'.\tau_{n}}(X\!s')). 832\] 833 834\medskip 835 836Lemma~2 in \ref{instances-and-substitution} is needed to see that both 837sides of the above equation are elements of the same set of functions. 838The validity of the equation is proved by induction on the structure 839of the term $t$. 840 841\subsubsection*{Substituting terms for variables in terms} 842\index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!formal semantics of} 843 844Suppose $t$ is a term, with canonical context $\alpha\!s,\!x\!s$ say, 845where $\alpha\!s = \alpha_1,\ldots,\alpha_n$, $x\!s = x_1,\ldots,x_m$ 846and where for $j=1,\ldots,m$ the type of the variable $x_j$ is 847$\sigma_j$. If one has terms-in-context $\alpha\!s,\!x\!s'.t_{j}$ for 848$j=1,\ldots,m$ with $t_{j}$ of the same type as $x_{j}$, say 849$\sigma_{j}$, then one obtains a new term-in-context 850$\alpha\!s,\!x\!s'.t''$ by substituting the terms 851$t\!s=t_1,\ldots,t_m$ for the variables $x\!s$ in $t$ (with suitable 852renaming of bound occurrences of variables to prevent the free 853variables of the $t_{j}$ becoming bound after substitution). The 854notation 855\[ 856t[t\!s/x\!s] 857\] 858is used for the term $t''$. 859 860\medskip 861 862\noindent{\bf Lemma 4\ }{\it 863The meaning of $\alpha\!s,\!x\!s'.t''$ in a model is related to that of 864$t$ as follows. For all $X\!s\in{\cal U}^{n}$ and all 865$y\!s'\in\den{\alpha\!s.\sigma'_{1}} \times\cdots\times 866\den{\alpha\!s.\sigma'_{m'}}$ (where $\sigma'_{j}$ is the type of 867$x'_{j}$)} 868\[ 869\den{\alpha\!s,\!x\!s'.t''}(X\!s)(y\!s') = \den{t}(X\!s)( 870\den{\alpha\!s,\!x\!s'.t_{1}}(X\!s)(y\!s'),\ldots, 871\den{\alpha\!s,\!x\!s'.t_{m}}(X\!s)(y\!s')) 872\] 873 874\medskip 875 876Once again, this result is proved by induction on the structure of 877the term $t$. 878 879 880\section{Standard notions} 881 882Up to now the syntax of types and terms has been very general. To 883represent the standard formulas of logic it is necessary to 884impose some specific structure. In particular, every type structure 885must contain an atomic type \ty{bool} which is intended to denote 886the distinguished two-element set $\two\in{\cal U}$, regarded as a set 887of truth-values. Logical formulas are then identified with 888terms\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 889logical constants are assumed to be in all signatures. These 890requirements are formalized by defining the notion of a 891standard signature. 892 893\subsection{Standard type structures} 894\label{standard-type-structures} 895 896A type structure $\Omega$ is {\em standard\/} if it contains the 897atomic types \ty{bool} (of booleans or truth-values) and \ty{ind} (of 898individuals). (In the literature, the symbol $o$ is often used 899instead of \ty{bool} and $\iota$ instead of \ty{ind}.) 900 901A model $M$ of $\Omega$ is {\em standard\/} if $M(\bool)$ and $M(\ind)$ are 902respectively the distinguished sets $\two$ and $\inds$ in the universe 903$\cal U$. 904 905It will be assumed from now on that type structures and their models 906are standard. 907 908\subsection{Standard signatures} 909\label{standard-signatures} 910\index{signatures, of HOL logic@signatures, of \HOL{} logic!standard}\index{standard signatures, of HOL logic@standard signatures, of \HOL{} logic} 911 912A signature $\Sigma_{\Omega}$ is {\em standard\/} if it contains the 913following 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}: 914\[ 915{\imp}_{\ty{bool}\fun\ty{bool}\fun\ty{bool}} 916\] 917\[ 918{=}_{\alpha\fun\alpha\fun\ty{bool}} 919\] 920\[ 921\hilbert_{(\alpha\fun\ty{bool})\fun\alpha} 922\] 923The intended interpretation of these constants is that $\imp$ denotes 924implication, $=_{\sigma\fun\sigma\fun\ty{bool}}$ denotes equality on 925the set denoted by $\sigma$, and 926$\hilbert_{(\sigma\fun\ty{bool})\fun\sigma}$ denotes a choice function 927on 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 929\begin{itemize} 930 931\item 932$M({\imp},\bool\fun\bool\fun\bool)\in(\two\fun\two\fun\two)$ is the 933standard implication\index{implication, in HOL logic@implication, in \HOL{} logic!formal semantics of} function, sending $b,b'\in\two$ to 934\[ 935(b\imp b') = \left\{ \begin{array}{ll} 936 0 & \mbox{if $b=1$ and $b'=0$} \\ 937 1 & \mbox{otherwise} 938 \end{array} 939 \right.%} 940\] 941 942\item 943$M({=},\alpha\fun\alpha\fun\bool)\in\prod_{X\in{\cal U}}.X\fun 944X\fun\two$ is the function assigning to each $X\in{\cal U}$ the 945equality\index{equality, in HOL logic@equality, in \HOL{} logic!formal semantics of} test function, sending $x,x'\in X$ to 946\[ 947(x=_{X}x') = \left\{ \begin{array}{ll} 948 1 & \mbox{if $x=x'$} \\ 949 0 & \mbox{otherwise} 950 \end{array} 951 \right.%} 952\] 953 954\item 955\index{epsilon operator}$M(\hilbert,(\alpha\fun\bool)\fun\alpha)\in\prod_{X\in{\cal 956U}}.(X\fun\two)\fun X$ is the function assigning to each $X\in{\cal 957U}$ the choice\index{choice operator, in HOL logic@choice operator, in \HOL{} logic!formal semantics of} function sending $f\in(X\fun\two)$ to 958\[ 959\ch_{X}(f) = \left\{ \begin{array}{ll} 960 \ch(f^{-1}\{1\}) 961 & \mbox{if $f^{-1}\{1\}\not=\emptyset$}\\ 962 \ch(X) & \mbox{otherwise} 963 \end{array} 964 \right.%} 965\] 966where $f^{-1}\{1\}=\{x\in X : f(x)=1\}$. (Note that $f^{-1}\{1\}$ is in 967$\cal U$ when it is non-empty, by the property {\bf Sub} of the 968universe $\cal U$ given in Section~\ref{introduction}. The function 969$\ch$ is given by property {\bf Choice}.) 970 971\end{itemize} 972 973It will be assumed from now on that signatures and their models are 974standard. 975 976\medskip 977 978\noindent{\bf Remark\ } 979This particular choice of primitive constants is arbitrary. The 980standard 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$ 982(`or'), $\neg$ (`not'), $\forall$ (`for all'), $\exists$ (`there 983exists'), $=$ (`equals'), $\iota$ (`the'), and $\hilbert$ (`a'). This 984set is redundant, since it can be defined (in a sense explained in 985Section~\ref{defs}) from various subsets. In practice, it is 986necessary to work with the full set of logical constants, and the 987particular subset taken as primitive is not important. The interested 988reader can explore this topic further by reading Andrews' 989book~\cite{Andrews} and the references it contains. 990 991\medskip 992 993Terms of type \ty{bool} are called {\it formulas\/}\index{formulas as terms, in HOL logic@formulas as terms, in \HOL{} logic}. 994 995The following notational abbreviations are used: 996 997\begin{center} 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} 1003\index{epsilon operator} 1004\begin{tabular}{|l|l|}\hline 1005{\rm Notation} & {\rm Meaning}\\ \hline 1006$t_{\sigma}=t'_{\sigma}$ & 1007 $=_{\sigma\fun\sigma\fun\ty{bool}}\ t_{\sigma}\ t'_{\sigma}$\\ \hline 1008$t\imp t'$ & 1009 $\imp_{\ty{bool}\fun\ty{bool}\fun\ty{bool}}\ t_\ty{bool}\ 1010t'_\ty{bool}$\\ \hline 1011$\hilbert x_{\sigma}.\ t$ & 1012 $ \hilbert_{(\sigma\fun\ty{bool})\fun\sigma} 1013(\lambda x_{\sigma}.\ t)$\\ \hline 1014\end{tabular} 1015\end{center} 1016These notations are special cases of general abbreviatory conventions 1017supported by the \HOL{} system. The first two are infixes and the 1018third is a binder (see \DESCRIPTION's sections on parsing and 1019pretty-printing). 1020 1021 1022 1023%%% Local Variables: 1024%%% mode: latex 1025%%% TeX-master: "logic" 1026%%% End: 1027