Manual/Logic/semantics.tex

1 % Revised version of Part II, Chapter 10 of HOL DESCRIPTION
11 The result, if any, of a session with the \HOL{} system is an object
13 logician would call a theory\index{theories, in HOL logic@theories, in \HOL{} logic!abstract form of}, but there are some differences arising
14 from the needs of mechanical proof.  A \HOL{} theory, like a logician's
16 addition, however, a \HOL{} theory, at any point in time, contains an
23 between logicians' theories and \HOL{} theories is that for logicians,
24 theories are static objects, but in \HOL{} they can be thought of as
25 potentially extendable. For example, the \HOL{} system provides tools
27 with \HOL{} consists in combining some existing theories, making some
30 The purpose of the \HOL{} system is to provide tools to enable
31 well-formed theories to be constructed.  The \HOL{} logic is typed:
35 of the definitions and axioms of the theory.  The \HOL{} system ensures
39 of the proof system of \HOL, to be given below. It is shown to be {\em
40 sound\/} for the set theoretic semantics of \HOL{} described in the
48 This chapter also describes the various mechanisms by which \HOL\
51 up from the initial \HOL{} theory (which does possess a model) using
58 The \HOL{} logic is phrased in terms of hypothetical assertions called
152 \index{inference rules, of HOL logic@inference rules, of \HOL{} logic!abstract form of primitive}
171 \subsection{The \HOL{} deductive system}
174 The deductive system of the \HOL{} logic is specified by eight rules
177 brackets are the names of the \ML\ functions in the \HOL{} system that
185 ASSUME}]}\index{assumption introduction, in HOL logic@assumption introduction, in \HOL{} logic!abstract form of}
191 REFL}]}\index{REFL@\ml{REFL}}\index{reflexivity, in HOL logic@reflexivity, in \HOL{} logic!abstract form of}
197 \index{beta-conversion, in HOL logic@beta-conversion, in \HOL{} logic!abstract form of}\index{BETA_CONV@\ml{BETA\_CONV}}
209 SUBST}]}\index{SUBST@\ml{SUBST}} \index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!abstract form of}
225 \index{ABS@\ml{ABS}}\index{abstraction rule, in HOL logic@abstraction rule, in \HOL{} logic!abstract form of}
235 \index{type instantiation, in HOL logic@type instantiation, in \HOL{} logic!abstract form of}
253 DISCH}]}\index{discharging assumptions, in HOL logic@discharging assumptions, in \HOL{} logic!abstract form of}\index{DISCH@\ml{DISCH}}
264 MP}]}\index{MP@\ml{MP}}\index{Modus Ponens, in HOL logic@Modus Ponens, in \HOL{} logic!abstract form of}
279 The particular set of rules and axioms chosen to axiomatize the \HOL\
283 \PPL\index{PPlambda (same as PPLAMBDA), of LCF system@\ml{PP}$\lambda$ (same as \ml{PPLAMBDA}), of \ml{LCF} system}, since \HOL{} was
285 substitution\index{substitution rule, in HOL logic@substitution rule, in \HOL{} logic!implementation of} rule {\small\tt SUBST} is exactly
295 \index{soundness!of HOL deductive system@of \HOL{} deductive system}
298 \index{inference rules, of HOL logic@inference rules, of \HOL{} logic!formal semantics of}
299 \emph{The rules of the \HOL{} deductive system are {\em sound} for
322 \section{\HOL{} Theories}
325 A \HOL{} {\it theory\/}\index{theories, in HOL logic@theories, in \HOL{} logic!abstract form of} ${\cal T}$ is a $4$-tuple:
333 \item ${\sf Struc}_{\cal T}$ is a type structure\index{type structures, of HOL theories@type structures, of \HOL{} theories}  called the type
336 \item ${\sf Sig}_{\cal T}$ is a signature\index{signatures, of HOL logic@signatures, of \HOL{} logic!of HOL theories@of \HOL{} theories}
340 called the  axioms\index{axioms, in a HOL theory@axioms, in a \HOL{} theory}
346 \index{theorems, in HOL logic@theorems, in \HOL{} logic!abstract form of}
350 the \HOL{} deductive system.
372 The {\it minimal theory\/}\index{MIN@\ml{MIN}}\index{minimal theory, of HOL logic@minimal theory, of \HOL{} logic} \theory{MIN} is defined by:
386 syntax, by exploiting the higher order constructs of \HOL{} one can
405 \index{truth values, in HOL logic@truth values, in \HOL{} logic!abstract form of}
409 \index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!abstract form of}
413 \index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abstract form of}
421 \index{negation, in HOL logic@negation, in \HOL{} logic!abstract form of}
425 \index{conjunction, in HOL logic@conjunction, in \HOL{} logic!abstract form of}
429 \index{disjunction, in HOL logic@disjunction, in \HOL{} logic!abstract form of}
433 \index{one-to-one predicate, in HOL logic@one-to-one predicate, in \HOL{} logic!abstract form of}
437 \index{onto predicate, in HOL logic@onto predicate, in \HOL{} logic!abstract form of}
444 \index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abbreviation for multiple}
445 \index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!abbreviation for multiple}
513 \index{axioms!formal semantics of HOL logic's@formal semantics of \HOL{} logic's|(}
518 \item \index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!formal semantics of}
525 \index{universal quantifier, in HOL logic@universal quantifier, in \HOL{} logic!formal semantics of}
527 \item \index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!formal semantics of}
544                     \right. \]\index{negation, in HOL logic@negation, in \HOL{} logic!formal semantics of}
552                            \right. \]\index{conjunction, in HOL logic@conjunction, in \HOL{} logic!formal semantics of}
560                         \right. \]\index{disjunction, in HOL logic@disjunction, in \HOL{} logic!formal semantics of}
570                             \right. \]\index{one-to-one predicate, in HOL logic@one-to-one predicate, in \HOL{} logic!formal semantics of}
579                            \right. \]\index{onto predicate, in HOL logic@onto predicate, in \HOL{} logic!formal semantics of}
594 \index{axioms!formal semantics of HOL logic's@formal semantics of \HOL{} logic's|)}
605 obtained by adding the following four axioms\index{axioms!abstract form of HOL logic's@abstract form of \HOL{} logic's} to the theory
638   of HOL logic@initial theory, of \HOL{} logic!abstract form of} of the
639 \HOL{} logic. A theory which extends \theory{INIT} will be called a
656 derived from the theory's axioms using the \HOL{} logic, or
672 `true'), but which are not provable in the \HOL{} logic.
679 \index{extension, of HOL logic@extension, of \HOL{} logic!abstract form of}
711 There are two main mechanisms for making extensions of theories in \HOL:
718 not implemented in the \HOL{}4 system.}
748 introduce inconsistent axiomatizations, users of the \HOL{} system are
757 \index{extension, of HOL logic@extension, of \HOL{} logic!by constant definition|(}
777 Sig}_{\cal T}$, then the {\em definitional extension\/}\index{constant definition extension, of HOL logic@constant definition extension, of \HOL{} logic!abstract form of} of ${\cal T}$
799    {+_{\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} \ =\
801    {+_{\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 =
803    {+_{\it def}}\langle {\exists}\index{existential quantifier, in HOL logic@existential quantifier, in \HOL{} logic!abstract form of}\ =\
807    {+_{\it def}}\langle \neg\ =\ \lquant{b}\ b \imp \F \rangle\index{negation, in HOL logic@negation, in \HOL{} logic!abstract form of}\\
808    {+_{\it def}}\langle {\wedge}\index{conjunction, in HOL logic@conjunction, in \HOL{} logic!abstract form of}\ =\ \lquant{b_1\ b_2}\uquant{b}
810    {+_{\it def}}\langle {\vee}\index{disjunction, in HOL logic@disjunction, in \HOL{} logic!abstract form of}\ =\ \lquant{b_1\ b_2}\uquant{b}
813      \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}\\
814    {+_{\it def}}\langle\Onto \  =\ \lquant{f_{\alpha\fun\beta}}\index{onto predicate, in HOL logic@onto predicate, in \HOL{} logic!abstract form of}
861 \index{extension, of HOL logic@extension, of \HOL{} logic!by constant definition|)}
864 \index{extension, of HOL logic@extension, of \HOL{} logic!by constant specification|(}
867 Constant specifications\index{constant specification extension, of HOL logic@constant specification extension, of \HOL{} logic!abstract form
876 consistent\index{consistency, of HOL logic@consistency, of \HOL{} logic!under constant specification}, they can only be made if it has
971 Soundness Theorem \ref{soundness}\index{consistency, of HOL logic@consistency, of \HOL{} logic!under constant specification} this
1058 \index{extension, of HOL logic@extension, of \HOL{} logic!by constant specification|)}
1060 \subsection{Remarks about constants in \HOL{}}
1071 introducing constants, but rather the syntax of \HOL{} which does not
1083 In the current version of \HOL, constants are (name,type)-pairs.
1084 One can envision a slight extension of the \HOL{} syntax with
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|(}
1138 ones. Such types are defined\index{extension, of HOL logic@extension, of \HOL{} logic!by type definition} in \HOL{} by introducing a new type
1159 Types in \HOL{} must denote non-empty sets.  Thus it is only
1160 consistent\index{consistency, of HOL logic@consistency, of \HOL{} logic!under type definition} to define a new type isomorphic to a
1197 variables. Such dependent types are not (yet!) a part of the \HOL{} system.}
1224 type definition\/}\index{type definitions, in HOL logic@type definitions, in \HOL{} logic!abstract structure of} for a theory ${\cal
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|)}
1287 \index{extension, of HOL logic@extension, of \HOL{} logic!by type specification|(}
1306 can be expressed in \HOL.) The mechanism described in this section
1325 the \HOL{} logic and one must proceed indirectly---replacing the
1327 \HOL{} syntax. The formula used is
1573 \index{extension, of HOL logic@extension, of \HOL{} logic!by type specification|)}