Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <02292-0@swan.cl.cam.ac.uk>; Wed, 29 Jan 1992 00:17:47 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19159; Tue, 28 Jan 92 12:42:18 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from electra.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA19154; Tue, 28 Jan 92 12:41:13 -0800 Date: Tue, 28 Jan 92 15:38:30 EST From: garrel@com.oracorp.electra Received: by electra.oracorp.com (4.1/1.3-ORA Corporation) id AA14237; Tue, 28 Jan 92 15:38:30 EST Message-Id: <9201282038.AA14237@electra.oracorp.com> To: info-hol@edu.uidaho.cs.ted, andrews@edu.cmu.cs, rc@edu.cornell.cs, bret@com.oracorp, hook@edu.ogi.cse, anil@edu.cornell.msi.mssun7, richard@com.oracorp, shb@com.oracorp, griffin@com.att.research Subject: Report on HOL completeness theorem Completeness for the HOL Logic Preliminary report January 28, 1992 Garrel Pottinger garrel@oracorp.com 1. Introduction This document provides a brief account of the completeness result for the HOL logic announced in my message to info-hol dated November 20, 1991. The definition of models is given in full, but most proofs and many technical details are omitted. The document is structured as follows. Section 2 discusses the central problem involved in establishing completeness for systems of second-order and higher-order logic, describes Henkin's method for solving this problem, and explains why the models described in [HOL, Part II] are not suited to applying Henkin's techniques. Section 3 describes the models used in extending Henkin's techniques to cover the HOL logic, and section 4 introduces the notions of implication and derivability used in stating the completeness theorem. Section 5 states the model existence theorem, and section 6 contains its corollaries: the completeness, compactness, and Lowenheim-Skolem theorems. Section 7 uses the preceding results to clarify the relations between the HOL logic and Andrews's system Q_0 [And86, chapter 5], and section 8 discusses the definition mechanisms included in the HOL system in the light of what has been done in sections 3--6. Section 9 comments on how the work reported here bears on the project of adding new quantifiers, including type quantifiers, to the HOL logic. 2. Background Intuitively, we think of the n-ary predicate variables of second-order logic as ranging over the nth cartesian power of the set of individuals (or, equivalently, as ranging over the set of n-ary functions from individuals to truth values). As Henkin points out [Hen50, p. 81], if we define the notion of a second-order model in accordance with this intuition, the set of valid second-order formulas cannot be recursively enumerated. This is proved as follows. The Peano axioms can be expressed as a second-order formula A, and it can be shown that, for the class of models so defined, all models of A are isomorphic. Hence, where B is an arbitrary arithmetic formula, A => B or A => ~B is valid in the class of models in question, according as B is true or false of the natural numbers. So a recursive enumeration of the valid second-order formulas would yield a recursive decision procedure for arithmetic, which cannot exist due to the recursive unsolvability of the halting problem. Evidently, this argument also applies to higher-order logic, if we define higher-order models so that sigma->tau denotes the full space of functions from the type denoted by sigma to the type denoted by tau. Henkin modified the intuitive notion of second-order and higher-order models by allowing the range of n-ary predicate variables to be a non-empty subset of the nth cartesian power of the set of individuals and, in the higher-order case, allowing sigma->tau to denote a non-empty subset of the full space of functions from the type denoted by sigma to the type denoted by tau. More exactly, he called structures of the kind described in the preceding sentence frames and counted as models frames in which each formula and term could be assigned a denotation. Henkin called the models so defined general models. Evidently, every model of the kind described in the first paragraph of this section is a general model, but the definition of general models does not rule out the existence of models other than these. I will call the models described at the beginning of this section full models and will call such other models as may exist sparse models. (Henkin used the terms "standard" and "non-standard", instead of "full" and "sparse", to distinguish these two classes of general models. I use "full" and "sparse" to mark the distinction in order to avoid conflicts with the usage of "standard" and "non-standard" current in discussions of non-standard analysis.) Since a second-order term purporting to denote an n-ary relation can contain bound variables ranging over all such relations and a higher-order term can contain bound variables ranging over arbitrary types, the definition of general models is highly impredicative. Consequently, it is not clear from the definition whether any sparse models exist. Henkin proved that, in fact, there are sparse models. Indeed, he showed that there are enough of them to yield a strong completeness theorem for second-order and higher-order logic --- not only are the formulas valid in the class of general models theorems according to the usual axioms and rules of second-order and higher-order logic, but, in a given theory, every formula implied by a specified set of hypotheses is derivable from that set of hypotheses. Henkin established this by showing that every consistent set of (closed) formulas has a model. Combining the strong completeness theorem with soundness enabled him to prove the compactness theorem for second-order and higher-order logic, and the model existence theorem used as a lemma in the proof of the completeness result also yielded the Lowenheim-Skolem theorem as a corollary. The version of higher-order logic considered by Henkin does not contain type variables, and the same thing is true of Andrews' system Q_0, which is a refinement of the system Henkin worked with. Consequently, in their original form, Henkin's results do not cover the HOL logic. (The system Q of [And65] contains type variables and allows such variables to be bound. But Q contains transfinite types, which lead to a theorem of infinity, making it possible to develop arithmetic inside the system. Consequently, no completeness result for Q is possible, in view of the the first incompleteness theorem.) The models for the HOL logic described in [HOL, chapter 10] are adequate for proving the consistency of the theory INIT [HOL, p. 102] and extensions of INIT produced via the definition mechanisms of the HOL system [HOL, section 9.6], which is their intended purpose. But they do not furnish a good basis for generalizing Henkin's techniques to cover the HOL logic, for the following reasons: * Even if INFINITY_AX is dropped from INIT and Infty is deleted from the conditions defining universes [HOL, p. 107], having Prod and Pow as separate conditions on universes, as opposed to a single closure condition involving function spaces, complicates the problem of defining a suitable notion of general model. * The condition Sub, introduced in order to show that extending INIT by means of type definitions leads to consistent theories, is incompatible with the methods Henkin used to prove the existence of sparse models. It can be shown (and will be, in section 8) that the theory obtained by adding: exists x_alpha . exists y_alpha. ~ x_alpha = y_alpha to INIT as an axiom is consistent, but, clearly, the resulting theory cannot have a model for which Sub holds, since the new axiom rules out the existence of one element types. Consequently, if a suitable model existence theorem is to be proved, Sub must be deleted from the conditions defining models. * Dropping Sub makes Choice an idle wheel, since, without Sub, it is not be possible to define the semantics of epsilon in the manner of [HOL, p. 110]. Since Inhab is the only condition used in defining universes that is not touched by the preceding remarks, it is better to approach the problem of defining general models for HOL by starting directly from the kind of models considered by Henkin, instead of trying to work from the definitions of [HOL, chapter 10]. The next section shows how to go about this. 3. Models >From now on, I will drop the word "general" and speak simply of models. Following [And86, chapter 5], I will define models by first defining frames, then defining interpretations, and finally taking models to be those interpretations in which a denotation can be defined for every term. Also, I will omit => from the list of primitive constants and work with a definite description operator iota instead of the choice constant epsilon. It will be shown later that => can be defined by means of the primitives I have chosen, and, of course, there is no obstacle to postulating that iota happens to behave like a choice constant, if this is desirable in an application. The definitions proceed relative to a morphology Mor = (Omega, Sigma), where Omega specifies type operators and their arities, and, given Omega, Sigma specifies type schemes for constants and variables. The type scheme assigned to a constant c by Sigma may be an arbitrary type symbol over Omega, but Sigma must assign a type variable as the type scheme of a variable x. Note that there is a difference between the terminology I am using and the terminology of [HOL, sections 9.1 and 9.2]. The syntactic objects called variable names there will be called variables here, and the objects called constant names there will be called constants here. Both constants and variables will be called atoms. In the terminology used here, constants and variables are not terms. On the other hand, c_sigma will be called a constant term and x_alpha will be called a variable term in what follows, and, of course, such syntactic objects are terms. Reasons for preferring the present terminology will be given later in this section and in section 9. Since concrete syntax has no importance for the present discussion, I will also depart from the notation of [HOL, section 9.1] by using omega, omega_1, ... to denote type operators and denoting the application of an n_ary type operator omega to type symbols sigma_1, ..., sigma_n by omega simga_1 ... sigma_n. Where Mor = (Omega, Sigma), a Mor-frame is a pair Fr = (U, F) such that (1) U, the universe, is a set of non-empty sets, (2) domain F = domain Omega, (3) if Omega omega = 0, then F omega is in U, (4) if Omega omega = n >= 1, then F omega is an n-ary operation on U, (5) F bool is the set containing the two truth values, and (6) for u, v in U, (F ->)(u, v) is a subset of the space of functions from u to v. If w is a set of type variables, the w-valuations over a frame Fr = (U, F), a.k.a. type valuations of w over Fr, are those functions the domains of which include w and are included in the set of type variables and the ranges of which are included in U. Given Fr, a w-valuation V over Fr, and a type symbol sigma, the obvious recursion on the complexity of sigma defines the type denoted by sigma in Fr under V. If sigma contains no type variables, the denotation of sigma is, of course, independent of V, and we may simply speak of the type denoted by sigma in Fr. Note that in the terminology of [HOL, Part II] sigma itself is called a type, but in the terminology used here sigma is called a type symbol and the semantic object denoted by sigma, given a frame and a type valuation, is called a type. A Mor-interpretation is a pair In = (Fr, I) such that Fr is a Mor-frame and I is a function that assigns meanings to constants in the manner that will now be explained. The explanation has three parts. The first introduces a novel way of looking at the syntax of the HOL logic. The second uses the notions introduced in the first part of the explanation to define a relation between type valuations of the type variables of the type symbol sigma of a constant term c_sigma and the type scheme Sigma c of the constant c. Relying on the concepts introduced in the second part of the explanation, the third part states the conditions that the function I must satisfy. A primitive type substitution over Mor is a function s that maps type variables to Mor type symbols. Given such an s, let s+ be the recursive extension of s to the set of Mor type symbols given by: (1) s+ alpha = if alpha is in domain s then s alpha, else alpha, and (2) s+ omega sigma_0 ... sigma_n-1 = omega (s+ sigma_0) ... (s+ sigma_n-1) (n >= 0). For each constant term c_sigma over the morphology Mor = (Omega, Sigma), there is a unique primitive type substitution s such that domain s is the set of type variables occurring in Sigma c and s+(Sigma c) = sigma. Conversely, for each Mor-constant c and each primitive type substitution s such that domain s is the set of type variables occurring in Sigma c, c_s+(Sigma c) is a constant term over Mor. Hence, for logical purposes, we may identify the constant terms over Mor with pairs (c, s) such that c is a Mor-constant and s is a primitive type substitution that has the set of type variables occurring in Sigma c as its domain. This will be done in what follows, and the notation "c_sigma" will be taken as a description of such pairs. (NB: I am NOT suggesting any change in the implementation of the HOL system.) Now consider a Mor-constant term c_sigma = (c, s), a Mor-frame Fr, and a type valuation V_1 over Fr such that, for every type variable alpha in the domain of s, V_1 assigns types to every type variable occurring in s alpha. Let V, the type valuation over Fr induced by c, s, and V_1, be the type valuation over Fr that has the same domain as s and, for every alpha in domain s, assigns to alpha the type denoted by s alpha in Fr under V_1. A valuation V is an induced type valuation for c and s over Fr if, and only if, for some V_1, V is the type valuation over Fr induced by c, s, and V_1. In order for In = (Fr, I) to be a Mor-interpretation, the function I must satisfy the following conditions: (1) For each Mor-constant c, each primitive type substitution s that has the set of type variables occurring in Sigma c as its domain, and each V that is an induced type valuation for c and s over Fr, I c s V is a member of type denoted by Sigma c in Fr under V. (2) Where Sigma = is alpha->alpha->bool, domain s is {alpha}, and V is an induced type valuation for = and s over Fr, I = s V is the the function f such that, for u, v in V alpha, f u v is truth if u is the same object as v, and f u v is falsehood if u and v are distinct. (3) Where Sigma iota is (alpha->bool)->alpha, domain s is {alpha}, and V is an induced type valuation for iota and s over Fr, I iota s V is a function f such that, for g in the type denoted by alpha->bool in Fr under V, if there is a u in domain g such that {v in domain g | g v is truth} = {u}, then f g = u. This completes the definition of interpretations. Note that the function I assigns a definite semantic object I c as the meaning of the Mor-constant c. Thus, c itself has a meaning, rather than being an uninterpreted piece of syntax (a mere name) from which semantically significant syntactic objects are generated. This motivates the terminology use here, according to which c is called a constant and the various c_sigma's are called constant terms. With the definition of interpretations in hand, the next step in defining models is to extend the assignments of types to type variables provided by type valuations to assignments that also assign appropriate values to variables. Such extended assignments will be called, simply, valuations. As in the case of constant terms, a variable term x_sigma will be identified with the pair (x, s) such that domain s is the set of type variables occurring in Sigma x and s+(Sigma x) = sigma. And, given this, the notion of an induced type valuation extends automatically to cover variables. The valuations over the Mor-interpretation In = (Fr, I) are the functions V such that: (1) For some set w of type variables, V includes a w-valuation over Fr. (2) For each variable x, each primitive type substitution s that has the set of type variables occurring in Sigma x as its domain, and each V_1 that is an induced type valuation for x and s over Fr, V x s V_1 is a member of the type denoted by Sigma x in Fr under V_1. Note that each valuation V assigns a definite meaning V x to x. This motivates calling x a variable and calling the various x_sigma's variable terms. (Cf. terminological remarks about constants and constant terms following the definition of interpretations.) This point will be taken up again in section 9. The Mor-interpretation In = (Fr, I) is a Mor-model if, for every Mor-term X and every valuation V over In such that the type variables occurring in X are assigned types by the type valuation V_Ty included in V, the denotation function D specified by the following conditions has as its value a member of the type denoted by the type symbol of X in Fr under V_Ty: (1) If X is (a, s), where a is an atom, let f be if a is a constant then I, else V. Also, let V_Ty' be the type valuation over Fr induced by a, s, and V_Ty. Then D X V is f a s V_Ty'. (2) If X is YZ, then D X V is (D Y V)(D Z V). (3) If X is lambda (x, s) . Y, let f be the function defined for v in the type denoted by s(Sigma x) in Fr under V_Ty by taking f v to be D Y V', where, for the type valuation V_Ty' over Fr induced by x, s, and V_Ty, V x s V_Ty' is v, and, otherwise, V' is like V. Then D X V is f. 4. Implication and Derivability >From now on, A, B, C, ... are to be terms of type bool, and such terms will be called formulas. Also, Gamma, Delta, Theta, Xi, Gamma_1, ... are to be sets of formulas. Sequents have the form Gamma >> A. As in section 3, the definitions that follow proceed relative to a morphology, but, here and hereafter, I will omit references to the background morphology, wherever this cannot cause confusion. As usual, I will say that a valuation V satisfies the formula A in the model M if, and only if, where D_M is the denotation function for M, D_M A V is truth. Also, V satisfies the set of formulas Gamma in the model M if, and only if, V satisfies every member of Gamma in M. The model M is a model of A if, and only if, every M-valuation that assigns values to the type variables of A satisfies A, and M is a model of the set of formulas Gamma if, and only if, M is a model of every member of Gamma. The set of formulas Gamma implies the formula A relative to the set of formulas Theta if, and only if, for every M that is a model of Theta and every M-valuation V that assigns values to all type variables of A and all type variables of members of Gamma, either V fails to satisfy a member of Gamma or V satisfies A. In the preceding definition, the formulas in Theta are treated as axioms, and, consequently, the type variables and variables occurring free in them are treated as if they were universally quantified. On the other hand, the formulas in Gamma are treated as assumptions, and, hence, the definition refers to the behavior of the members of Gamma and the formula A under the various valuations that assign values to the type variables and variables occurring free in them. The general notion of implication is specialized to the case where axioms are absent by saying say that Gamma implies A if, and only if, Gamma implies A relative to the empty set of formulas. The corresponding specialized notion for the case where assumptions are absent is consequence --- A is a consequence of Theta if, and only if, the empty set of formulas implies A relative to Theta. I will write Gamma;Theta |= A to indicate that Gamma implies A relative to Theta, and, suppressing notations for the empty set, Gamma; |= A will mean that Gamma implies A, and ;Theta |= A will mean that A is A consequence of Gamma. The next order of business is to explain how various familiar logical operators, including the conditional =>, will be represented in terms of the primitives I have chosen. I will use the following abbreviations (that is, each case, the notation to the left of "=DF" is being introduced as a metalinguistic shorthand for the notation on the right, without affecting the object language): (1) =_ =DF =_sigma->sigma->bool (2) <=> =DF =_ (3) iota_ =DF iota_(sigma->bool)->sigma (4) T =DF <=> =_bool->bool> <=> (5) All_(sigma->bool)->bool =DF =_bool> lambda x_sigma . T (6) All x_sigma . A =DF All_(sigma->bool)->bool lambda x_sigma . A (7) F =DF All x_bool . x_bool (8) ~ =DF lambda x_bool . x_bool <=> F (9) Exists x_sigma . A =DF ~All x_sigma . ~A (10) P =DF lambda x_bool . lambda y_bool . lambda z_bool->bool->bool . z_bool->bool->bool x_bool y_bool (11) => =DF lambda x_bool. lambda y_bool . ~(P x_bool y_bool =_<(bool->bool->bool)->bool> P T F) (12) Or =DF lambda x_bool . lambda y_bool . ~x_bool => y_bool The content of abbreviations (1)--(9) and (12) is straightforward, but (10) and (11) require comment. In the type-free lambda calculus, pairing can be represented by the term lambda x . lambda y . lambda z . z x y, and the corresponding first and second projections can be represented by lambda x . lambda y . x and lambda x . lambda y . y [Bar84, p. 133]. Although this way of representing pairs will not work generally in the context of the HOL typing discipline, it will work if the variables x and y can be decorated with the same type symbol. Thus, the term P represents pairing of boolean values, with the term lambda x_bool . lambda y_bool . x_bool representing the first projection and the term lambda x_bool . lambda y_bool . y_bool representing the second projection. Hence, asserting A => B amounts to denying that A is true and B is false, and the term => is a way of representing the conditional. Abbreviations (1)--(12) provide a way of construing the rules DISCH and MP of [HOL, p. 99] and the axioms BOOL_CASES_AX, IMP_ANTISYM_AX, and ETA_AX of [HOL, p. 102] within the framework of primitives used in this document. As was remarked above, I have chosen to work with the description operator iota, instead a choice constant. A suitable axiom for iota is: IOTA_AX >> All x_alpha . iota_ (=_ x_alpha) =_ x_alpha which says that the object equal to x_alpha is x_alpha (Cf. [And86, p. 164, axiom 5]). Combining the rules and axioms of the preceding paragraph with the rules ASSUME, REFL, BETA_CONV, SUBST, ABS, and INST_TYPE of [HOL, pp. 98--99] furnishes basis for defining the notion of derivability to which the completeness theorem applies, as follows. Let Rules be the set of instances of DISCH, MP, ASSUME, REFL, BETA_CONV, SUBST, ABS, and INST_TYPE, and let Ax be the set containing BOOL_CASES_AX, IMP_ANTISYM_AX, ETA_AX, and IOTA_AX. The formula A is derivable from the set of formulas Gamma relative to the set of formulas Theta if, and only if, for some finite subset Gamma_1 of Gamma, the sequent Gamma_1 >> A follows from {>> B | B in Ax or B in Theta} by RULES, in the sense of "follows from" defined for sets of sequents and deductive systems by [HOL, p. 97]. As in the case of implication, the definition of derivability just given treats the members of Theta as axioms and treats the members of Gamma as assumptions. The general notion of derivability is specialized to the case where axioms are absent by saying that A is derivable from Gamma if, and only if, A is derivable from Gamma relative to the empty set of formulas. Theoremhood is the special case where assumptions are absent --- A is a theorem relative to Theta if, and only if, A is derivable from the empty set of formulas relative to Theta. In what follows, Gamma;Theta |- A means that A is derivable from Gamma relative to Theta, Gamma; |- A means that A is derivable from Gamma, and ;Theta |- A means that A is a theorem relative to Theta. 5. The Model Existence Theorem As usual, a straightforward induction on length of derivations proves soundness. That is, such an argument proves that if Gamma;Theta |- A, then Gamma;Theta |= A. Following [Hen 50], the proof of completeness --- i.e., the proof that if Gamma;Theta |= A, then Gamma;Theta |- A --- is obtained as a corollary of a theorem to the effect that every consistent theory has a model. In order to state this model existence result exactly, the following definitions are required. Consider a morphology Mor. A set of formulas Theta is a Mor-theory if, and only if, Theta is a set of Mor-formulas and, for every Mor-formula A, if ;Theta |- A, then A is a member of Theta. The members of a Mor-theory Theta are the theorems of Theta, and a Mor-theory Theta is consistent if, and only if, F is not a member of Theta. Theorem 5.1 [Model existence theorem] If Theta is a consistent Mor-theory, then there is a Mor-model M = (Fr, I) such that, where Fr = (U, F): (1) Every member of U is denoted in Fr by a Mor-type symbol that does not contain type variables. (2) For all u in U, if u is denoted in Fr by the Mor-type symbol sigma and sigma does not contain type variables, then the cardinality of u is less than or equal to the cardinality of the set of Mor-terms that have sigma as their type symbol. (3) M is a model of Theta. 6. Completeness and other Corollaries The model existence theorem, together with some supporting lemmas not stated in this document, yields: Theorem 6.1 [Completeness theorem] If Gamma;Theta |= A, then Gamma;Theta |- A. So, in view of this and the soundness theorem, we have: Corollary 6.2 Gamma;Theta |= A if, and only if, Gamma;Theta |- A. Part (a) of the following theorem is a consequence of corollary 6.2 and the finitiess of derivations, and part (b) follows from part (a) and the model existence theorem: Corollary 6.3 [Compactness theorem] (a) Gamma;Theta |= A if, and only if, for some finite subset Gamma_1 of Gamma and some finite subset Theta_1 of Theta, Gamma_1;Theta_1 |= A. (b) If every finite subset of the set of formulas Theta has a model, then Theta has a model. And the soundness and model existence theorems yield: Theorem 6.3 [Lowenheim-Skolem theorem] If the set Theta of Mor-formulas has a model, then Theta has a model M = (Fr, I) such that, where Fr = (U, F), (1) every member of U is denoted in Fr by a Mor-type symbol that does not contain type variables, and (2) for all u in U, if u is denoted in Fr by the Mor-type symbol sigma and sigma does not contain type variables, then the cardinality of u is less than or equal to the cardinality of the set of Mor-terms that have sigma as their type symbol. 7. The HOL Logic and Andrews' System Q_0 The following remarks show that the version of the HOL logic considered here is a conservative extension of Andrews' system Q_0. The formulas of Q_0 can be regarded as monomorphic formulas of the HOL logic involving only type symbols built up from bool, ind, and ->. Also, it is not difficult to see that, given a model M of the kind defined in [And86, section 54], one can define a model M' of the kind considered in this document such that the set of Q_0 formulas that hold in M the same as the set of Q_0 formulas that hold in M', and conversely. Consequently, corollary 6.2 and the corresponding result for Q_0 imply that, where Theta is a set of Q_0 formulas, A is a Q_0 formula, and Theta' is the set of universal closures of members of theta, A is provable from Theta' in the sense of [And86, p. 165] if, and only if, ;Theta |= A. 8. Definitions in HOL According to the usual logical theory of definition (see, for example, [Kle50, section 74], [Sup57, chapter 8], and [Sho76, section 4.6]), defined symbols must be eliminable and the axioms introducing them must not lead to proofs of new theorems stated in the language available prior to the definition. Of the "definition" mechanisms included in the HOL system, only constant definitions [HOL, section 9.6.1] satisfy these requirements. Extensions by constant specifications [HOL, section 9.6.5] are conservative, but, in general, the new symbols are not eliminable, and extensions by type definitions [HOL, section 9.6.6] may violate both requirements. These claims are established as follows. Given an extension by a constant definition and a formula A of the extension, successive applications of SUBST to the defining axiom for the new constant and the tautology A <=> A will produce a proof of A <=> A'in the extension, for some formula A' of the unextended language. This shows that eliminability holds for extensions by constant definitions. Furthermore, every model of the unextended theory can be expanded to a model of an extension by a constant definition, since an interpretation that covers the new constant and validates the defining axiom for the new constant can be read off from the term on the right side of the defining axiom. It follows from this and the soundness theorem that if A is a forumula of the unextended language and A is a theorem of the extension, then A holds in every model of the unextended theory. Applying the completeness theorem, it follows that A is a theorem of the unextended theory. Thus, extensions by constant definitions are conservative. Mutatis mutandis, the conservation argument of the preceding paragraph applies to extensions by constant specifications. But the argument for eliminability given two paragraphs above fails for extensions by constant specifications, and, as the following example shows, there is no hope of repairing it. Let LOG be the minimal theory relative to the minimal morphology, and not that LOG certainly has models. A constant specification allows us extend LOG by introducing new constants b and c with bool as their type scheme and ~(b_bool <=> c_bool) as the new axiom specifying their behavior (Cf. [HOL, p. 102] ). But there is no formula A' of the unextended language such that b_bool <=> A' can be proved in the extension. For, given a candidate formula A', a model M of LOG, and, if A' has free type variables or free variables, a valuation V , we can produce a model M' of the extension in which ~(b_bool <=> c_bool) holds, but b_bool <=> A' does not, by interpreting c so that the denotation of c_bool in M' is the denotation of A' in M under V and interpreting b so that the denotation of b_bool in M' is the remaining truth value. It follows via the soundness theorem that b <=> A' is not a theorem of the extension, and, since A was arbitrary, it follows that eliminability fails for constant specifications. A variant of the argument given in the preceding paragraph shows that type operators introduced in extensions by type definitions are not eliminabile, as follows. A type definition allows us to extend LOG by introducing a type symbol bool' and an axiom postulating that the type denoted by bool' has the same number of elements as the type denoted by bool. But the soundness theorem implies that there is no formula A' of the unextended language such that x_bool' =_ y_bool' <=> A' can be proved in the extension. To see this note that the extension clearly has models, and, given a model M, we can easily produce a valuation V under which x_bool' =_ y_bool' and A' denote different truth values by starting with an arbitrary valuation V_1 that assigns types to the type variables of A' and then altering V_1, if necessary, to make x_bool' =_ y_bool' denote the truth value not denoted by A'. It remains to show that extensions by type definitions may not be conservative. To see this, note first that the theory LOG' produced by adding exists x_alpha . exists y_alpha. ~ x_alpha = y_alpha to LOG as an axiom has models --- any model in which the type denoted by ind has at least two elements and U is the result of closing the set containing the denotation of ind and the denotation of bool under function space formation will be a model of this theory. But a type definition based on lambda x_bool . x_bool =_ T allows us to extend LOG' to a theory LOG'' in which the existence of a unit type is postulated. The soundness theorem implies that LOG' is consistent, but, clearly, LOG'' is inconsistent. Hence, LOG'' is not a conservative extension of LOG'. 9. Adding New Quantifiers Judging from what Tom Melham said at last year's HOL Workshop and in subsequent messages to info-hol, there is considerable interest in extendending HOL to include quantifiers that bind type variables. The models defined in this document are sufficient to support a definition of denotation for terms involving type quantifiers and, moreover, quantifiers binding variables, where "variable" is understood in the sense explained in section 3. In such an extension, one would have boolean terms of the form Forall nu . A, where Forall us a new variable binder, nu is a type variable or a variable, and A is a formula. Given a model M and a valuation V assigning types to the free type variables of such a term, the denotation of Forall nu . X in M under V would be truth if X denoted truth in M under every V' differing from V only at nu; otherwise, Forall nu . X would denote falsehood in M under V. I have not had a chance to write down rules of proof for this extension of HOL or to explore the expressive power of the resulting language, but the language must be very expressive and I see no obstacle, in principle, to developing an appropriate proof theory. It also remains to be seen how the quantificational extension of HOL proposed here is related to the version of HOL with type quantifiers under development at Cambridge. [And65] Peter B. Andrews, A Transfinite Type Theory with Type Variables, North- Holland, 1965. [And86] Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth through Proof, Academic Press, 1986. [Bar84] H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland, 1984. [Hen50] Leon Henkin, Completeness in the theory of types, Journal of Symbolic Logic, vol. 15 (1950), pp. 81--91. [HOL] The HOL System Description, Cambridge Research Center of SRI International. Distributed with HOL version 1.12. [Kle50] Stephen Cole Kleene, Introduction to Metamathematics, van Nostrand, 1950. [Sho67] Joseph R. Shoenfield, Mathematical Logic, Addison-Wesley, 1967. [Sup57] Patrick Suppes, Introduction to Logic, van Nostrand, 1957.