155714Skris% Revised version of Part II, Chapter 10 of HOL DESCRIPTION 255714Skris% Incorporates material from both of chapters 9 and 10 of the old 355714Skris% version of DESCRIPTION 455714Skris% Written by Andrew Pitts 555714Skris% 8 March 1991 655714Skris% revised August 1991 755714Skris\chapter{Theories}\label{semantics} 8296341Sdelphij 955714Skris\section{Introduction} 1055714Skris 1155714SkrisThe result, if any, of a session with the \HOL{} system is an object 1255714Skriscalled a {\it theory\/}. This object is closely related to what a 1355714Skrislogician would call a theory\index{theories, in HOL logic@theories, in \HOL{} logic!abstract form of}, but there are some differences arising 1455714Skrisfrom the needs of mechanical proof. A \HOL{} theory, like a logician's 15296341Sdelphijtheory, contains sets of types, constants, definitions and axioms. In 1655714Skrisaddition, however, a \HOL{} theory, at any point in time, contains an 1755714Skrisexplicit list of theorems that have already been proved from the 1855714Skrisaxioms and definitions. Logicians have no need to distinguish theorems 1955714Skrisactually proved from those merely provable; hence they do not normally 2055714Skrisconsider sets of proven theorems as part of a theory; rather, they 2155714Skristake the theorems of a theory to be the (often infinite) set of all 22296341Sdelphijconsequences of the axioms and definitions. A related difference 2355714Skrisbetween logicians' theories and \HOL{} theories is that for logicians, 2455714Skristheories are static objects, but in \HOL{} they can be thought of as 2555714Skrispotentially extendable. For example, the \HOL{} system provides tools 2655714Skrisfor adding to theories and combining theories. A typical interaction 2755714Skriswith \HOL{} consists in combining some existing theories, making some 2855714Skrisdefinitions, proving some theorems and then saving the new results. 2955714Skris 3055714SkrisThe purpose of the \HOL{} system is to provide tools to enable 3155714Skriswell-formed theories to be constructed. The \HOL{} logic is typed: 3255714Skriseach theory specifies a signature of type and individual constants; 3355714Skristhese then determine the sets of types and terms as in the previous 3455714Skrischapter. All the theorems of such theories are logical consequences 3555714Skrisof the definitions and axioms of the theory. The \HOL{} system ensures 3655714Skristhat only well-formed theories can be constructed by allowing theorems 37296341Sdelphijto be created only by {\it formal proof\/}. Explicating this involves 3855714Skrisdefining what it means to be a theorem, which leads to the description 3955714Skrisof the proof system of \HOL, to be given below. It is shown to be {\em 40296341Sdelphijsound\/} for the set theoretic semantics of \HOL{} described in the 4155714Skrisprevious chapter. This means that a theorem is satisfied by a model 4255714Skrisif it has a formal proof from axioms which are themselves satisfied by 4355714Skristhe model. Since a logical contradiction is not satisfied by any 4455714Skrismodel, this guarantees in particular that a theory possessing a model 4555714Skrisis necessarily consistent, \ie\ a logical contradiction cannot be 4655714Skrisformally proved from its axioms. 4755714Skris 4855714SkrisThis chapter also describes the various mechanisms by which \HOL\ 4955714Skristheories can be extended to new theories. Each mechanism is shown 5055714Skristo preserve the property of possessing a model. Thus theories built 5155714Skrisup from the initial \HOL{} theory (which does possess a model) using 52296341Sdelphijthese mechanisms are guaranteed to be consistent. 5355714Skris 5455714Skris 5555714Skris\section{Sequents} 5655714Skris\label{sequents} 5755714Skris 58100928SnectarThe \HOL{} logic is phrased in terms of hypothetical assertions called 59238405Sjkim{\em sequents}.\index{sequents!in natural deduction} Fixing a 60100928Snectar(standard) signature $\Sigma_\Omega$, a sequent is a pair $(\Gamma, 61100928Snectart)$ where $\Gamma$ is a finite set of formulas over $\Sigma_\Omega$ 62100928Snectarand $t$ is a single formula over $\Sigma_\Omega$.\footnote{Note that 63100928Snectarthe type subscript is omitted from terms when it is clear from the 64100928Snectarcontext that they are formulas, \ie\ have type \ty{bool}.} The set of 65100928Snectarformulas $\Gamma$ forming the first component of a sequent is called 66296341Sdelphijits set of {\it assumptions\/}\index{assumptions!of sequents} and the 67100928Snectarterm $t$ forming the second component is called its {\it 68100928Snectarconclusion\/}\index{conclusions!of sequents}. When it is not ambiguous 69100928Snectarto do so, a sequent $(\{\},t)$ is written as just $t$. 70100928Snectar 71100928Snectar 72100928SnectarIntuitively, a model $M$ of $\Sigma_\Omega$ {\em 73100928Snectarsatisfies}\index{satisfaction of sequents, by model} a sequent 74100928Snectar$(\Gamma, t)$ if any interpretation of relevant free variables as 75100928Snectarelements of $M$ making the formulas in $\Gamma$ true, also makes the 76100928Snectarformula $t$ true. To make this more precise, suppose 77100928Snectar$\Gamma=\{t_1,\ldots,t_p\}$ and let $\alpha\!s,\!x\!s$ be a 78100928Snectarcontext containing all the type variables and all the free variables 79100928Snectaroccurring in the formulas $t,t_{1},\ldots,t_{p}$. Suppose that 80100928Snectar$\alpha\!s$ has length $n$, that $x\!s=x_{1},\ldots,x_{m}$ and that the 81100928Snectartype of $x_{j}$ is $\sigma_{j}$. Since formulas are terms of type 82100928Snectar$\bool$, the semantics of terms defined in the previous chapter gives 83100928Snectarrise to elements $\den{\alpha\!s,\!x\!s.t}_M$ and 84100928Snectar$\den{\alpha\!s,\!x\!s.t_{k}}_M$ ($k=1,\ldots,p$) in 85100928Snectar\[ 86100928Snectar\prod_{X\!s\in{\cal U}^{n}} \left( 87100928Snectar\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}_M(X\!s)\right) \fun \:\two \] 88100928SnectarSay that the model $M$ {\em satisfies\/} the sequent $(\Gamma,t)$ and 89100928Snectarwrite 90100928Snectar\[ 91100928Snectar\Gamma \models_{M} t 92100928Snectar\] 93100928Snectarif for all $X\!s\in{\cal U}^{n}$ and 94100928Snectarall $y\!s\in\den{\alpha\!s.\sigma_{1}}_M(X\!s)\times\cdots\times 95100928Snectar\den{\alpha\!s.\sigma_{m}}_M(X\!s)$ with 96100928Snectar\[ 97100928Snectar\den{\alpha\!s,\!x\!s.t_{k}}_M(X\!s)(y\!s)=1 98100928Snectar\] 99100928Snectarfor all $k=1,\ldots,p$, it is also the case that 100100928Snectar\[ 101100928Snectar\den{\alpha\!s,\!x\!s.t}_M(X\!s)(y\!s)=1. 102100928Snectar\] 103100928Snectar(Recall that $\two$ is the set $\{0,1\}$.) 104100928Snectar 105100928SnectarIn the case $p=0$, the satisfaction of $(\{\},t)$ by $M$ will be written 106100928Snectar$\models_{M} t$. Thus $\models_{M} t$ means that the dependently typed function 107100928Snectar\[ 108100928Snectar\den{t}_M \in \prod_{X\!s\in{\cal U}^{n}} 109100928Snectar\left(\prod_{j=1}^{m}\den{\alpha\!s.\sigma_{j}}_M(X\!s)\right) \fun \:\two 110100928Snectar\] 111238405Sjkimis constant with value $1\in\two$. 112238405Sjkim 113238405Sjkim\section{Logic} 114238405Sjkim 115238405SjkimA deductive system\index{deductive systems} 116238405Sjkim${\cal D}$ is a set of pairs $(L,(\Gamma,t))$ where $L$ is a 117238405Sjkim(possibly empty) list of sequents and $(\Gamma,t)$ is a sequent. 118238405Sjkim 119238405SjkimA sequent $(\Gamma,t)$ follows from\index{follows from, in natural deduction} 120238405Sjkima set of sequents 121238405Sjkim$\Delta$ by a deductive system 122238405Sjkim${\cal D}$ if 123238405Sjkimand only if there exist sequents 124238405Sjkim$(\Gamma_1,t_1)$, $\ldots$ , $(\Gamma_n,t_n)$ such that: 125238405Sjkim\begin{enumerate} 126238405Sjkim\item $(\Gamma,t) = (\Gamma_n,t_n)$, and 127238405Sjkim\item for all $i$ such that $1\leq i\leq n$ 128238405Sjkim\begin{enumerate} 129238405Sjkim\item either 130238405Sjkim$(\Gamma_i,t_i)\in \Delta$ or 131238405Sjkim\item $(L_i,(\Gamma_i,t_i))\in{\cal D}$ for some list $L_i$ of members of 132238405Sjkim$\Delta\cup\{(\Gamma_1,t_1),\ldots,(\Gamma_{i-1},t_{i-1})\}$. 133238405Sjkim\end{enumerate} 134238405Sjkim\end{enumerate} 135238405SjkimThe sequence $(\Gamma_1,t_1),\cdots,(\Gamma_n,t_n)$ 136238405Sjkimis called a {\it proof\/}\index{proof!in natural deduction} of 13755714Skris$(\Gamma,t)$ from $\Delta$ with respect to ${\cal D}$. 13855714Skris 139109998SmarkmNote that if $(\Gamma,t)$ follows from $\Delta$, then $(\Gamma,t)$ 140109998Smarkmalso follows from any $\Delta'$ such that $\Delta\subseteq\Delta'$. 14155714SkrisThis property is called {\it monotonicity\/}\index{monotonicity, in deductive systems}. 14255714Skris 143296341SdelphijThe notation\index{turnstile notation} $t_1,\ldots,t_n\vdash_{{\cal 144296341SdelphijD},\Delta} t$ means that the sequent $(\{t_1,\ldots,t_n\},\ t)$ 145296341Sdelphijfollows from $\Delta$ by ${\cal D}$. If either ${\cal D}$ or $\Delta$ 146296341Sdelphijis clear from the context then it may be omitted. In the case that 147296341Sdelphijthere are no hypotheses\index{hypotheses!of sequents} (\ie\ $n=0$), 148296341Sdelphijjust $\vdash t$ is written. 149296341Sdelphij 150296341SdelphijIn practice, a particular deductive system is usually specified by a 15155714Skrisnumber of (schematic) \emph{rules of inference}, 152296341Sdelphij\index{inference rules, of HOL logic@inference rules, of \HOL{} logic!abstract form of primitive} 153296341Sdelphijwhich take the form 154296341Sdelphij\[ 155296341Sdelphij\frac{\Gamma_1\turn t_1 \qquad\cdots\qquad\Gamma_n\turn t_n} 156296341Sdelphij{\Gamma \turn t} 157296341Sdelphij\] 158296341SdelphijThe sequents above the line are called the {\it 159296341Sdelphijhypotheses\/}\index{hypotheses!of inference rules} of the rule and the 160296341Sdelphijsequent below the line is called its {\it 161238405Sjkimconclusion}.\index{conclusions!of inference rules} Such a rule is 162296341Sdelphijschematic because it may contain metavariables 163109998Smarkmstanding for arbitrary terms of the appropriate types. Instantiating 164296341Sdelphijthese metavariables with actual terms, one gets a list of sequents 165296341Sdelphijabove the line and a single sequent below the line which together 166296341Sdelphijconstitute a particular element of the deductive system. The 167296341Sdelphijinstantiations allowed for a particular rule may be restricted by 168296341Sdelphijimposing a {\em side condition\/} on the rule. 169296341Sdelphij 17055714Skris 17155714Skris\subsection{The \HOL{} deductive system} 172296341Sdelphij\label{HOLrules} 17355714Skris 174296341SdelphijThe deductive system of the \HOL{} logic is specified by eight rules 175296341Sdelphijof inference, given below. The first three rules have no hypotheses; 176296341Sdelphijtheir conclusions can always be deduced. The identifiers in square 177296341Sdelphijbrackets are the names of the \ML\ functions in the \HOL{} system that 178296341Sdelphijimplement the corresponding inference rules (see \DESCRIPTION). Any 179296341Sdelphijside conditions restricting the scope of a rule are given immediately 180296341Sdelphijbelow it. 181296341Sdelphij 182296341Sdelphij\bigskip 183296341Sdelphij 184296341Sdelphij\subsubsection*{Assumption introduction [{\small\tt 18555714SkrisASSUME}]}\index{assumption introduction, in HOL logic@assumption introduction, in \HOL{} logic!abstract form of} 186296341Sdelphij\[ 187296341Sdelphij\overline{t \turn t} 188296341Sdelphij\] 189296341Sdelphij 190296341Sdelphij\subsubsection*{Reflexivity [{\small\tt 191296341SdelphijREFL}]}\index{REFL@\ml{REFL}}\index{reflexivity, in HOL logic@reflexivity, in \HOL{} logic!abstract form of} 192296341Sdelphij\[ 193296341Sdelphij\overline{\turn t = t} 194296341Sdelphij\] 195296341Sdelphij 19655714Skris\subsubsection*{Beta-conversion [{\small\tt BETA\_CONV}]} 197296341Sdelphij\index{beta-conversion, in HOL logic@beta-conversion, in \HOL{} logic!abstract form of}\index{BETA_CONV@\ml{BETA\_CONV}} 198296341Sdelphij\[ 199296341Sdelphij\overline{\turn (\lquant{x}t_1)t_2 = t_1[t_2/x]} 200296341Sdelphij\] 201296341Sdelphij\begin{itemize} 202296341Sdelphij\item Where $t_1[t_2/x]$ is 203296341Sdelphijthe result of substituting $t_2$ for $x$ 204296341Sdelphijin $t_1$, with suitable renaming of variables to prevent free variables 205296341Sdelphijin $t_2$ becoming bound after substitution. 20655714Skris\end{itemize} 207296341Sdelphij 208296341Sdelphij\subsubsection*{Substitution [{\small\tt 209296341SdelphijSUBST}]}\index{SUBST@\ml{SUBST}} \index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!abstract form of} 210296341Sdelphij\[ 211296341Sdelphij\frac{\Gamma_1\turn t_1 = t_1'\qquad\cdots\qquad\Gamma_n\turn t_n = 212296341Sdelphijt_n'\qquad\qquad \Gamma\turn t[t_1,\ldots,t_n]} 213296341Sdelphij{\Gamma_1\cup\cdots\cup\Gamma_n\cup\Gamma\turn t[t_1',\ldots,t_n']} 214296341Sdelphij\] 21555714Skris\begin{itemize} 216296341Sdelphij\item Where $t[t_1,\ldots,t_n]$ denotes a term $t$ with some free 217296341Sdelphijoccurrences of subterms $t_1$, $\ldots$ , $t_n$ singled out and 218296341Sdelphij$t[t_1',\ldots,t_n']$ denotes the result of replacing each selected 219296341Sdelphijoccurrence of $t_i$ by $t_i'$ (for $1{\leq}i{\leq}n$), with suitable 220296341Sdelphijrenaming of variables to prevent free variables in $t_i'$ becoming 221296341Sdelphijbound after substitution. 222296341Sdelphij\end{itemize} 223160814Ssimon 224296341Sdelphij\subsubsection*{Abstraction [{\small\tt ABS}]} 225160814Ssimon\index{ABS@\ml{ABS}}\index{abstraction rule, in HOL logic@abstraction rule, in \HOL{} logic!abstract form of} 226296341Sdelphij\[ 227296341Sdelphij\frac{\Gamma\turn t_1 = t_2} 228296341Sdelphij{\Gamma\turn (\lquant{x}t_1) = (\lquant{x}t_2)} 229296341Sdelphij\] 23055714Skris\begin{itemize} 231296341Sdelphij\item Provided $x$ is not free in $\Gamma$. 232296341Sdelphij\end{itemize} 233296341Sdelphij 234296341Sdelphij\subsubsection*{Type instantiation [{\small\tt INST\_TYPE}]} 235296341Sdelphij\index{type instantiation, in HOL logic@type instantiation, in \HOL{} logic!abstract form of} 236160814Ssimon\newcommand{\insttysub}{[\sigma_1,\ldots,\sigma_n/\alpha_1,\ldots,\alpha_n]} 237296341Sdelphij\[ 238296341Sdelphij\frac{\Gamma\turn t} 239296341Sdelphij{\Gamma\insttysub\turn t\insttysub} 240296341Sdelphij\] 241160814Ssimon\begin{itemize} 24255714Skris\item Where $t\insttysub$ is the result of substituting, in parallel, 243296341Sdelphij the types $\sigma_1$, $\dots$, $\sigma_n$ for type variables 244296341Sdelphij $\alpha_1$, $\dots$, $\alpha_n$ in $t$, and where $\Gamma\insttysub$ 245296341Sdelphij is the result of performing the same substitution across all of the 246296341Sdelphij theorem's hypotheses. 247296341Sdelphij\item After the instantiation, variables free in the input can not 248296341Sdelphij become bound, but distinct free variables in the input may become 249296341Sdelphij identified. 250296341Sdelphij\end{itemize} 251296341Sdelphij 252296341Sdelphij\subsubsection*{Discharging an assumption [{\small\tt 253296341SdelphijDISCH}]}\index{discharging assumptions, in HOL logic@discharging assumptions, in \HOL{} logic!abstract form of}\index{DISCH@\ml{DISCH}} 254296341Sdelphij\[ 255238405Sjkim\frac{\Gamma\turn t_2} 256296341Sdelphij{\Gamma -\{t_1\} \turn t_1 \imp t_2} 257160814Ssimon\] 258296341Sdelphij\begin{itemize} 259296341Sdelphij\item Where $\Gamma -\{t_1\}$ is the set subtraction of $\{t_1\}$ 260296341Sdelphijfrom $\Gamma$. 261296341Sdelphij\end{itemize} 262296341Sdelphij 263296341Sdelphij\subsubsection*{Modus Ponens [{\small\tt 264296341SdelphijMP}]}\index{MP@\ml{MP}}\index{Modus Ponens, in HOL logic@Modus Ponens, in \HOL{} logic!abstract form of} 265296341Sdelphij\[ 266296341Sdelphij\frac{\Gamma_1 \turn t_1 \imp t_2 \qquad\qquad \Gamma_2\turn t_1} 267296341Sdelphij{\Gamma_1 \cup \Gamma_2 \turn t_2} 268296341Sdelphij\] 269296341Sdelphij 270296341SdelphijIn addition to these eight rules, there are also four {\it 271296341Sdelphijaxioms\/}\index{axioms!as inference rules} which could have been 272296341Sdelphijregarded as rules of inference without hypotheses. This is not done, 273296341Sdelphijhowever, since it is most natural to state the axioms using some 274296341Sdelphijdefined logical constants and the principle of constant definition has 275296341Sdelphijnot yet been described. The axioms are given in Section~\ref{INIT} and 276160814Ssimonthe definitions of the extra logical constants they involve are given in 277296341SdelphijSection~\ref{LOG}. 278296341Sdelphij 279296341SdelphijThe particular set of rules and axioms chosen to axiomatize the \HOL\ 280296341Sdelphijlogic is rather arbitrary. It is partly based on the rules that were 281296341Sdelphijused in the 282296341Sdelphij\LCF\index{LCF@\LCF}\ logic 283296341Sdelphij\PPL\index{PPlambda (same as PPLAMBDA), of LCF system@\ml{PP}$\lambda$ (same as \ml{PPLAMBDA}), of \ml{LCF} system}, since \HOL{} was 284296341Sdelphijimplemented by modifying the \LCF\ system. In particular, the 285296341Sdelphijsubstitution\index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!implementation of} rule {\small\tt SUBST} is exactly 286296341Sdelphijthe same as the corresponding rule in \LCF; the code implementing this 287296341Sdelphijwas written by Robin Milner and is highly optimized. Because 288296341Sdelphijsubstitution is such a pervasive activity in proof, it was felt to be 289296341Sdelphijimportant that the system primitive be as fast as possible. From a 290296341Sdelphijlogical point of view it would be better to have a simpler 291296341Sdelphijsubstitution primitive, such as `Rule R' of Andrews' logic ${\cal 292160814SsimonQ}_0$, and then to derive more complex rules from it. 293296341Sdelphij 294296341Sdelphij\subsection{Soundness theorem} 295296341Sdelphij\index{soundness!of HOL deductive system@of \HOL{} deductive system} 296296341Sdelphij\label{soundness} 297296341Sdelphij 298296341Sdelphij\index{inference rules, of HOL logic@inference rules, of \HOL{} logic!formal semantics of} 299296341Sdelphij\emph{The rules of the \HOL{} deductive system are {\em sound} for 300296341Sdelphij the notion of satisfaction defined in Section~\ref{sequents}: for 301296341Sdelphij any instance of the rules of inference, if a (standard) model 302296341Sdelphij satisfies the hypotheses of the rule it also satisfies the 303296341Sdelphij conclusion.} 304296341Sdelphij 305296341Sdelphij\medskip 306160814Ssimon 307296341Sdelphij\noindent{\bf Proof\ } 308296341SdelphijThe verification of the soundness of the rules is straightforward. 309296341SdelphijThe properties of the semantics with respect to substitution given by 31055714SkrisLemmas 3 and 4 in Section~\ref{term-substitution} are needed for rules 311296341Sdelphij\ml{BETA\_CONV}, \ml{SUBST} and 312296341Sdelphij\ml{INST\_TYPE}\index{INST_TYPE@\ml{INST\_TYPE}}.\footnote{Note in 31355714Skris particular that the second restriction on \ml{INST\_TYPE} enables 314296341Sdelphij the result on the semantics of substituting types for type variables 315296341Sdelphij in terms to be applied.} The fact that $=$ and $\imp$ are 316296341Sdelphijinterpreted standardly (as in Section~\ref{standard-signatures}) is 317296341Sdelphijneeded for rules \ml{REFL}\index{REFL@\ml{REFL}}, 318296341Sdelphij\ml{BETA\_CONV}\index{BETA_CONV@\ml{BETA\_CONV}}, 319296341Sdelphij\ml{SUBST}\index{SUBST@\ml{SUBST}}, \ml{ABS}\index{ABS@\ml{ABS}}, 320296341Sdelphij\ml{DISCH}\index{DISCH@\ml{DISCH}} and \ml{MP}\index{MP@\ml{MP}}. 321296341Sdelphij 322296341Sdelphij\section{\HOL{} Theories} 323296341Sdelphij\label{theories} 324296341Sdelphij 325296341SdelphijA \HOL{} {\it theory\/}\index{theories, in HOL logic@theories, in \HOL{} logic!abstract form of} ${\cal T}$ is a $4$-tuple: 326296341Sdelphij\begin{eqnarray*} 327296341Sdelphij{\cal T} & = & \langle{\sf Struc}_{\cal T},{\sf Sig}_{\cal T}, 328296341Sdelphij {\sf Axioms}_{\cal T},{\sf Theorems}_{\cal T}\rangle 329296341Sdelphij\end{eqnarray*} 330296341Sdelphijwhere 331296341Sdelphij\begin{myenumerate} 332296341Sdelphij 333296341Sdelphij\item ${\sf Struc}_{\cal T}$ is a type structure\index{type structures, of HOL theories@type structures, of \HOL{} theories} called the type 334296341Sdelphijstructure of ${\cal T}$; 335296341Sdelphij 336296341Sdelphij\item ${\sf Sig}_{\cal T}$ is a signature\index{signatures, of HOL logic@signatures, of \HOL{} logic!of HOL theories@of \HOL{} theories} 337296341Sdelphijover ${\sf Struc}_{\cal T}$ called the signature of ${\cal T}$; 338296341Sdelphij 339296341Sdelphij\item ${\sf Axioms}_{\cal T}$ is a set of sequents over ${\sf Sig}_{\cal T}$ 340296341Sdelphijcalled the axioms\index{axioms, in a HOL theory@axioms, in a \HOL{} theory} 341296341Sdelphij of ${\cal T}$; 342296341Sdelphij 343296341Sdelphij\item ${\sf Theorems}_{\cal T}$ is a set of sequents over 34455714Skris${\sf Sig}_{\cal T}$ called the theorems 345296341Sdelphij% 346296341Sdelphij\index{theorems, in HOL logic@theorems, in \HOL{} logic!abstract form of} 347296341Sdelphij% 348296341Sdelphijof ${\cal T}$, with 34955714Skristhe property that every member follows from ${\sf Axioms}_{\cal T}$ by 350296341Sdelphijthe \HOL{} deductive system. 351296341Sdelphij 352296341Sdelphij\end{myenumerate} 353296341Sdelphij 354296341SdelphijThe sets ${\sf Types}_{\cal T}$ and ${\sf Terms}_{\cal T}$ of types and 355296341Sdelphijterms of a theory ${\cal T}$ are, respectively, the sets of types and 356296341Sdelphijterms constructable from the type structure and signature of ${\cal 357296341SdelphijT}$, \ie: 358296341Sdelphij\begin{eqnarray*} 359296341Sdelphij{\sf Types}_{\cal T} & = & {\sf Types}_{{\sf Struc}_{\cal T}}\\ 360296341Sdelphij{\sf Terms}_{\cal T} & = & {\sf Terms}_{{\sf Sig}_{\cal T}} 361296341Sdelphij\end{eqnarray*} 362296341SdelphijA model of a theory $\cal T$ is specified by giving a (standard) model 36355714Skris$M$ of the underlying signature of the theory with the property that 364296341Sdelphij$M$ satisfies all the sequents which are axioms of $\cal T$. Because 365296341Sdelphijof the Soundness Theorem~\ref{soundness}, it follows that $M$ also 366296341Sdelphijsatisfies any sequents in the set of given theorems, ${\sf 367296341SdelphijTheorems}_{\cal T}$. 368296341Sdelphij 369296341Sdelphij\subsection{The theory {\tt MIN}} 370296341Sdelphij\label{sec:min-thy} 371296341Sdelphij 37255714SkrisThe {\it minimal theory\/}\index{MIN@\ml{MIN}}\index{minimal theory, of HOL logic@minimal theory, of \HOL{} logic} \theory{MIN} is defined by: 373296341Sdelphij\[ 37455714Skris\theory{MIN} = 375296341Sdelphij\langle\{(\bool,0),\ (\ind,0)\},\ 37655714Skris \{\imp_{\bool\fun\bool\fun\bool}, 377296341Sdelphij=_{\alpha\fun\alpha\fun\bool}, 378296341Sdelphij\hilbert_{(\alpha\fun\bool)\fun\alpha}\},\ 379296341Sdelphij\{\},\ \{\}\rangle 380296341Sdelphij\] 381296341SdelphijSince the theory \theory{MIN} has a signature consisting only of 382296341Sdelphijstandard items and has no axioms, it possesses a unique standard model, 383296341Sdelphijwhich will be denoted {\em Min}. 384296341Sdelphij 385296341SdelphijAlthough the theory \theory{MIN} contains only the minimal standard 38655714Skrissyntax, by exploiting the higher order constructs of \HOL{} one can 38755714Skrisconstruct a rather rich collection of terms over it. The following 388296341Sdelphijtheory introduces names for some of these terms that denote useful 389296341Sdelphijlogical operations in the model {\em Min}. 390296341Sdelphij 391296341SdelphijIn the implementation, the theory \theory{MIN} is given the name 392296341Sdelphij\theoryimp{min}, and also contains the distinguished binary type 393296341Sdelphijoperator $\fun$, for constructing function spaces. 394296341Sdelphij 39555714Skris\subsection{The theory {\tt LOG}} 396296341Sdelphij\index{LOG@\ml{LOG}} 397296341Sdelphij\label{LOG} 39855714Skris 399296341SdelphijThe theory \theory{LOG} has the same type 400296341Sdelphijstructure as \theory{MIN}. Its signature contains the constants in 401296341Sdelphij\theory{MIN} and the following constants: 402296341Sdelphij\[ 40355714Skris\T_\ty{bool} 404296341Sdelphij\index{T@\holtxt{T}!abstract form of} 405296341Sdelphij\index{truth values, in HOL logic@truth values, in \HOL{} logic!abstract form of} 406160814Ssimon\] 407296341Sdelphij\[ 408160814Ssimon\forall_{(\alpha\fun\ty{bool})\fun\ty{bool}} 409296341Sdelphij\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!abstract form of} 410160814Ssimon\] 41155714Skris\[ 412296341Sdelphij\exists_{(\alpha\fun\ty{bool})\fun\ty{bool}} 413296341Sdelphij\index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abstract form of} 414296341Sdelphij\] 415238405Sjkim\[ 416296341Sdelphij\F_\ty{bool} 417296341Sdelphij\index{F@\holtxt{F}!abstract form of} 41855714Skris\] 419296341Sdelphij\[ 42055714Skris\neg_{\ty{bool}\fun\ty{bool}} 421296341Sdelphij\index{negation, in HOL logic@negation, in \HOL{} logic!abstract form of} 422296341Sdelphij\] 42355714Skris\[ 424296341Sdelphij\wedge_{\ty{bool}\fun\ty{bool}\fun\ty{bool}} 425296341Sdelphij\index{conjunction, in HOL logic@conjunction, in \HOL{} logic!abstract form of} 426109998Smarkm\] 427296341Sdelphij\[ 428109998Smarkm\vee_{\ty{bool}\fun\ty{bool}\fun\ty{bool}} 429296341Sdelphij\index{disjunction, in HOL logic@disjunction, in \HOL{} logic!abstract form of} 430296341Sdelphij\] 431296341Sdelphij\[ 432296341Sdelphij\OneOne_{(\alpha\fun\beta)\fun\ty\bool} 433296341Sdelphij\index{one-to-one predicate, in HOL logic@one-to-one predicate, in \HOL{} logic!abstract form of} 434296341Sdelphij\] 435100936Snectar\[ 436296341Sdelphij\Onto_{(\alpha\fun\beta)\fun\ty\bool} 437296341Sdelphij\index{onto predicate, in HOL logic@onto predicate, in \HOL{} logic!abstract form of} 438296341Sdelphij\] 439296341Sdelphij\[ 440109998Smarkm\TyDef_{(\alpha\fun\ty{bool})\fun(\beta\fun\alpha)\fun\ty{bool}} 441296341Sdelphij\] 442296341SdelphijThe following special notation is used in connection with these constants: 443100928Snectar\begin{center} 444296341Sdelphij\index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abbreviation for multiple} 445296341Sdelphij\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!abbreviation for multiple} 446109998Smarkm\begin{tabular}{|l|l|}\hline 447296341Sdelphij{\rm Notation} & {\rm Meaning}\\ \hline $\uquant{x_{\sigma}}t$ & 44855714Skris$\forall(\lambda x_{\sigma}.\ t)$\\ \hline $\uquant{x_1\ x_2\ \cdots\ 449296341Sdelphijx_n}t$ & $\uquant{x_1}(\uquant{x_2} \cdots\ (\uquant{x_n}t) 450296341Sdelphij\ \cdots\ )$\\ \hline 451296341Sdelphij$\equant{x_{\sigma}}t$ 452296341Sdelphij & $\exists(\lambda x_{\sigma}.\ t)$\\ \hline 453296341Sdelphij$\equant{x_1\ x_2\ \cdots\ x_n}t$ 45455714Skris & $\equant{x_1}(\equant{x_2} \cdots\ (\equant{x_n}t) 455296341Sdelphij\ \cdots\ )$\\ \hline 456296341Sdelphij$t_1\ \wedge\ t_2$ & $\wedge\ t_1\ t_2$\\ \hline 457296341Sdelphij$t_1\ \vee\ t_2$ & $\vee\ t_1\ t_2$\\ \hline 458296341Sdelphij\end{tabular}\end{center} 459296341Sdelphij 460296341SdelphijThe axioms of the theory \theory{LOG} consist of the following 461296341Sdelphijsequents: 462296341Sdelphij\[ 46355714Skris\begin{array}{l} 464296341Sdelphij 465296341Sdelphij\turn \T = ((\lquant{x_{\ty{bool}}}x) = 466246772Sjkim (\lquant{x_{\ty{bool}}}x)) \\ 467246772Sjkim\turn \forall = \lquant{P_{\alpha\fun\ty{bool}}}\ P = 468246772Sjkim (\lquant{x}\T ) \\ 469246772Sjkim\turn \exists = \lquant{P_{\alpha\fun\ty{bool}}}\ 470246772Sjkim P({\hilbert}\ P) \\ 471246772Sjkim\turn \F = \uquant{b_{\ty{bool}}}\ b \\ 472246772Sjkim\turn \neg = \lquant{b}\ b \imp \F \\ 473246772Sjkim\turn {\wedge} = \lquant{b_1\ b_2}\uquant{b} 47455714Skris (b_1\imp (b_2 \imp b)) \imp b \\ 475296341Sdelphij\turn {\vee} = \lquant{b_1\ b_2}\uquant{b} 476296341Sdelphij (b_1 \imp b)\imp ((b_2 \imp b) \imp b) \\ 477296341Sdelphij\turn \OneOne = \lquant{f_{\alpha \fun\beta}}\uquant{x_1\ x_2} 478296341Sdelphij (f\ x_1 = f\ x_2) \imp (x_1 = x_2) \\ 479296341Sdelphij\turn \Onto = \lquant{f_{\alpha\fun\beta}} 480296341Sdelphij \uquant{y}\equant{x} y = f\ x \\ 48155714Skris\turn \TyDef = \begin{array}[t]{l} 482296341Sdelphij \lambda P_{\alpha\fun\ty{bool}}\ 483296341Sdelphij rep_{\beta\fun\alpha}. 484296341Sdelphij \OneOne\ rep\ \ \wedge{}\\ 485296341Sdelphij \quad(\uquant{x}P\ x \ =\ (\equant{y} x = rep\ y)) 486296341Sdelphij \end{array} 487296341Sdelphij\end{array} 488296341Sdelphij\] 489296341SdelphijFinally, as for the theory \theory{MIN}, the set ${\sf 490296341SdelphijTheorems}_{\theory{LOG}}$ is taken to be empty. 491296341Sdelphij 492296341SdelphijNote that the axioms of the theory \theory{LOG} are essentially {\em 493296341Sdelphijdefinitions\/} of the new constants of \theory{LOG} as terms in the 494296341Sdelphijoriginal theory \theory{MIN}. (The mechanism for making such 495296341Sdelphijextensions of theories by definitions of new constants will be set out 496296341Sdelphijin general in Section~\ref{defs}.) The first seven axioms define the 49755714Skrislogical constants for truth, universal quantification, existential 498296341Sdelphijquantification, falsity, negation, conjunction and disjunction. 499296341SdelphijAlthough these definitions may be obscure to some readers, they are in 500296341Sdelphijfact standard definitions of these logical constants in terms of 501296341Sdelphijimplication, equality and choice within higher order logic. The next 502296341Sdelphijtwo axioms define the properties of a function being one-one and onto; 503296341Sdelphijthey will be used to express the axiom of infinity (see 50455714SkrisSection~\ref{INIT}), amongst other things. The last axiom defines a 505296341Sdelphijconstant used for type definitions (see Section~\ref{tydefs}). 50655714Skris 507296341SdelphijThe unique standard model {\em Min\/} of \theory{MIN} gives rise to a 508296341Sdelphijunique standard model of 50955714Skris\theory{LOG}\index{LOG@\ml{LOG}!formal semantics of}. This is 510296341Sdelphijbecause, given the semantics of terms set out in 511296341SdelphijSection~\ref{semantics of terms}, to satisfy the above equations one 512296341Sdelphijis forced to interpret the new constants in the following way: 513296341Sdelphij\index{axioms!formal semantics of HOL logic's@formal semantics of \HOL{} logic's|(} 514296341Sdelphij\begin{itemize} 515296341Sdelphij 516296341Sdelphij\item $\den{\T_{\bool}}\index{T@\holtxt{T}!formal semantics of} = 1 \in \two$ 517296341Sdelphij 518296341Sdelphij\item \index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!formal semantics of} 519296341Sdelphij$\den{\forall_{(\alpha\fun\bool)\fun\bool}}\in\prod_{X\in{\cal 52055714Skris U}}(X\fun\two)\fun\two$ sends $X\in{\cal U}$ and $f\in X\fun\two$ to 521296341Sdelphij\[ 522296341Sdelphij\den{\forall}(X)(f) = \left\{ \begin{array}{ll} 1 & \mbox{if 523296341Sdelphij$f^{-1}\{1\}=X$} \\ 0 & \mbox{otherwise} \end{array} \right. 524296341Sdelphij\] 525296341Sdelphij\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!formal semantics of} 52655714Skris 527296341Sdelphij\item \index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!formal semantics of} 528296341Sdelphij$\den{\exists_{(\alpha\fun\bool)\fun\bool}}\in\prod_{X\in{\cal 52955714Skris U}}(X\fun\two)\fun\two$ sends $X\in{\cal U}$ and $f\in X\fun\two$ to 530296341Sdelphij\[ 531296341Sdelphij\den{\exists}(X)(f) = \left\{ \begin{array}{ll} 532296341Sdelphij 1 & \mbox{if $f^{-1}\{1\}\not=\emptyset$} \\ 533296341Sdelphij 0 & \mbox{otherwise} 534296341Sdelphij \end{array} 535296341Sdelphij \right. \] 536296341Sdelphij 537238405Sjkim\item $\den{\F_{\bool}} = 0 \in \two$\index{F@\holtxt{F}!formal semantics of} 538296341Sdelphij 539296341Sdelphij\item $\den{\neg_{\bool\fun\bool}}\in\two\fun\two$ sends $b\in\two$ to 540296341Sdelphij \[ \den{\neg}(b) = \left\{ \begin{array}{ll} 541296341Sdelphij 1 & \mbox{if $b=0$} \\ 542296341Sdelphij 0 & \mbox{otherwise} 543296341Sdelphij \end{array} 544296341Sdelphij \right. \]\index{negation, in HOL logic@negation, in \HOL{} logic!formal semantics of} 545296341Sdelphij 546296341Sdelphij\item $\den{\wedge_{\bool\fun\bool\fun\bool}}\in\two\fun\two\fun\two$ sends 547238405Sjkim$b,b'\in\two$ to 548296341Sdelphij \[ \den{\wedge}(b)(b') = \left\{ \begin{array}{ll} 549296341Sdelphij 1 & \mbox{if $b=1=b'$} \\ 550296341Sdelphij 0 & \mbox{otherwise} 551296341Sdelphij \end{array} 552296341Sdelphij \right. \]\index{conjunction, in HOL logic@conjunction, in \HOL{} logic!formal semantics of} 553296341Sdelphij 554296341Sdelphij\item $\den{\vee_{\bool\fun\bool\fun\bool}}\in\two\fun\two\fun\two$ sends 555296341Sdelphij$b,b'\in\two$ to 556296341Sdelphij \[ \den{\vee}(b)(b') = \left\{ \begin{array}{ll} 557296341Sdelphij 0 & \mbox{if $b=0=b'$} \\ 558296341Sdelphij 1 & \mbox{otherwise} 559296341Sdelphij \end{array} 560238405Sjkim \right. \]\index{disjunction, in HOL logic@disjunction, in \HOL{} logic!formal semantics of} 56155714Skris 562296341Sdelphij\item $\den{\OneOne_{(\alpha\fun\beta)\fun\bool}}\in\prod_{(X,Y)\in{\cal 563296341Sdelphij U}^{2}} (X\fun Y)\fun \two$ sends $(X,Y)\in{\cal U}^{2}$ and 564296341Sdelphij $f\in(X\fun Y)$ to 565296341Sdelphij \[ \den{\OneOne}(X,Y)(f) = \left\{ \begin{array}{ll} 566296341Sdelphij 0 & \mbox{if $f(x)=f(x')$ 567296341Sdelphij for some $x\not=x'$ in $X$} \\ 568296341Sdelphij 1 & \mbox{otherwise} 569296341Sdelphij \end{array} 570296341Sdelphij \right. \]\index{one-to-one predicate, in HOL logic@one-to-one predicate, in \HOL{} logic!formal semantics of} 571296341Sdelphij 572296341Sdelphij\item $\den{\Onto_{(\alpha\fun\beta)\fun\bool}}\in\prod_{(X,Y)\in{\cal 573296341Sdelphij U}^{2}} (X\fun Y)\fun \two$ sends $(X,Y)\in{\cal U}^{2}$ and 57455714Skris $f\in(X\fun Y)$ to 575238405Sjkim \[ \den{\Onto}(X,Y)(f) = \left\{ \begin{array}{ll} 576296341Sdelphij 1 & \mbox{if $\{f(x):x\in X\}=Y$} \\ 577296341Sdelphij 0 & \mbox{otherwise} 578296341Sdelphij \end{array} 579296341Sdelphij \right. \]\index{onto predicate, in HOL logic@onto predicate, in \HOL{} logic!formal semantics of} 580296341Sdelphij 581296341Sdelphij\item $\den{\TyDef_{(\alpha\fun\bool)\fun(\beta\fun\alpha)\fun\bool}}\in 582238405Sjkim \prod_{(X,Y)\in{\cal U}^{2}} (X\fun\two)\fun(Y\fun X)\fun\two$ \\ 583296341Sdelphij sends $(X,Y)\in{\cal U}^{2}$, $f\in(X\fun\two)$ and $g\in(Y\fun X)$ to 584296341Sdelphij \[ \den{\TyDef}(X,Y)(f)(g) = \left\{ \begin{array}{ll} 585296341Sdelphij 1 & \mbox{if 586296341Sdelphij $\den{\OneOne}(Y,X)(g)=1$}\\ 587296341Sdelphij & \mbox{and $f^{-1}\{1\}= 588296341Sdelphij \{g(y) : y\in Y\}$} \\ 589296341Sdelphij 0 & \mbox{otherwise.} 590296341Sdelphij \end{array} 591296341Sdelphij \right. 592296341Sdelphij\] 593238405Sjkim\end{itemize} 594296341Sdelphij\index{axioms!formal semantics of HOL logic's@formal semantics of \HOL{} logic's|)} 595296341SdelphijSince these definitions were obtained by applying the semantics of 596296341Sdelphijterms to the left hand sides of the equations which form the axioms of 597296341Sdelphij\theory{LOG}, these axioms are satisfied and one obtains a model of 598238405Sjkimthe theory \theory{LOG}. 599296341Sdelphij 600296341Sdelphij 601296341Sdelphij\subsection{The theory {\tt INIT}} 602296341Sdelphij\label{INIT} 603238405Sjkim 604296341SdelphijThe theory \theory{INIT}\index{INIT@\ml{INIT}!abstract form of} is 605296341Sdelphijobtained by adding the following four axioms\index{axioms!abstract form of HOL logic's@abstract form of \HOL{} logic's} to the theory 606296341Sdelphij\theory{LOG}. 607296341Sdelphij\[ 608296341Sdelphij\index{BOOL_CASES_AX@\ml{BOOL\_CASES\_AX}!abstract form of} 609296341Sdelphij\index{ETA_AX@\ml{ETA\_AX}!abstract form of} 610296341Sdelphij\index{SELECT_AX@\ml{SELECT\_AX}!abstract form of} 611296341Sdelphij\index{INFINITY_AX@\ml{INFINITY\_AX}!abstract form of} 612296341Sdelphij\index{choice axiom!abstract form of} 613296341Sdelphij\index{axiom of infinity!abstract form of} 614296341Sdelphij\begin{array}{@{}l@{\qquad}l} 615238405Sjkim\mbox{\small\tt BOOL\_CASES\_AX}&\vdash \uquant{b} (b = \T ) \vee (b = \F )\\ 616296341Sdelphij \\ 617296341Sdelphij\mbox{\small\tt ETA\_AX}& 61855714Skris\vdash \uquant{f_{\alpha\fun\beta}}(\lquant{x}f\ x) = f\\ 619238405Sjkim \\ 620296341Sdelphij\mbox{\small\tt SELECT\_AX}& 621296341Sdelphij\vdash \uquant{P_{\alpha\fun\ty{bool}}\ x} P\ x \imp 622296341SdelphijP({\hilbert}\ P)\\ 623269686Sjkim \\ 624296341Sdelphij\mbox{\small\tt INFINITY\_AX}& 625296341Sdelphij\vdash \equant{f_{\ind\fun \ind}} \OneOne \ f \conj \neg(\Onto \ f)\\ 626296341Sdelphij\end{array} 627296341Sdelphij\] 628296341Sdelphij 629296341SdelphijThe unique standard model of \theory{LOG} satisfies these four axioms 630296341Sdelphijand hence is the unique standard model of the theory 631269686Sjkim\theory{INIT}.\index{INIT@\ml{INIT}!formal semantics of} (For axiom 632296341Sdelphij{\small\tt SELECT\_AX} one needs to use the definition of 633269686Sjkim$\den{\hilbert}$ given in Section~\ref{standard-signatures}; for axiom 634296341Sdelphij{\small\tt INFINITY\_AX} one needs the fact that $\den{\ind}=\inds$ is 635296341Sdelphijan infinite set.) 636296341Sdelphij 637296341SdelphijThe theory \theory{INIT} is the initial theory\index{initial theory, 638296341Sdelphij of HOL logic@initial theory, of \HOL{} logic!abstract form of} of the 639296341Sdelphij\HOL{} logic. A theory which extends \theory{INIT} will be called a 640296341Sdelphij{\em standard theory}\index{standard theory}. 641296341Sdelphij 642238405Sjkim\subsection{Implementing theories \texttt{LOG} and \texttt{INIT}} 643296341Sdelphij\label{sec:implementing-log-init} 644296341Sdelphij 645296341SdelphijThe implementation combines the theories \theory{LOG} and 646296341Sdelphij\theory{INIT} into a theory \theoryimp{bool}. It includes all of the 647296341Sdelphijconstants and axioms from those theories, and includes a number of 648296341Sdelphijderived results about those constants. For more on the 649296341Sdelphijimplementation's \theoryimp{bool} theory, see \DESCRIPTION. 65055714Skris 651296341Sdelphij\subsection{Consistency} 652296341Sdelphij\label{consistency} 653296341Sdelphij 654238405SjkimA (standard) theory is {\em consistent\/}\index{consistent theory} if 655296341Sdelphijit is not the case that every sequent over its signature can be 656296341Sdelphijderived from the theory's axioms using the \HOL{} logic, or 657296341Sdelphijequivalently, if the particular sequent $\turn\F$ cannot be so derived. 658296341Sdelphij 659296341SdelphijThe existence of a (standard) model of a theory is sufficient to 660296341Sdelphijestablish its consistency. For by the Soundness 661296341SdelphijTheorem~\ref{soundness}, any sequent that can be derived from the 662296341Sdelphijtheory's axioms will be satisfied by the model, whereas the sequent 663296341Sdelphij$\turn\F$ is never satisfied in any standard model. So in particular, 664296341Sdelphijthe initial theory \theory{INIT} is consistent. 665296341Sdelphij 666296341SdelphijHowever, it is possible for a theory to be consistent but not to 667296341Sdelphijpossess a standard model. This is because the notion of a {\em 668296341Sdelphijstandard\/} model is quite restrictive---in particular there is no 669296341Sdelphijchoice how to interpret the integers and their arithmetic in such a 670296341Sdelphijmodel. The famous incompleteness theorem of G\"odel ensures that there 671296341Sdelphijare sequents which are satisfied in all standard models (\ie\ which are 672296341Sdelphij`true'), but which are not provable in the \HOL{} logic. 673296341Sdelphij 674296341Sdelphij 67555714Skris 676296341Sdelphij 677296341Sdelphij 678296341Sdelphij\section{Extensions of theories} 679296341Sdelphij\index{extension, of HOL logic@extension, of \HOL{} logic!abstract form of} 680296341Sdelphij\label{extensions} 681296341Sdelphij 682296341SdelphijA theory ${\cal T}'$ is said to be an {\em 68355714Skrisextension\/}\index{extension, of theory} of a theory ${\cal T}$ if: 684296341Sdelphij\begin{myenumerate} 685296341Sdelphij\item ${\sf Struc}_{{\cal T}}\subseteq{\sf Struc}_{{\cal T}'}$. 686296341Sdelphij\item ${\sf Sig}_{{\cal T}}\subseteq{\sf Sig}_{{\cal T}'}$. 687296341Sdelphij\item ${\sf Axioms}_{{\cal T}}\subseteq{\sf Axioms}_{{\cal T}'}$. 688296341Sdelphij\item ${\sf Theorems}_{{\cal T}}\subseteq{\sf Theorems}_{{\cal T}'}$. 689296341Sdelphij\end{myenumerate} 69055714SkrisIn this case, any model $M'$ of the larger theory ${\cal T}'$ can be 691296341Sdelphijrestricted to a model of the smaller theory $\cal T$ in the following 69255714Skrisway. First, $M'$ gives rise to a model of the structure and signature 693296341Sdelphijof $\cal T$ simply by forgetting the values of $M'$ at constants not 694296341Sdelphijin ${\sf Struc}_{\cal T}$ or ${\sf Sig}_{\cal T}$. Denoting this model 69555714Skrisby $M$, one has for all $\sigma\in{\sf Types}_{\cal T}$, $t\in{\sf 696238405SjkimTerms}_{\cal T}$ and for all suitable contexts that 697296341Sdelphij\begin{eqnarray*} 698296341Sdelphij\den{\alpha\!s.\sigma}_{M} & = & \den{\alpha\!s.\sigma}_{M'} \\ 699296341Sdelphij\den{\alpha\!s,\!x\!s.t}_{M} & = & \den{\alpha\!s,\!x\!s.t}_{M'}. 700296341Sdelphij\end{eqnarray*} 701296341SdelphijConsequently if $(\Gamma,t)$ is a sequent over ${\sf Sig}_{\cal T}$ 702296341Sdelphij(and hence also over ${\sf Sig}_{{\cal T}'}$), then $\Gamma 703296341Sdelphij\models_{M} t$ if and only if $\Gamma \models_{M'} t$. Since ${\sf 704296341SdelphijAxioms}_{\cal T}\subseteq{\sf Axioms}_{{\cal T}'}$ and $M'$ is a model 705296341Sdelphijof ${\cal T}'$, it follows that $M$ is a model of $\cal T$. $M$ will 70655714Skrisbe called the {\em restriction}\index{restrictions, of models} of the 707296341Sdelphijmodel $M'$ of the theory ${\cal T}'$ to the subtheory $\cal T$. 708296341Sdelphij 709296341Sdelphij\bigskip 710296341Sdelphij 711296341SdelphijThere are two main mechanisms for making extensions of theories in \HOL: 712296341Sdelphij\begin{itemize} 713296341Sdelphij 714296341Sdelphij\item Extension by a constant specification (see Section~\ref{specs}). 715296341Sdelphij 716296341Sdelphij\item Extension by a type specification (see 717296341SdelphijSection~\ref{tyspecs}).\footnote{This theory extension mechanism is 71855714Skrisnot implemented in the \HOL{}4 system.} 719296341Sdelphij 720296341Sdelphij\end{itemize} 721296341SdelphijThe first mechanism allows `loose specification' of constants (as in 722296341Sdelphijthe {\bf Z} notation~\cite{Z}, for example); the latter allows new 723296341Sdelphijtypes and type-operators to be introduced. As special cases (when the 72455714Skristhing being specified is uniquely determined) one also has: 725296341Sdelphij\begin{itemize} 726296341Sdelphij 727296341Sdelphij\item Extension by a constant definition (see Section~\ref{defs}). 728296341Sdelphij 729296341Sdelphij\item Extension by a type definition (see Section~\ref{tydefs}). 73055714Skris 731296341Sdelphij\end{itemize} 732296341SdelphijThese mechanisms are described in the following sections. They all 733296341Sdelphijproduce {\it definitional extensions\/} in the sense that they extend 734296341Sdelphija theory by adding new constants and types which are defined in terms 735296341Sdelphijof properties of existing ones. Their key property is that the 736296341Sdelphijextended theory possesses a (standard) model if the original theory 737296341Sdelphijdoes. So a series of these extensions starting from the theory 738296341Sdelphij\theory{INIT} is guaranteed to result in a theory with a standard 73955714Skrismodel, and hence in a consistent theory. It is also possible to extend 740296341Sdelphijtheories simply by adding new uninterpreted constants and types. This 741296341Sdelphijpreserves consistency, but is unlikely to be useful without additional 742296341Sdelphijaxioms. However, when adding arbitrary new 743296341Sdelphijaxioms\index{axioms!dispensibility of adding}, there is no guarantee 744296341Sdelphijthat consistency is preserved. The advantages of postulation over 745296341Sdelphijdefinition have been likened by Bertrand Russell to the advantages of 746296341Sdelphijtheft over honest toil.\footnote{See page 71 of Russell's book {\sl 747296341SdelphijIntroduction to Mathematical Philosophy\/}.} As it is all too easy to 748296341Sdelphijintroduce inconsistent axiomatizations, users of the \HOL{} system are 749296341Sdelphijstrongly advised to resist the temptation to add axioms, but to toil 750296341Sdelphijthrough definitional theories honestly. 751296341Sdelphij 752296341Sdelphij 753296341Sdelphij 754296341Sdelphij 755296341Sdelphij 756296341Sdelphij\subsection{Extension by constant definition} 757296341Sdelphij\index{extension, of HOL logic@extension, of \HOL{} logic!by constant definition|(} 758296341Sdelphij\label{defs} 75955714Skris 760296341SdelphijA {\it constant definition\/}\index{constant definition} over a 761296341Sdelphijsignature $\Sigma_{\Omega}$ is a formula of the form 762296341Sdelphij$\con{c}_{\sigma} = t_{\sigma}$, such that: 763296341Sdelphij\begin{myenumerate} 764296341Sdelphij 765296341Sdelphij\item 766296341Sdelphij$\con{c}$ is not the name of any constant in $\Sigma_{\Omega}$; 767296341Sdelphij 768296341Sdelphij\item 769296341Sdelphij$t_{\sigma}$ a closed term in ${\sf Terms}_{\Sigma_{\Omega}}$; 770109998Smarkm 771296341Sdelphij\item 772296341Sdelphijall the type variables occurring in $t_\sigma$ also occur in $\sigma$. 773296341Sdelphij 774296341Sdelphij\end{myenumerate} 775296341Sdelphij 776296341SdelphijGiven a theory $\cal T$ and such a constant definition over ${\sf 777296341SdelphijSig}_{\cal T}$, then the {\em definitional extension\/}\index{constant definition extension, of HOL logic@constant definition extension, of \HOL{} logic!abstract form of} of ${\cal T}$ 778296341Sdelphijby $\con{c}_{\sigma}=t_{\sigma}$ is the theory ${\cal T}{+_{\it 779296341Sdelphijdef}}\langle 780296341Sdelphij\con{c}_{\sigma}=t_{\sigma}\rangle$ defined by: 781296341Sdelphij\[ 782246772Sjkim{\cal T}{+_{\it def}}\langle 783296341Sdelphij\con{c}_{\sigma}=t_{\sigma}\rangle\ =\ \langle 784296341Sdelphij\begin{array}[t]{l} 785296341Sdelphij{\sf Struc}_{\cal T},\ 786296341Sdelphij{\sf Sig}_{\cal T}\cup\{(\con{c},\sigma)\},\\ 787296341Sdelphij{\sf Axioms}_{\cal T}\cup\{ 788296341Sdelphij\con{c}_{\sigma}=t_{\sigma} \},\ 789246772Sjkim{\sf Theorems}_{\cal T}\rangle 790296341Sdelphij\end{array} 791296341Sdelphij\] 792246772Sjkim 793296341SdelphijNote that the mechanism of extension by constant definition has 794296341Sdelphijalready been used implicitly in forming the theory \theory{LOG} from 795296341Sdelphijthe theory \theory{MIN} in Section~\ref{LOG}. Thus with the notation 796160814Ssimonof this section one has 797160814Ssimon\[ 798296341Sdelphij\theory{LOG}\; =\; \theory{MIN}\;\begin{array}[t]{@{}l} 799296341Sdelphij {+_{\it def}} \langle \T\index{T@\holtxt{T}!abstract form of}\index{truth values, in HOL logic@truth values, in \HOL{} logic!abstract form of} \ =\ 800160814Ssimon ((\lquant{x_{\ty{bool}}}x) = (\lquant{x_{\ty{bool}}}x))\rangle\\ 801296341Sdelphij {+_{\it def}}\langle {\forall}\index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!abstract form of}\ =\ \lquant{P_{\alpha\fun\ty{bool}}}\ P = 802296341Sdelphij (\lquant{x}\T )\rangle\\ 803296341Sdelphij {+_{\it def}}\langle {\exists}\index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abstract form of}\ =\ 804296341Sdelphij \lquant{P_{\alpha\fun\ty{bool}}}\ P({\hilbert}\ P)\rangle\\ 805296341Sdelphij {+_{\it def}}\langle \F\index{F@\holtxt{F}!abstract form of} 806296341Sdelphij \ =\ \uquant{b_{\ty{bool}}}\ b\rangle\\ 80755714Skris {+_{\it def}}\langle \neg\ =\ \lquant{b}\ b \imp \F \rangle\index{negation, in HOL logic@negation, in \HOL{} logic!abstract form of}\\ 80855714Skris {+_{\it def}}\langle {\wedge}\index{conjunction, in HOL logic@conjunction, in \HOL{} logic!abstract form of}\ =\ \lquant{b_1\ b_2}\uquant{b} 809296341Sdelphij (b_1\imp (b_2 \imp b)) \imp b\rangle\\ 810296341Sdelphij {+_{\it def}}\langle {\vee}\index{disjunction, in HOL logic@disjunction, in \HOL{} logic!abstract form of}\ =\ \lquant{b_1\ b_2}\uquant{b} 811296341Sdelphij (b_1 \imp b)\imp ((b_2 \imp b) \imp b)\rangle\\ 81255714Skris {+_{\it def}}\langle\OneOne \ =\ \lquant{f_{\alpha \fun\beta}} 813296341Sdelphij \uquant{x_1\ x_2} (f\ x_1 = f\ x_2) \imp (x_1 = x_2)\rangle\index{one-to-one predicate, in HOL logic@one-to-one predicate, in \HOL{} logic!abstract form of}\\ 814296341Sdelphij {+_{\it def}}\langle\Onto \ =\ \lquant{f_{\alpha\fun\beta}}\index{onto predicate, in HOL logic@onto predicate, in \HOL{} logic!abstract form of} 815296341Sdelphij \uquant{y}\equant{x} y = f\ x\rangle\\ 81655714Skris {+_{\it def}}\langle\TyDef \ =\ 817296341Sdelphij \begin{array}[t]{@{}l} 818296341Sdelphij \lambda P_{\alpha\fun\ty{bool}}\ rep_{\beta\fun\alpha}.\\ 819296341Sdelphij \OneOne\ rep\ \ \wedge\\ 82055714Skris (\uquant{x}P\ x \ =\ (\equant{y} x = rep\ y)) \rangle\\ 821296341Sdelphij\end{array}\end{array} 822296341Sdelphij\] 823296341Sdelphij 824296341SdelphijIf $\cal T$ possesses a standard model then so does the extension 825296341Sdelphij${\cal T}{+_{\it def}}\langle\con{c}_{\sigma}=t_{\sigma}\rangle$. This 82655714Skriswill be proved as a corollary of the corresponding result in 827296341SdelphijSection~\ref{specs} by showing that extension by constant definition 828296341Sdelphijis in fact a special case of extension by constant specification. 829296341Sdelphij(This reduction requires that one is dealing with {\em standard\/} 830296341Sdelphijtheories in the sense of section~\ref{INIT}, since although 831296341Sdelphijexistential quantification is not needed for constant definitions, it 832296341Sdelphijis needed to state the mechanism of constant specification.) 833296341Sdelphij 834296341Sdelphij\medskip 83555714Skris 836296341Sdelphij\noindent{\bf Remark\ } Condition (iii) in the definition of 837296341Sdelphijwhat constitutes a correct constant definition is an important 838296341Sdelphijrestriction without which consistency could not be guaranteed. To see 839296341Sdelphijthis, consider the term $\equant{f_{\alpha\fun\alpha}} \OneOne \ f 840296341Sdelphij\conj \neg(\Onto \ f)$, which expresses the proposition that (the set 841296341Sdelphijof elements denoted by the) type $\alpha$ is infinite. The term contains the 842296341Sdelphijtype variable $\alpha$, whereas the type of the term, $\ty{bool}$, 843296341Sdelphijdoes not. Thus by (iii) 844296341Sdelphij\[ 845296341Sdelphij\con{c}_\ty{bool} = 846296341Sdelphij\equant{f_{\alpha\fun\alpha}} \OneOne \ f \conj \neg(\Onto \ f) 84755714Skris\] 84855714Skrisis not allowed as a constant definition. The problem is that the 849296341Sdelphijmeaning of the right hand side of the definition varies with $\alpha$, 850296341Sdelphijwhereas the meaning of the constant on the left hand side is fixed, 851296341Sdelphijsince it does not contain $\alpha$. Indeed, if we were allowed to 852296341Sdelphijextend the consistent theory $\theory{INIT}$ by this definition, the 853296341Sdelphijresult would be an inconsistent theory. For instantiating $\alpha$ to 854296341Sdelphij$\ty{ind}$ in the right hand side results in a term that is provable 855296341Sdelphijfrom the axioms of $\theory{INIT}$, and hence $\con{c}_\ty{bool}=\T$ is 856296341Sdelphijprovable in the extended theory. But equally, instantiating $\alpha$ 857296341Sdelphijto $\ty{bool}$ makes the negation of the right hand side provable 858296341Sdelphijfrom the axioms of $\theory{INIT}$, and hence $\con{c}_\ty{bool}=\F$ is 859296341Sdelphijalso provable in the extended theory. Combining these theorems, one 860296341Sdelphijhas that $\T=\F$, \ie\ $\F$ is provable in the extended theory. 861296341Sdelphij\index{extension, of HOL logic@extension, of \HOL{} logic!by constant definition|)} 862296341Sdelphij 863296341Sdelphij\subsection{Extension by constant specification} 864296341Sdelphij\index{extension, of HOL logic@extension, of \HOL{} logic!by constant specification|(} 865296341Sdelphij\label{specs} 866296341Sdelphij 867296341SdelphijConstant specifications\index{constant specification extension, of HOL logic@constant specification extension, of \HOL{} logic!abstract form 868296341Sdelphijof} introduce constants (or sets of constants) 869296341Sdelphijthat satisfy arbitrary given (consistent) properties. For example, a 870296341Sdelphijtheory could be extended by a constant specification to have two new 871296341Sdelphijconstants $\con{b}_1$ and $\con{b}_2$ of type \ty{bool} such that 872296341Sdelphij$\neg(\con{b}_1=\con{b}_2)$. This specification does not uniquely 873296341Sdelphijdefine $\con{b}_1$ and $\con{b}_2$, since it is satisfied by either 874296341Sdelphij$\con{b}_1=\T$ and $\con{b}_2=\F$, or $\con{b}_1=\F$ and 875296341Sdelphij$\con{b}_2=\T$. To ensure that such specifications are 876296341Sdelphijconsistent\index{consistency, of HOL logic@consistency, of \HOL{} logic!under constant specification}, they can only be made if it has 877296341Sdelphijalready been proved that the properties which the new constants are to 878296341Sdelphijhave are consistent. This rules out, for example, introducing three 879296341Sdelphijboolean constants $\con{b}_1$, $\con{b}_2$ and $\con{b}_3$ such that 880296341Sdelphij$\con{b}_1\neq \con{b}_2$, $\con{b}_1\neq \con{b}_3$ and 881296341Sdelphij$\con{b}_2\neq \con{b}_3$. 882296341Sdelphij 883296341SdelphijSuppose $\equant{x_1\cdots x_n}t$ is a formula, with $x_1,\ldots, x_n$ 884296341Sdelphijdistinct variables. If $\turn \equant{x_1 \cdots x_n}t$, then a 885296341Sdelphijconstant specification allows new constants $\con{c}_1$, $\ldots$ , 886296341Sdelphij$\con{c}_n$ to be introduced satisfying: 887296341Sdelphij\[ 888296341Sdelphij\turn t[\con{c}_1,\cdots,\con{c}_n/x_1,\cdots,x_n] 889296341Sdelphij\] 890296341Sdelphijwhere $t[\con{c}_1,\cdots,\con{c}_n/x_1,\cdots,x_n]$ denotes the 891296341Sdelphijresult of simultaneously substituting $\con{c}_1, \ldots, \con{c}_n$ 892296341Sdelphijfor $x_1, \ldots, x_n$ respectively. Of course the type of each 893296341Sdelphijconstant $\con{c}_i$ must be the same as the type of the corresponding 894296341Sdelphijvariable $x_i$. To ensure that this extension mechanism preserves the 895296341Sdelphijproperty of possessing a model, a further more technical requirement 896296341Sdelphijis imposed on these types: they must each contain all the type 897296341Sdelphijvariables occurring in $t$. This condition is discussed further in 898296341SdelphijSection~\ref{constants} below. 899296341Sdelphij 900296341SdelphijFormally, a {\em constant specification\/}\index{constant specification} 901296341Sdelphijfor a theory ${\cal T}$ is given by 902296341Sdelphij 903296341Sdelphij\medskip 904296341Sdelphij\noindent{\bf Data} 905296341Sdelphij\[ 906296341Sdelphij\langle(\con{c}_1,\ldots,\con{c}_n), 907296341Sdelphij\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}}\rangle 908296341Sdelphij\] 909296341Sdelphij 910296341Sdelphij\noindent{\bf Conditions} 911296341Sdelphij\begin{myenumerate} 912296341Sdelphij 913296341Sdelphij\item 914296341Sdelphij$\con{c}_1,\ldots,\con{c}_n$ are distinct names that 915296341Sdelphijare not the names of any constants in ${\sf Sig}_{\cal T}$. 916296341Sdelphij 917\item 918$\lquant{{x_1}_{\sigma_1} 919\cdots {x_n}_{\sigma_n}}t_{\ty{bool}}\ \in\ {\sf Terms}_{\cal T}$. 920 921\item 922$tyvars(t_{\ty{bool}})\ =\ tyvars(\sigma_i)$ for $1\leq i\leq n$. 923 924\item 925$\equant{{x_1}_{\sigma_1}\ \cdots\ {x_n}_{\sigma_n}}t 926\ \in\ {\sf Theorems}_{\cal T}$. 927 928\end{myenumerate} 929The extension of a standard theory ${\cal T}$ by such a constant 930specification is denoted by 931\[ 932{\cal T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 933\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} \rangle 934\] 935and is defined to be the theory: 936\[ 937\langle 938\begin{array}[t]{@{}l} 939{\sf Struc}_{\cal T},\\ 940{\sf Sig}_{\cal T} \cup 941\{{\con{c}_1}_{\sigma_1}, \ldots, 942{\con{c}_n}_{\sigma_n}\},\\ 943{\sf Axioms}_{\cal T}\cup 944\{ t[\con{c}_1,\ldots,\con{c}_n/x_1,\ldots,x_n] \},\\ 945{\sf Theorems}_{\cal T} 946\rangle 947\end{array} 948\] 949 950\noindent{\bf Proposition\ }{\em 951The theory ${\cal 952T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 953\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} 954\rangle$ has a standard model if the theory ${\cal T}$ does.} 955 956\medskip 957 958\noindent{\bf Proof\ } 959Suppose $M$ is a standard model of ${\cal T}$. Let 960$\alpha\!s=\alpha_{1},\ldots,\alpha_{m}$ be the list of distinct type 961variables occurring in the formula $t$. Then $\alpha\!s,\!x\!s.t$ is a 962term-in-context, where $x\!s=x_{1},\ldots,x_{n}$. (Change any bound 963variables in $t$ to make them distinct from $x\!s$ if necessary.) 964Interpreting this term-in-context in the model $M$ yields 965\[ 966\den{\alpha\!s,\!x\!s.t}_{M} \in \prod_{X\!s\in{\cal U}^{m}} 967\left(\prod_{i=1}^{n}\den{\alpha\!s.\sigma_{i}}_{M}(X\!s)\right) 968\fun \two 969\] 970Now $\equant{x\!s}t$ is in ${\sf Theorems}_{\cal T}$ and hence by the 971Soundness Theorem \ref{soundness}\index{consistency, of HOL logic@consistency, of \HOL{} logic!under constant specification} this 972sequent is satisfied by $M$. Using the semantics of $\exists$ given in 973Section~\ref{LOG}, this means that for all $X\!s\in{\cal 974U}^{m}$ the set 975\[ 976S(X\!s) = \{y\!s\in\den{\alpha\!s.\sigma_{1}}_{M}(X\!s) \times\cdots\times 977 \den{\alpha\!s.\sigma_{n}}_{M}(X\!s)\; : \; 978 \den{\alpha\!s,\!x\!s.t}_{M}(X\!s)(y\!s)=1 \} 979\] 980is non-empty. Since it is also a subset of a finite product of sets in 981$\cal U$, it follows that it is an element of $\cal U$ (using properties 982{\bf Sub} and {\bf Prod} of the universe). So one can apply the global 983choice function $\ch\in\prod_{X\in{\cal U}}X$ to select a specific element 984\[ 985(s_{1}(X\!s),\ldots,s_{n}(X\!s)) = 986\ch(S(X\!s)) \in \prod_{i=1}^{n}\den{\alpha\!s.\sigma_{i}}_{M}(X\!s) 987\] 988at which $\den{\alpha\!s,\!x\!s.t}_{M}(X\!s)$ takes the value $1$. Extend 989$M$ to a model $M'$ of the signature of ${\cal 990T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 991\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} 992\rangle$ by defining its value at 993each new constant $(\con{c}_{i},\sigma_{i})$ to be 994\[ 995M'(\con{c}_{i},\sigma_{i}) = 996s_{i} \in \prod_{X\!s\in{\cal U}^{m}}\den{\sigma_{i}}_{M}(X\!s) . 997\] 998Note that the Condition (iii) in the definition of a constant 999specification ensures that $\alpha\!s$ is the canonical context of each 1000type $\sigma_{i}$, so that 1001$\den{\sigma_{i}}=\den{\alpha\!s.\sigma_{i}}$ and thus $s_{i}$ is 1002indeed an element of the above product. 1003 1004Since $t$ is a term of the subtheory $\cal T$ of ${\cal 1005T}{+_{\it spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 1006\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} 1007\rangle$, 1008as remarked at the beginning of Section~\ref{extensions}, one has that 1009$\den{\alpha\!s,\!x\!s.t}_{M'} = \den{\alpha\!s,\!x\!s.t}_{M}$. Hence by 1010definition of the $s_{i}$, for all $X\!s\in{\cal U}^{m}$ 1011\[ 1012\den{\alpha\!s,\!x\!s.t}_{M'}(X\!s)(s_{1}(X\!s),\ldots,s_{n}(X\!s)) = 1 1013\] 1014Then using Lemma~4 in Section 1015\ref{term-substitution} on the semantics of substitution together with 1016the definition of $\den{\con{c}_{i}}_{M'}$, one finally obtains that 1017for all $X\!s\in{\cal U}^{m}$ 1018\[ 1019\den{t[\con{c}_{1},\ldots,\con{c}_{n}/x_{1},\ldots,x_{n}]}_{M'}(X\!s)=1 1020\] 1021or in other words that $M'$ satisfies 1022$t[\con{c}_{1},\ldots,\con{c}_{n}/x_{1},\ldots,x_{n}]$. 1023Hence $M'$ is a model of ${\cal T}{+_{\it 1024spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 1025\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} 1026\rangle$, as required. 1027 1028\medskip 1029 1030The constants which are asserted to exist in a constant specification 1031are not necessarily uniquely determined. Correspondingly, there may 1032be many different models of ${\cal T}{+_{\it 1033spec}}\langle(\con{c}_1,\ldots,\con{c}_n), 1034\lquant{{x_1}_{\sigma_1},\ldots,{x_n}_{\sigma_n}}t_{\ty{bool}} 1035\rangle$ whose restriction to $\cal T$ is $M$; the above construction 1036produces such a model in a uniform manner by making use of the global 1037choice function on the universe. 1038 1039Extension by a constant definition, $\con{c}_\sigma=t_\sigma$, is a 1040special case of extension by constant specification. For let $t'$ be 1041the formula $x_\sigma=t_\sigma$, where $x_\sigma$ is a variable not 1042occurring in $t_\sigma$. Then clearly $\turn 1043\equant{x_\sigma}t'$ and one can apply the method of constant 1044specification to obtain the theory 1045\[ 1046{\cal T}{+_{\it spec}}\langle \con{c},\lquant{x_\sigma}t'\rangle 1047\] 1048But since $t'[\con{c}_\sigma/x_\sigma]$ is just 1049$\con{c}_\sigma=t_\sigma$, 1050this extension yields exactly ${\cal T}{+_{\it def}}\langle 1051\con{c}_{\sigma}=t_{\sigma}\rangle$. 1052So as a corollary of the Proposition, one has that for each standard 1053model $M$ of $\cal T$, there is a standard model $M'$ of ${\cal 1054T}{+_{\it def}}\langle\con{c}_{\sigma}=t_{\sigma}\rangle$ whose 1055restriction to $\cal T$ is $M$. In contrast with the case of constant 1056specifications, $M'$ is uniquely determined by $M$ and the constant 1057definition. 1058\index{extension, of HOL logic@extension, of \HOL{} logic!by constant specification|)} 1059 1060\subsection{Remarks about constants in \HOL{}} 1061\label{constants} 1062 1063Note how Condition (iii) in the definition of a constant specification 1064was needed in the proof that the extension mechanism preserves the 1065property of possessing a standard model. Its role is to ensure that 1066the introduced constants have, via their types, the same dependency on 1067type variables as does the formula loosely specifying them. The 1068situation is the same as that discussed in the Remark in 1069Section~\ref{defs}. In a sense, what is causing the problem in the 1070example given in that Remark is not so much the method of extension by 1071introducing constants, but rather the syntax of \HOL{} which does not 1072allow constants to depend explicitly on type variables (in the way 1073that type operators can). Thus in the example one would like to 1074introduce a `polymorphic' constant $\con{c}_\ty{bool}(\alpha)$ 1075explicitly depending upon $\alpha$, and define it to be 1076$\equant{f_{\alpha\fun\alpha}} \OneOne \ f \conj 1077\neg(\Onto \ f)$. Then in the extended theory one could derive 1078$\con{c}_\ty{bool}(\ty{ind})=\T$ and 1079$\con{c}_\ty{bool}(\ty{bool})=\F$, but now no contradiction results since 1080$\con{c}_\ty{bool}(\ty{ind})$ and $\con{c}_\ty{bool}(\ty{bool})$ 1081are different. 1082 1083In the current version of \HOL, constants are (name,type)-pairs. 1084One can envision a slight extension of the \HOL{} syntax with 1085`polymorphic' constants, specified by pairs 1086$(\con{c},\alpha\!s.\sigma)$ where now $\alpha\!s.\sigma$ is a 1087type-in-context and the list $\alpha\!s$ may well contain extra type 1088variables not occurring in $\sigma$. Such a pair would give rise 1089to the particular constant term 1090$\con{c}_\sigma(\alpha\!s)$, and more generally to 1091constant terms $\con{c}_{\sigma'}(\tau\!s)$ obtained from 1092this one by instantiating the type variables $\alpha_i$ with types 1093$\tau_i$ (so $\sigma'$ is the instance of $\sigma$ obtained by 1094substituting $\tau\!s$ for $\alpha\!s$). This new syntax of polymorphic 1095constants is comparable to the existing syntax of compound types (see 1096section~\ref{types}): an $n$-ary type operator $\textsl{op}$ gives rise to a 1097compound type $(\alpha_1,\ldots,\alpha_n){\textsl{op}}$ depending upon $n$ 1098type variables. Similarly, the above syntax of polymorphic constants 1099records how they depend upon type variables (as well as which generic 1100type the constant has). 1101 1102However, explicitly recording dependency of constants on type variables 1103makes for a rather cumbersome syntax which in practice one would like 1104to avoid where possible. It is possible to avoid it if the type 1105context $\alpha\!s$ in $(\con{c},\alpha\!s.\sigma)$ is actually the 1106{\em canonical\/} context of $\sigma$, \ie\ contains exactly the type 1107variables of $\sigma$. For then one can apply Lemma~1 of 1108Section~\ref{instances-and-substitution} to deduce that the 1109polymorphic constant $\con{c}_{\sigma'}(\tau\!s)$ can be abbreviated 1110to the ordinary constant $\con{c}_{\sigma'}$ without ambiguity---the 1111missing information $\tau\!s$ can be reconstructed from $\sigma'$ and 1112the information about the constant $\con{c}$ given in the signature. 1113From this perspective, the rather technical side Conditions (iii) in 1114Sections~\ref{defs} and \ref{specs} become rather less mysterious: 1115they precisely ensure that in introducing new constants one is always 1116dealing just with canonical contexts, and so can use ordinary constants 1117rather than polymorphic ones without ambiguity. In this way one avoids 1118complicating the existing syntax at the expense of restricting 1119somewhat the applicability of these theory extension mechanisms. 1120 1121 1122\subsection{Extension by type definition} 1123\index{extension, of HOL logic@extension, of \HOL{} logic!by type definition|(} 1124\index{representing types, in HOL logic@representing types, in \HOL{} logic!abstract form of|(} 1125\label{tydefs} 1126 1127Every (monomorphic) type $\sigma$ in the initial theory \theory{INIT} 1128determines a set $\den{\sigma}$ in the universe $\cal U$. However, 1129there are many more sets in $\cal U$ than there are types in 1130\theory{INIT}. In particular, whilst $\cal U$ is closed under the 1131operation of taking a non-empty subset of $\den{\sigma}$, there is no 1132corresponding mechanism for forming a `subtype' of $\sigma$. Instead, 1133subsets are denoted indirectly via characteristic functions, whereby a 1134closed term $p$ of type $\sigma\fun\ty{bool}$ determines the subset 1135$\{x\in\den{\sigma} : \den{p}(x)=1\}$ (which is a set in the universe 1136provided it is non-empty). However, it is useful to have a 1137mechanism for introducing new types which are subtypes of existing 1138ones. Such types are defined\index{extension, of HOL logic@extension, of \HOL{} logic!by type definition} in \HOL{} by introducing a new type 1139constant and asserting an axiom that characterizes it as denoting a 1140set in bijection (\ie\ one-to-one correspondence) with a non-empty 1141subset of an existing type (called the {\it representing type\/}). 1142For example, the type \ml{num} is defined to be equal to a countable 1143subset of the type \ml{ind}, which is guaranteed to exist by the axiom 1144{\small\tt INFINITY\_AX} (see Section~\ref{INIT}). 1145 1146As well as defining types, it is also convenient to be able to define 1147type operators. An example would be a type operator \ty{inj} which 1148mapped a set to the set of one-to-one (\ie\ injective) functions on 1149it. The subset of $\sigma\fun\sigma$ representing $(\sigma)\ty{inj}$ 1150would be defined by the predicate \OneOne. Another example would be a 1151binary cartesian product type operator \ty{prod}. This is defined by 1152choosing a representing type containing two type variables, say 1153$\sigma[\alpha_1;\alpha_2]$, such that for any types $\sigma_1$ and 1154$\sigma_2$, a subset of $\sigma[\sigma_1;\sigma_2]$ represents the 1155cartesian product of $\sigma_1$ and $\sigma_2$. The details of such a 1156definition are given in \DESCRIPTION's section on the theory of 1157cartesian products. 1158 1159Types in \HOL{} must denote non-empty sets. Thus it is only 1160consistent\index{consistency, of HOL logic@consistency, of \HOL{} logic!under type definition} to define a new type isomorphic to a 1161subset specified by a predicate $p$, if there is at least one thing 1162for which $p$ holds, \ie\ $\turn\equant{x}p\ x$. For example, it 1163would be inconsistent to define a binary type operator \ty{iso} such 1164that $(\sigma_1,\sigma_2)\ty{iso}$ denoted the set of one-to-one 1165functions from $\sigma_1$ {\em onto\/} $\sigma_2$ because for some 1166values of $\sigma_1$ and $\sigma_2$ the set would be empty; for 1167example $(\ty{ind},\ty{bool})\ty{iso}$ would denote the empty set. To 1168avoid this, a precondition of defining a new type is that the 1169representing subset is non-empty. 1170 1171To summarize, a new type is defined by: 1172\begin{enumerate} 1173\item Specifying an existing type. 1174\item Specifying a subset of this type. 1175\item Proving that this subset is non-empty. 1176\item Specifying that the new type is isomorphic to this subset. 1177\end{enumerate} 1178 1179\noindent In more detail, 1180defining a new type $(\alpha_1,\ldots,\alpha_n)\ty{op}$ consists in: 1181\begin{enumerate} 1182\item 1183Specifying a type-in-context, $\alpha_1,\ldots,\alpha_n.\sigma$ say. 1184The type 1185$\sigma$ is called the {\it representing type\/}, and the type 1186$(\alpha_1,\ldots,\alpha_n)\ty{op}$ is intended to be isomorphic to a 1187subset of $\sigma$. 1188 1189\item 1190Specifying a closed term-in-context, $\alpha_1,\ldots,\alpha_n,.p$ 1191say, of type $\sigma\fun\bool$. The term $p$ is called the {\it 1192characteristic function\/}\index{characteristic function, of type definitions}. This defines the subset of $\sigma$ to which 1193$(\alpha_1,\ldots,\alpha_n)\ty{op}$ is to be isomorphic.\footnote{The 1194reason for restricting $p$ to be closed, \ie\ to have no free 1195variables, is that otherwise for consistency the defined type operator 1196would have to {\em depend\/} upon (\ie\ be a function of) those 1197variables. Such dependent types are not (yet!) a part of the \HOL{} system.} 1198 1199\item 1200Proving $\turn \equant{x_{\sigma}} p\ x$. 1201 1202\item 1203Asserting an axiom saying that $(\alpha_1,\ldots,\alpha_n)\ty{op}$ is 1204isomorphic to the subset of $\sigma$ selected by $p$. 1205 1206\end{enumerate} 1207 1208To make this formal, the theory \theory{LOG} provides 1209the polymorphic constant \TyDef\ defined in Section~\ref{LOG}. 1210The formula 1211$\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\ p\ f$ 1212asserts that 1213there exists a one-to-one map $f$ from $(\alpha_1,\ldots,\alpha_n)\ty{op}$ 1214onto the subset of elements of $\sigma$ for which $p$ is true. 1215Hence, the axiom that characterizes $(\alpha_1,\ldots,\alpha_n)\ty{op}$ is: 1216\[ 1217\turn \equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}\TyDef\ 1218p\ f 1219\] 1220 1221Defining a new type $(\alpha_1,\ldots,\alpha_n)\ty{op}$ in a theory 1222${\cal T}$ thus consists of introducing $\ty{op}$ as a new $n$-ary 1223type operator and the above axiom as a new axiom. Formally, a {\em 1224type definition\/}\index{type definitions, in HOL logic@type definitions, in \HOL{} logic!abstract structure of} for a theory ${\cal 1225T}$ is given by 1226 1227\medskip 1228 1229\noindent{\bf Data} 1230\[ 1231\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\ \sigma,\ 1232p_{\sigma\fun\ty{bool}}\rangle 1233\] 1234 1235\noindent{\bf Conditions} 1236 1237\begin{myenumerate} 1238\item 1239$(\ty{op},n)$ is not the name of a type constant in ${\sf Struc}_{\cal T}$. 1240 1241\item 1242$\alpha_1,\ldots,\alpha_n.\sigma$ is a type-in-context with $\sigma 1243\in{\sf Types}_{\cal T}$. 1244 1245\item $p_{\sigma\fun\bool}$ is a closed term in ${\sf Terms}_{\cal T}$ 1246whose type variables occur in $\alpha_1,\ldots,\alpha_n$. 1247 1248\item 1249$\equant{x_{\sigma}}p\ x \ \in\ {\sf Theorems}_{\cal T}$. 1250\end{myenumerate} 1251 1252The extension of a standard theory ${\cal T}$ by a such a type definition 1253is denoted by 1254\[ 1255{\cal 1256T}{+_{tydef}}\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle 1257\] 1258and defined to be the theory 1259\[ 1260\langle 1261\begin{array}[t]{@{}l} 1262{\sf Struc}_{\cal T}\cup\{(\ty{op},n)\},\\ 1263 {\sf Sig}_{\cal T},\\ 1264 {\sf Axioms}_{\cal T}\cup\{ 1265\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op} 1266\fun\sigma}}\TyDef\ p\ f\},\\ 1267 {\sf Theorems}_{\cal T}\rangle\\ 1268\end{array} 1269\] 1270 1271\medskip 1272 1273\noindent{\bf Proposition\ }{\em 1274The theory ${\cal T}{+_{\it 1275tydef}}\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle$ has a 1276standard model if the theory ${\cal T}$ does.} 1277 1278\medskip 1279 1280Instead of giving a direct proof of this result, it will be deduced as 1281a corollary of the corresponding proposition in the next section. 1282\index{extension, of HOL logic@extension, of \HOL{} logic!by type definition|)} 1283\index{representing types, in HOL logic@representing types, in \HOL{} logic!abstract form of|)} 1284 1285 1286\subsection{Extension by type specification} 1287\index{extension, of HOL logic@extension, of \HOL{} logic!by type specification|(} 1288\label{tyspecs} 1289\noindent 1290(\textbf{Note:} This theory extension mechanism is \emph{not} 1291implemented in the HOL4 system. It was proposed by T.~Melham and 1292refines a suggestion from R.~Jones and R.~Arthan.) 1293 1294\smallskip 1295\noindent The type definition 1296mechanism allows one to introduce new types by giving a concrete 1297representation of the type as a `subtype' of an existing type. One 1298might instead wish to introduce a new type satisfying some property 1299without having to give an explicit representation for the type. For 1300example, one might want to extend \theory{INIT} with an atomic type 1301$\ty{one}$ satisfying $\turn\uquant{f_{\alpha\fun\ty{one}}\ 1302 g_{\alpha\fun\ty{one}}}f=g$ without choosing a specific type in 1303$\theory{INIT}$ and saying that $\ty{one}$ is in bijection with a 1304one-element subset of it. (The idea being that the choice of 1305representing type is irrelevant to the properties of $\ty{one}$ that 1306can be expressed in \HOL.) The mechanism described in this section 1307provides one way of achieving this while at the same time preserving 1308the all-important property of possessing a standard model and hence 1309maintaining consistency. 1310 1311Each closed formula $q$ involving a single type variable $\alpha$ can 1312be thought of as specifying a property $q[\tau/\alpha]$ of types 1313$\tau$. Its interpretation in a model is of the form 1314\[ 1315\den{\alpha,.q}\in \prod_{X\in{\cal U}}\den{\alpha.\bool}(X) 1316\;= \prod_{X\in{\cal U}}\two \;=\; {\cal U}\fun\two 1317\] 1318which is a characteristic function on the universe, determining a 1319subset $\{X\in{\cal U}:\den{\alpha,.q}(X)=1\}$ consisting of those 1320sets in the universe for which the property $q$ holds. The most 1321general way of ensuring the consistency of introducing a new atomic 1322type $\nu$ satisfying $q[\nu/\alpha]$ would be to prove 1323`$\equant{\alpha}q$'. However, such a 1324formula with quantification over types is not\footnote{yet!} a part of 1325the \HOL{} logic and one must proceed indirectly---replacing the 1326formula by (a logically weaker) one that can be expressed formally with 1327\HOL{} syntax. The formula used is 1328\[ 1329(\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ p\ f)\ \imp\ q 1330\] 1331where $\sigma$ is a type, $p_{\sigma\fun\ty{bool}}$ is a closed term 1332and neither involve the type variable $\alpha$. This formula says `$q$ 1333holds of any type which is in bijection with the subtype of $\sigma$ 1334determined by $p$'. If this formula is provable and if the subtype is 1335non-empty, \ie\ if 1336\[ 1337\equant{x_\sigma}p\ x 1338\] 1339is provable, then it is consistent to introduce an extension with a new 1340atomic type $\nu$ satisfying $q[\nu/\alpha]$. 1341 1342In giving the formal definition of this extension mechanism, two 1343refinements will be made. Firstly, $\sigma$ is allowed to be 1344polymorphic and hence a new type constant of appropriate arity is 1345introduced, rather than just an atomic type. Secondly, the above 1346existential formulas are permitted to be proved (in the theory to be 1347extended) from some hypotheses.\footnote{This refinement increases the 1348applicability of the extension mechanism without increasing its 1349expressive power. A similar refinement could have be made to the other 1350theory extension mechanisms.} Thus a {\em type 1351specification\/}\index{type specification} for a theory $\cal T$ is 1352given by 1353 1354\medskip 1355 1356\noindent{\bf Data} 1357\[ 1358\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q\rangle 1359\] 1360 1361\noindent{\bf Conditions} 1362 1363\begin{myenumerate} 1364\item 1365$(\ty{op},n)$ is a type constant that is not in 1366${\sf Struc}_{\cal T}$. 1367 1368\item 1369$\alpha_1,\ldots,\alpha_n.\sigma$ is a type-in-context with 1370$\sigma\in{\sf Types}_{\cal T}$. 1371 1372\item $p_{\sigma\fun\bool}$ is a closed term in ${\sf Terms}_{\cal T}$ 1373whose type variables occur in $\alpha\!s=\alpha_1,\ldots,\alpha_n$. 1374 1375\item $\alpha$ is a type variable distinct from those in 1376$\alpha\!s$. 1377 1378\item $\Gamma$ is a list of closed formulas in ${\sf Terms}_{\cal T}$ 1379not involving the type variable $\alpha$. 1380 1381\item $q$ is a closed formula in ${\sf Terms}_{\cal T}$. 1382 1383\item The sequents 1384\begin{eqnarray*} 1385(\Gamma & , & \equant{x_\sigma}p\ x )\\ 1386(\Gamma & , & (\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ 1387 p\ f)\ \imp\ q ) 1388\end{eqnarray*} 1389are in ${\sf Theorems}_{\cal T}$. 1390 1391\end{myenumerate} 1392The extension of a standard theory $\cal T$ by such a type 1393specification is denoted 1394\[ 1395{\cal T}{+_{\it tyspec}} \langle 1396(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q\rangle 1397\] 1398and is defined to be the theory 1399\[ 1400\langle 1401\begin{array}[t]{@{}l} 1402{\sf Struc}_{\cal T}\cup\{(\ty{op},n)\},\\ 1403 {\sf Sig}_{\cal T},\\ 1404 {\sf Axioms}_{\cal 1405 T}\cup\{(\Gamma , q[(\alpha_1,\ldots,\alpha_n)\ty{op}/\alpha])\},\\ 1406 {\sf Theorems}_{\cal T}\rangle 1407\end{array} 1408\] 1409 1410\noindent{\bf Example\ } To carry out the extension of \theory{INIT} 1411mentioned at the start of this section, one forms 1412\[ 1413\theory{INIT}{+_{\it tyspec}} \langle 1414()\ty{one},\ty{bool},p,\alpha,\emptyset,q\rangle 1415\] 1416where $p$ is the term $\lquant{b_\bool}b$ and $q$ is the formula 1417$\uquant{f_{\beta\fun\alpha}\ g_{\beta\fun\alpha}}f=g$. Thus the 1418result is a theory extending \theory{INIT} with a 1419new type constant $\ty{one}$ satisfying the axiom 1420$\uquant{f_{\beta\fun\ty{one}}\ g_{\beta\fun\ty{one}}}f=g$. 1421 1422To verify that this is a correct application of the extension 1423mechanism, one has to check Conditions (i) to (vii) above. Only the last 1424one is non-trivial: it imposes the obligation of proving 1425two sequents from the axioms of \theory{INIT}. The first sequent says 1426that $p$ defines an inhabited subset of $\bool$, which is certainly 1427the case since $\T$ witnesses this fact. The second sequent says in 1428effect that any type $\alpha$ that is in bijection with the subset of 1429$\bool$ defined by $p$ has the property that there is at most one 1430function to it from any given type $\beta$; the proof of this from the 1431axioms of \theory{INIT} is left as an exercise. 1432 1433\medskip 1434 1435\noindent{\bf Proposition\ }{\em 1436The theory ${\cal T}{+_{\it tyspec}}\langle 1437(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\Gamma,q 1438\rangle$ has a standard model if the theory ${\cal T}$ does.} 1439 1440\medskip 1441 1442\noindent{\bf Proof\ } 1443Write $\alpha\!s$ for $\alpha_1,\ldots,\alpha_n$, and suppose that 1444$\alpha\!s'={\alpha'}_1,\ldots,{\alpha'}_m$ is the list of type 1445variables occurring in $\Gamma$ and $q$, but not already in the list 1446$\alpha\!s,\alpha$. 1447 1448Suppose $M$ is a standard model of ${\cal T}$. Since $\alpha\!s,.p$ is 1449a term-in-context of type $\sigma\fun\ty{bool}$, interpreting it in 1450$M$ yields 1451\[ 1452\den{\alpha\!s,.p}_{M} 1453\in \prod_{X\!s\in{\cal U}^{n}}\den{\alpha\!s.\sigma\fun\ty{bool}}_M(X\!s) 1454= \prod_{X\!s\in{\cal U}^{n}} 1455 \den{\alpha\!s.\sigma}_M(X\!s)\fun\two . 1456\] 1457 1458There is no loss of generality in assuming that $\Gamma$ consists of a 1459single formula $\gamma$. (Just replace $\Gamma$ by the conjunction of 1460the formulas it contains, with the convention that this conjunction is 1461$\T$ if $\Gamma$ is empty.) By assumption on $\alpha\!s'$ and by 1462Condition~(iv), $\alpha\!s,\alpha\!s',.\gamma$ is a term-in-context.\footnote{Note the two commas in $\alpha\!s,\alpha\!s',.\gamma$. The first separates the two lists of type variables; the second splits type variables from term variables.} 1463Interpreting it in $M$ yields 1464\[ 1465\den{\alpha\!s,\alpha\!s',.\gamma}_{M} 1466\in \prod_{(X\!s,X\!s')\in 1467{\cal U}^{n+m}}\den{\alpha\!s,\alpha\!s'.\ty{bool}}_M(X\!s,X\!s') 1468={\cal U}^{n+m}\fun\two 1469\] 1470 1471Now $(\gamma,\equant{x_{\sigma}}p\ x)$ is in ${\sf Theorems}_{\cal T}$ 1472and hence by the Soundness Theorem~\ref{soundness} this sequent is 1473satisfied by $M$. Using the semantics of $\exists$ given in 1474Section~\ref{LOG} and the definition of satisfaction of a sequent from 1475Section~\ref{sequents}, this means that for all $(X\!s,X\!s')\in{\cal U}^{n+m}$ 1476if $\den{\alpha\!s,\alpha\!s',.\gamma}_M(X\!s,X\!s')=1$, then 1477the set 1478\[ 1479\{y\in\den{\alpha\!s.\sigma}_{M}\: :\: \den{\alpha\!s,.p}(X\!s)(y)=1\} 1480\] 1481is non-empty. (This uses the fact that $p$ does not involve 1482the type variables $\alpha\!s'$, so that by Lemma~4 in 1483Section~\ref{term-substitution} 1484$\den{\alpha\!s,\alpha\!s',.p}_M(X\!s,X\!s')=\den{\alpha\!s,.p}_M(X\!s)$.) 1485Since it is also a subset of a set in $\cal U$, it 1486follows by property {\bf Sub} of the universe that this set is an element of 1487$\cal U$. So defining 1488\[ 1489S(X\!s) = \left\{\hspace{-1mm} 1490\begin{array}{ll} 1491\{y\in\den{\alpha\!s.\sigma}_{M} : \den{\alpha\!s,.p}(X\!s)(y)=1\} 1492 & \mbox{\rm if $\den{\alpha\!s,.\gamma}_M(X\!s,X\!s')=1$, some $X\!s'$}\\ 14931 & \mbox{\rm otherwise} 1494\end{array} 1495\right.%\} 1496\] 1497one has that $S$ is a function ${\cal U}^n\fun{\cal U}$. Extend $M$ 1498to a model of the signature of ${\cal T}'$ by defining its value at 1499the new $n$-ary type constant $\ty{op}$ to be this function $S$. Note 1500that the values of $\sigma$, $p$, $\gamma$ and 1501$q$ in $M'$ are the same as in $M$, since these expressions do not 1502involve the new type constant $\ty{op}$. 1503 1504For each $X\!s\in{\cal U}^{n}$ define $i_{X\!s}$ to be the inclusion 1505function for the subset $S(X\!s)\subseteq\den{\alpha\!s.\sigma}_{M}$ 1506if $\den{\alpha\!s,\alpha\!s',.\gamma}_M(X\!s,X\!s')=1$ for some 1507$X\!s'$, and otherwise to be the function 1508$1\fun\den{\alpha\!s.\sigma}_{M}$ sending $0\in 1$ to 1509$\ch(\den{\alpha\!s.\sigma}_{M})$. Then 1510$i_{X\!s}\in(S(X\!s)\fun\den{\alpha\!s.\sigma}_{M'}(X\!s))$ because 1511$\den{\alpha\!s.\sigma}_{M'}=\den{\alpha\!s.\sigma}_M$. Using the 1512semantics of $\TyDef$ given in Section~\ref{LOG}, one has that for any 1513$(X\!s,X\!s')\in{\cal U}^{n+m}$, if 1514$\den{\alpha\!s,\alpha\!s',.\gamma}_{M'}(X\!s,X\!s')=1$ then 1515\[ 1516\den{\TyDef}_{M'}(\den{\alpha\!s.\sigma}_{M'} , 1517 S(X\!s))(\den{\alpha\!s,.p}_{M'})(i_{X\!s}) = 1. 1518\] 1519Thus $M'$ satisfies the sequent 1520\[ 1521(\gamma\ ,\ \equant{f_{(\alpha\!s)\ty{op}\fun\sigma}}\TyDef\ p\ f). 1522\] 1523But since the sequent $(\gamma,(\equant{f_{\alpha\fun\sigma}}{\sf 1524Type\_Definition}\ p\ f)\ \imp\ q )$ is in ${\sf Theorems}_{\cal T}$, 1525it is satisfied by the model $M$ and hence also by the model $M'$ 1526(since the sequent does not involve the new type constant $\ty{op}$). 1527Instantiating $\alpha$ to $(\alpha\!s)\ty{op}$ in this sequent (which 1528is permissible since by Condition~(iv) $\alpha$ does not occur in 1529$\gamma$), one thus has that $M'$ satisfies the sequent 1530\[ 1531(\gamma\ ,\ 1532(\equant{f_{(\alpha\!s)\ty{op}\fun\sigma}}\TyDef\ p\ f)\imp 1533q[(\alpha\!s)\ty{op}/\alpha]). 1534\] 1535Applying Modus Ponens, one concludes that $M'$ satisfies 1536$(\gamma\ ,\ q[(\alpha\!s)\ty{op}/\alpha])$ and 1537therefore $M'$ is a model of ${\cal T}'$, as required. 1538 1539\medskip 1540 1541An extension by type definition is in fact a special case of extension 1542by type specification. To see this, suppose 1543$\langle (\alpha_1,\ldots,\alpha_n)\ty{op},\ \sigma,\ 1544p_{\sigma\fun\ty{bool}}\rangle$ is a type definition for a theory 1545$\cal T$. Choosing a type variable $\alpha$ different from 1546$\alpha_1,\ldots,\alpha_n$, let $q$ denote the formula 1547\[ 1548\equant{f_{\alpha\fun\sigma}}{\sf Type\_Definition}\ p\ f 1549\] 1550Then $\langle 1551(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\emptyset,q\rangle$ 1552satisfies all the conditions necessary to be a type specification for 1553$\cal T$. Since $q[(\alpha_1,\ldots,\alpha_n)\ty{op}/\alpha]$ is just 1554$\equant{f_{(\alpha_1,\ldots,\alpha_n)\ty{op}\fun\sigma}}{\sf 1555Type\_Definition}\ p\ f$, one has that 1556\[ 1557{\cal T}{+_{tydef}} 1558\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p\rangle 1559={\cal T}{+_{\it tyspec}} 1560\langle(\alpha_1,\ldots,\alpha_n)\ty{op},\sigma,p,\alpha,\emptyset,q\rangle 1561\] 1562Thus the Proposition in Section~\ref{tydefs} is a special case of the 1563above Proposition. 1564 1565In an extension by type specification, the property $q$ which is 1566asserted of the newly introduced type constant need not determine the 1567type constant uniquely (even up to bijection). Correspondingly there 1568may be many different standard models of the extended theory whose 1569restriction to $\cal T$ is a given model $M$. By contrast, a type 1570definition determines the new type constant uniquely up to bijection, 1571and any two models of the extended theory which restrict to the same 1572model of the original theory will be isomorphic. 1573\index{extension, of HOL logic@extension, of \HOL{} logic!by type specification|)} 1574 1575 1576 1577%%% Local Variables: 1578%%% mode: latex 1579%%% TeX-master: "logic" 1580%%% End: 1581