HIGH-LEVEL CORRECTNESS OF ACL2: A STORY (DRAFT) Matt Kaufmann Computational Logic Inc. 1717 W. 6th St. Suite 290 Austin, Texas 78703 OUTLINE: PART 0: Informal summary PART 1: Mathematical Foundations PART 2: Correctness of ACL2 APPENDIX: Conservativity of Skolemization PART 0: Informal Summary The purpose of this note is to tell a story that explains the ``meaning'' of ACL2 logical worlds. Unlike Nqthm, ACL2 provides a structuring mechanism (through the encapsulate event) that makes it slightly tricky to implement a consistent logic. The notions of ``local events'' and ``books'' must also be accounted for in this story. We introduce the notion of a "history", which is a sequence of axiomatic acts (typically definitions), as well as the notion of a "chronology", which is a history together with some theorems of that history. Thus, the restriction of a chronology to the axiomatic acts within it is a history. Loosely stated, our specification of ACL2 is that it must maintain the following invariant: its logical world corresponds to such a chronology. In summary, our goal is to introduce a notion of "chronology" that is: generous enough to allow us to verify the claim that every ACL2 logical world encodes a chronology; yet, restrictive enough to allow us to prove desirable properties of chronologies. Then we will know that every ACL2 logical world possesses those desirable properties. In fact, this note is split into two main parts. Part 1, which is much longer than Part 2, is purely mathematical. It introduces appropriate notions that help us to formalize an appropriate notion of chronology. Part 2 uses the theorems proved in Part 1 to convince us that ACL2 logical worlds have the desired logical properties. An Appendix is also included, which contains a proof of the conservativity of Skolemization in our context. Part 1 is organized roughly as follows. 1. A notion of "history" is formalized that directly captures our understanding of what it means to be an ``appropriate'' sequence of axiomatic acts (definitions, axioms, encapsulations, Skolem function introductions). It is important that this definition be a reasonable model of the axiomatic process one undergoes when using ACL2. 2. In order to carry out the verification of our claim of ACL2 correctness (in Part 2), we need to know that functional instantiation is sound. Much of the first part leads up to the proof of such a result, Theorem 2'. 3. The class of "chronologies" is then defined. The actual definition is not important, as long as we can prove appropriate properties of this class. Here are some of those properties, many of which are contained in Theorem 3. A chronology is a sequence containing axiomatic acts and theorems about the functions introduced in those axioms. If s is a chronology, we may write H(s) for the subsequence of axiomatic acts of s, which is a history. In particular, every history h is a chronology, where H(h) is h. We write THM(s) for the subsequence containing the rest of s, which consists of theorems provable from H(s). 4. Throughout Part 1 we prove nice structural properties of the classes of histories and chronologies. For example, each class is closed under the taking of initial segments, and their "defaxiom-free" members are consistent (by the Consistency Corollary and corollary to Theorem 3). Perhaps more interesting, every defaxiom-free history conservatively extends each of its subhistories (by Theorem 1). Hence in particular, and what is somewhat easier to prove, a defaxiom-free history conservatively extends each of its initial segments. Here we take for granted the conservativity of Skolemization in our context, deferring its proof to the Appendix. Again, in Part 1 we formalize notions of history and chronology with complete rigor. Each of the claims above are immediate consequences of these formalizations and theorems that we prove rigorously. In Part 2 we make the following claim and present a justification of it. In light of the properties listed above, we think it fair to assert that this claim is what we are really after. CLAIM. Let w be an ACL2 logical world that is constructed from the initial ACL2 logical world using embedded event forms. Then w encodes a chronology. The verification of this claim is informal, since we only hint at the notions of "logical world" and "encodes" rather than define them rigorously. Moreover, our informal verification will rely implicitly on the correctness of the ACL2 theorem prover, which implies that we will ignore obvious issues such as the correctness of the instantiation rule of inference in the context of first-order logic. Thus, we will not bother to justify rewriting, nor will we justify the use of :instance directives in :use hints. We will however justify the use of :functional-instance directives in :use hints, which is more problematic. In fact, we will formulate and prove the correctness of functional instantiation in Part 1, as indicated above. Remark. In this note we omit consideration of whether we correctly handle the ACL2 notion of state. This, and undoubtedly other aspects of the implementation, must surely be considered if we are to claim that the implementation is ``correct.'' They are simply beyond the scope of this note. PART 1: Mathematical Foundations In order to simplify the discussion, we view the syntax of ACL2 as that of first-order logic; in particular, we ignore packages, constants, macros, and LAMBDAs (LETs, MV-LETs), viewing these all as ``syntactic sugar.'' We will feel free to be loose in our distinction between terms and formulas. When we talk about notions such as "theorem" or "provable", we mean them in the sense of first-order logic. We also fix a consistent first-order ``ground-zero'' theory GZ that includes appropriate axioms in the language with equality as the only relation. GZ introduces a set PR of function symbols, the "primitive functions", which must never be functionally instantiated. We assume that the usual axioms about CONS, CAR, and CDR, as well as the definition of MEMBER, are included in GZ,as this allows the representation of finite sequences in the theory; more on that below We will refer to the "epsilon-0 induction axioms", which are the universal closures of all formulas of the following form. (forall y (implies (and (e0-ordinalp y) (forall x (implies (and (e0-ordinalp x) (e0-ord-lessp x y)) phi[y:=x]))) phi)) --> (forall y (implies (e0-ordinalp y) phi)) We assume that the theory GZ actually implemented by ACL2 meets the requirements above, in particular, that it is consistent. One can verify this claim by considering the usual universe of Lisp objects, restricted to what we call ``good'' lisp objects (ones built using the data types present in ACL2). We take for granted the notion of "measure theorem" for a definition with respect to a measure (or, a mutually recursive nest of definitions with corresponding measures), which is completely analogous to the corresponding Nqthm notion (extended in the obvious way to mutual recursion). When the measure theorem can be stated and proved in a given first-order theory, we take it as well-known that (given the epsilon-0 induction axioms stated above) the definitional axioms being introduced are consequences of explicit (non-recursive) definitions that can be made in that theory. A careful look at this proof shows that our assumption above for GZ about CONS, CAR, CDR, and MEMBER allows us to code computations in the manner usually done to justify recursive definitions. The idea is that finite sequence can be coded as a list of pairs where each successive pair increments the CAR by 1. Notation. Definitions and introduction of notation, as well as proofs of lemmas and theorems, conclude with the symbol -|. When the proof is obvious, this symbol appears immediately after the statement of the lemma or theorem. -| Definition. A "labeled formula" is a pair consisting of a formula and a label, where the label is of one of four forms below. , where fns is a finite set of function symbols. , where fn is a function symbol. , where s is a sequence of labeled formulas. We will feel free to confuse a labeled formula with its formula when the meaning is clear, and to call its universal closure an "axiom of" or "axiom introduced by (in)" any sequence in which it appears. We may refer to a label as a "defuns label", a "defchoose label", a "defaxiom label", or a "constraint label", in the obvious sense. We may also use phrases such as "the axiom labeled by defun" when the meaning is clear. -| Convention. All sequences in this note are finite sequences. Notation. We write h,A to denote the result of extending a sequence h by a new element A, and h,A,h' to denote the result of extending a sequence h by the new element A and then by the sequence h'; and so on. It will be clear from the context which objects being concatenated are elements and which are sequences. -| Next we define a notion of "weight", which provides a suitable measure for the admissibility of many recursive definitions that follow. Definition. We recursively define a natural-number-valued function, weight, on labeled formulas and sequences of labeled formulas. The weight of a labeled formula is 1 unless the label is of the form , in which case its weight is weight(s)+1. The weight of the empty sequence is 0. If A is a labeled formula, then the weight of h,A is weight(h)+weight(A)+1. -| Definition. The (set of) "function symbols introduced by" a labeled formula or a sequence of labeled formulas is defined recursively (using weight as a measure) as follows. A formula labeled by introduces the set of function symbols fns; similarly introduces {fn}. A formula labeled by introduces the empty set of function symbols. A formula labeled by introduces the set of function symbols that s introduces. A sequence of labeled formulas introduces the union of the sets of function symbols introduced by each labeled formula in the sequence. -| See the ``Remark on local functions'' below for an explanation of why we do not need to model the aspect of the ACL2 implementation that provides, in an encapsulate event, for local function definitions of function symbols not mentioned in its signature. Definition. A sequence of labeled formulas is "defaxiom-free" if none of its labels are defaxiom labels and moreover, for each label of a member of this sequence, s is defaxiom-free. -| Definition. We define the "theory of" a sequence h of labeled formulas to be the set of first-order consequences of the union of GZ with the universal closures of those formulas, together with all epsilon-0 induction axioms in the language containing PR together with all function symbols introduced by h. When our meaning is clear, we will feel free to confuse a sequence of labeled formulas with its theory. We will also feel free to talk about one sequence h0 of labeled formulas "conservatively extending" another sequence h1 of labeled formulas, to indicate that the theory of h0 conservatively extends the theory of h1. (Recall that a theory T0 conservatively extends a theory T1 if T0 extends T1 and moreover, every theorem of T0 in the language of T1 is a theorem of T1.) -| The following is obvious and well-known. Transitivity of Conservative Extension Lemma. If h0, h1, and h2 are theories or sequences of labeled formulas such that h0 conservatively extends h1 and h1 conservatively extends h2, then h0 conservatively extends h2. -| Definition. Let h be a sequence of labeled formulas. A "function symbol of" h is a function symbol that is either introduced by h or is a member of PR. A "formula of the language of" h is a formula all of whose function symbols are function symbols of h. -| Next, we prepare for the introduction of the notion of "history" by defining a weaker notion in which proof obligations are ignored. Definition. A "pseudo-history" is a finite sequence h of labeled formulas meeting the following requirements. 1. For each labeled formula in h whose label is not a defaxiom label, the set of function symbols introduced is non-empty. 2. Every function symbol occurring in the formula of a labeled formula A of h must either be introduced by A or be a function symbol of the set of predecessors of A in h. 3. The family of all sets of function symbols introduced by labeled formulas in h is pairwise disjoint, and each such set of function symbols is also disjoint from PR. (Thus, no introduced function symbol can occur in GZ.) 4. For each labeled formula in h whose label has the form , ev is a defchoose event that introduces fn, and the formula should be the appropriate one. (See the Appendix for details.) 5. For each labeled formula in h whose label has the form : s is a defaxiom-free sequence of labeled formulas and h,s is a pseudo-history. -| 6. For each labeled formula A in h whose label has the form , ev consists of definitions of the function symbols in fns. If the definitions are (mutually) recursive, then ev also contains measures for each that are definable using function symbols of the subsequence of h preceding A. -| Definition. A "history" is a pseudo-history h that meets the following additional requirements. 5'. Part 5 of the definition of pseudo-history is extended so that for each labeled formula A of h with label , we have that h,s is a history, and A is a theorem of the theory of that history. 6'. Part 6 of the definition of pseudo-history is extended so that for each labeled formula A in h that is labeled by defuns, the corresponding measure theorem is a theorem of the theory of the subsequence of h preceding A. -| Implementation note. When an encapsulate event in ACL2 does not introduce any local functions, it is viewed simply as the sequence of non-local events contained within. This allows us to satisfy Property 1 above. That property could probably be safely omitted, but at any rate, ACL2 does not introduce constraints when there are no local functions in an encapsulate. The purpose is to reduce the proof obligations arising later from functional instantiation. Remark on local functions. In the ACL2 implementation, when introducing an encapsulate event, one may introduce local definitions of functions that are not in the signature of the encapsulate. How does this situation fit into our notion of history? The real problem is that we need to be able to delete the local events and still have a history. Rather than deal with that issue here, we have defined our notion of history without any allowance for deleting local events. In Part 2 we allow for the deletion of local events before enclosing them in an encapsulate event. We argue in that setting that the resulting encapsulate event preserves the requirement that the labeled axioms form a history. We will use the following obvious lemma implicitly. Lemma. Every initial segment of a (pseudo-)history is a (pseudo-)history. -| Monotonicity lemma. Suppose that h0,h1,h2 is a history, and that h0,h1' is a history whose theory contains that of h0,h1, such that no function symbol introduced by h1' is introduced by h2. Then h0,h1',h2 is a history. Proof: an easy induction on the weight of h2, which we omit. The key idea is that the proof obligations introduced during the processing of h2 are still provable if we replace h1 by the larger history h1'. -| Definition. The "puffing" of a sequence of labeled formulas is defined as follows. The puffing of the empty sequence is the empty sequence. The puffing of h,A where A is labeled by is the puffing of h,s. Finally, the puffing of h,A for any other labeled formula A is h',A where h' is the puffing of h. -| Puffing Lemma. Let h1 be the puffing of the sequence h0 of labeled formulas. Then h1 is a sequence of labeled formulas having the following properties. (a) h1 and h0 introduce the same function symbols. (b) The theory of h0 is a subset of the theory of h1, and hence for all sequences h and h' of labeled formulas, the theory of h,h0,h' is a subset of the theory of h,h1,h'. (c) For every history h, if h,h0 is a history, then h,h1 is a history. (d) If h0 is defaxiom-free then h1 is defaxiom-free and contains no constraint labels. Proof: an easy induction on weight. The Monotonicity Lemma is used for the proof of (c). -| Our next goal is a Conservativity Lemma, stating that histories provide conservative extensions. In fact we prove a slightly stronger result that is useful later. The following two lemmas are crucial for the proof. Conservativity of Defuns Lemma. Suppose that h is a sequence of labeled formulas. Suppose also that A is a formula labeled by defuns, all of whose function symbols are function symbols of h, whose corresponding measure theorem is a theorem of h. Then h,A conservatively extends h. Proof sketch. Note that the theory of h,A includes all epsilon-0 induction axioms in the function symbols introduced by h,A together with PR. With this in mind, recall an earlier remark: the measure theorem of A allows us to prove A in an extension of h by an explicit definition, using the usual proof of the correctness of definition by recursion. The point is that this proof can be carried out inside the theory of h, using epsilon-0 induction. The lemma then follows from the eliminability of function symbols with explicit definitions. -| Conservativity of Defchoose Lemma. Suppose that h is a sequence of labeled formulas. Suppose also that A is a formula labeled by defchoose, all of whose function symbols are function symbols of h. Then h,A conservatively extends h. Proof: Deferred to the Appendix. -| Conservativity Lemma. If h0,h1 is a history and h1 is defaxiom-free, then h0,h1 conservatively extends h0. More generally: under the assumptions above, if h0' is any sequence of labeled formulas that includes h0 as a subsequence, then h0',h1 conservatively extends h0'. Proof. Suppose that phi is a theorem of the theory of h0',h1 which is a formula of h0', and let h2 be the puffing of h1. Then phi is a theorem of h0',h2 by part (b) of the Puffing Lemma, so by parts (c) and (d) of the Puffing Lemma, it suffices to prove the Conservativity Lemma in the case that h1 consists entirely of formulas labeled by defuns and defchoose, which will tell us that phi is a theorem of h0'. We proceed by induction on the length of such a history h1. The case that h1 is empty is clear. Otherwise let us write h1 as A,h1'. We can apply the inductive hypothesis using: h0,A for h0; h0',A for h0'; and h1' for h1. Then, we may conclude that h0',A,h1' (which is h0',h1) conservatively extends h0',A. Thus it remains only to show that h0',A conservatively extends h0', since then we are done by the transitivity of conservative extension. But this is immediate from the two immediately preceding lemmas. For the defuns case we are using the hypothesis that h0' extends h0, together with the fact that the measure theorem for A is provable in h0 (because h0,h1 is a history). -| Consistency Corollary. Every defaxiom-free history is consistent. Proof. This is immediate from the Conservativity Lemma, where h0 is the empty history and h1 is the given defaxiom-free history, since GZ has been assumed to be consistent. -| Definition. We define the "set of ancestors of" a function symbol or a labeled formula as follows. Every member of PR has the empty set of ancestors. Now fix a history and let A be a labeled formula in that history that introduces a function symbol fn (perhaps among others). The "set of ancestors of" fn (with respect to this history) is defined to be fn together with the set of ancestors of the formula of A. Finally, the set of ancestors of a labeled formula A is the union of the set of function symbols introduced by A with the set of ancestors of all function symbols occurring in A that are not introduced by A. The "set of proper ancestors" of a labeled axiom, or of a function symbol introduced by the labeled axiom, is defined to be the result of removing function symbols introduced by the labeled axiom from the set of ancestors. -| Definition. Suppose h is a sequence of labeled formulas, and suppose h' is a subsequence of h. We say that h' is "closed under ancestors" (with respect to h) provided the following two conditions hold. (1) Every ancestor of every function symbol introduced by h' is also introduced by h'. (2) Every element A of h with a defaxiom label is a member of h', and moreover, every ancestor (with respect to h) of A is introduced by h'. -| Note that if h' is closed under ancestors with respect to a pseudo-history h, then every function symbol occurring in a formula of an element of h' is in PR or is introduced in h'. The following simple lemma is a key ingredient of the argument required for Theorem 1. Restriction Lemma. Suppose that h0,s,h1 is a sequence of labeled formulas such that h0,s is a history, where s is defaxiom-free, and suppose that that the function symbols introduced in s do not occur in h1. Then h0,s,h1 conservatively extends h0,h1. Proof. Since h0,s is a history and s is defaxiom-free, then by the Conservativity Lemma, h0',s conservatively extends h0' for every sequence h0' of labeled formulas that extends h0. In particular, h0,h1,s conservatively extends h0,h1, and this is just another way of stating the conclusion above. -| Theorem 1. Suppose h is a history and h' is a subsequence of h that is closed under ancestors. Then h is a conservative extension of h'. Proof: by induction on the number of labeled formulas in h that are not in h'. If that number is 0, then we are done. Otherwise, let A be the first such. Let h'' be the result of inserting A into h' so that the result is a subsequence of h; thus we may write h'' as h0,A,h1 where h' is h0,h1, and h0,A is an initial subsequence of h. Thus h'' is closed under ancestors. By the inductive hypothesis, h is a conservative extension of h''. Since the relation of conservative extension is transitive, it suffices to show that h'' is conservative over h', i.e., that h0,A,h1 is conservative over h0,h1. Since h' is closed under ancestors, A is not labeled by a defaxiom label. Hence we are done by the Restriction Lemma, provided we can show that the function symbols introduced in A do not occur in h1. But this is clear since h0,h1 is closed under ancestors. -| With Theorem 1 we can prove a functional instantiation result. We'll prove a simplified version first (Theorem 2) and then derive the general version (Theorem 2') from that one. Definition. Let h be a history. A pseudo-function of h is either a function symbol of h, or an expression of the form (lambda vars term) where vars is a list of distinct variables and every function symbol occurring in term is a function symbol of h. In the latter case we define the arity of the pseudo-function to be the length of vars. -| Definition. A "functional substitution" (with respect to a history h) is a finite function fs from function symbols introduced in h to pseudo-functions of h, which preserves arity. If the range of fs consists entirely of function symbols, we call it a "simple functional substitution" (with respect to h). -| Notation. x\fs is the functional instance of the term or formula x by the functional substitution fs. (We may call this a "simple functional instance" when fs is simple.) We omit details of this definition, which can be found (at least when x is a term) in the paper ``Functional Instantiation in First Order Logic'' by R.S. Boyer, D. Goldschlag, M. Kaufmann, and J S. Moore, in: ``Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy,'' Academic Press, 1991, pp. 7-26. -| Lemma on Functional Instantiation and Theorems. Suppose that psi is a theorem of a first-order theory T and that fs is a simple functional substitution whose domain is disjoint from the function symbols of T. Then psi\fs is a theorem of T. Proof. This is easy to see proof-theoretically using one's favorite proof theory for first-order logic, since A\fs = A for every axiom A of T, and the rules of inference remain valid when applying fs to all formulas in them. It's also easy to see model theoretically, as follows. First, note that it suffices to assume that the domain and range of fs are disjoint, since we may write fs as the composition of two appropriate functional substitutions with that property. (Roughly: First rename the symbols in the domain to symbols occurring nowhere in sight, and then map those to the final values.) Now given any model of T (which also interprets the symbols in the range of fs, but not in the domain of fs) that satisfies the negation of psi\fs, we may expand this to a model of the negation of psi by interpreting every function symbol in the domain of fs to be the interpretation of the corresponding function symbol in the range of fs. -| Theorem 2. Suppose that fs is a simple functional substitution with respect to a history h and that phi is a theorem of h. Suppose further that h' is a subsequence of h that is closed under ancestors, such that phi is a formula of the language of h'. Finally, suppose that for every axiom A introduced in h', A\fs is a theorem of h. Then phi\fs is a theorem of h. Implementation note. Although we consider function symbols individually in our treatment of mutual recursion, we enforce the restriction that every function symbol in a mutual recursion nest is an ancestor of every other one. So, we will ``pick up'' all of their definitions when any of them is ``hit''. Proof of Theorem 2. Since phi is (by assumption) a theorem of h, it is also a theorem of h', by Theorem 1. Fix a proof of phi from the theory of h', and let S be the finitely many induction axioms used in in the proof of phi from h'. Thus, letting A be the universal closure of the conjunction of the axioms introduced in h', we have that [(A & S) -> phi] is a theorem of GZ. By the Lemma on Functional Instantiation and Theorems, it follows that [(A & S) -> phi]\fs is a theorem of GZ, i.e., that [(A\fs & S\fs) -> phi\fs] is a theorem of GZ, hence of h. But A\fs is a theorem of h by hypothesis, so it suffices to show that S\fs is a theorem of h. Thus, our final claim is that the simple functional instance of an induction axiom is an induction axiom. This is clear from the form of induction axioms, since every simple functional instance of such a formula is of that form as well. -| In the ACL2 implementation of functional instantiation, we allow functional substitutions to map a function symbol f to a pseudo-function (lambda vars term), where the length of vars is the arity of f. Moreover, this pseudo-function may include free variables, i.e., variables occurring in term that do not belong to vars. So, we need to extend Theorem 2 to handle such functional substitutions. The following strengthening of Theorem 2 also notes the obvious fact that we need only consider functional instances of theorems that contain at least one function symbol bound in the functional substitution. Theorem 2'. Suppose that fs is a functional substitution with respect to a history h and that phi is a theorem of h. Suppose further that h' is a subsequence of h that is closed under ancestors, such that phi is a formula of the language of h'. Finally, suppose that for every axiom A introduced in h' such that some function symbol in the domain of fs occurs in A, A\fs is a theorem of h and no free variable of fs occurs in A. Then phi\fs is a theorem of h. Proof. First we claim that it suffices to prove this theorem under the assumption that there are no free variables of fs. For if there are, first extend h to a new history h0 that introduces, with no constraint (i.e., constraint t (true)), a distinct zero-ary function symbol for each variable free in fs. Now consider the functional substitution fs0 obtained from fs by replacing each variable free in fs by the corresponding new constant (i.e., call of a new zero-ary function). We claim that the hypotheses of Theorem 2' are satisfied with h0 in place of h and fs0 in place of fs (and with h' unchanged). This is clear except perhaps to check that A\fs0 is a theorem of h, provided A\fs is a theorem of h, where A is an axiom introduced in h' and no free variable of fs occurs in A. In fact this is clear, since under these assumptions, A\fs0 is the result of instantiating A\fs by replacing each free variable of fs by the corresponding new constant. Now that we have checked the hypotheses for Theorem 2' where fs and h are respectively replaced by fs0 and h0, we know (if we can prove Theorem 2' assuming fs has no free variables) that phi\fs0 is a theorem of h0. It follows (easily if we use a model-theoretic argument) that phi\fs is a theorem of h0, and hence (by the Conservativity Lemma) a theorem of h. So, let us assume that fs has no free variables. For each pair in fs, extend h by a definition of the form g(vars)=term, where g is a new function symbol. Let us call the resulting history h1, and let us write fs1 for the functional substitution obtained by replacing each expression (lambda vars term) as above by the corresponding new function symbol g. We claim that the hypotheses of Theorem 2' hold for h1 and fs1 in place of h and fs (and with h' unchanged); in fact we only need show that for A as before, A\fs1 is a theorem of h1, given that A\fs is a theorem of h. But this is clear since A\fs1 and A\fs are logically equivalent in h1. So the conclusion of Theorem 2' holds for h1 and fs1, i.e., phi\fs1 is a theorem of h1. But phi\fs1 is logically equivalent in h1 to phi\fs, so phi\fs is a theorem of h1. By the Conservativity Lemma, phi\fs is a theorem of h. -| We turn now to the notion of a chronology. As suggested at the outset of this note, our real goal is to formulate such a notion and show, at least at some abstract level, that ACL2 maintains the invariant that its logical world corresponds to a chronology. Intuitively, a chronology is built up from axiomatic acts (what we have called a ``history'') and theorems proved from those axioms. We distinguish between these two kinds of formulas in a chronology by labeling the ones that are intended to belong to the history. We would like a chronology to be a sequence of labeled and unlabeled formulas such that its restriction to labeled formulas is a history, and for every initial segment, the unlabeled formulas are theorems of the theory of the labeled formulas. Let us turn now to the goal of providing a precise definition. Definitions. Let s be a finite sequence of labeled and unlabeled formulas. (i) H(s) is the subsequence of s consisting of labeled formulas. (Intuitively, we think of H(s) as the history part of s, i.e., the axiomatic acts in s.) (ii) THM(s) is the set of universal closures of unlabeled formulas of s. (Intuitively, we think of THM(s) as the proved theorems of s.) (iii) s is a "pseudo-chronology" if H(s) is a pseudo-history and for every initial subsequence of s of the form s0,A where A is an unlabeled formula, every function symbol occurring in A is a function symbol of H(s0). -| Definition. The class of "chronologies" is the least class of sequences that contains the empty sequence and is closed under the operations given below. [Labeled extension] If s is a chronology and A is a labeled formula such that H(s),A is a history, then s,A is a chronology. [Unlabeled extension] If s is a chronology and phi is a formula in the language of H(s) that is provable from the union of the theory of H(s) with THM(s), then s,phi is a chronology. [Delete] If s is a chronology and s' is a pseudo-chronology, where s' is a subsequence of s that contains all labeled formulas of s with label defaxiom, then s' is a chronology. [Include] Suppose that s0 and s1 are chronologies, that s2 is the subsequence of s1 obtained by deleting labeled formulas of s1 that belong to s0, and that s0,s2 is a pseudo-chronology. Then s0,s2 is a chronology. -| Proposition. Every history is a chronology. Proof: By an easy induction on length, using the [Labeled extension] rule. -| Implementation note. ACL2 lays down certain ``command markers'' that indicate the initial segments of a given chronology that it will accept. However, this observation isn't relevant to the mathematics here. History Sufficiency Lemma. Suppose that h is a pseudo-history. Assume that for every initial segment h',A of h, there exists h'' such that h'',A is a history and the set of elements of h'' is a subset of the set of elements of h'. Then h is a history. Proof: by induction on the weight of h. If h is empty then this is trivial. Otherwise, write h as h',A. By the inductive hypothesis, h' is a history. And, we are given that h is a pseudo-history. So, it suffices to check clauses 5' and 6' from the definition of history. Using the assumption of the theorem we may choose h'' such that h'',A is a history, where the set of elements of h'' is a subset of the set of elements of h'. Now there are two cases to consider. First, suppose that A is labeled by . Since h'',A is a history, we have that h'',s is a history and A is a theorem of h'',s. Since h'' is contained (as a set) in h', we have that A is a theorem of h',s. Also, since h',A is a pseudo-history, then h',s is a pseudo-history. By the inductive hypothesis, we have that h',s is a history. Therefore h',A is a history. Second, suppose that A is labeled by . We must show that the measure theorem phi corresponding to ev is a theorem of the theory of h'. Since h'',A is a history, phi is a theorem of h''. Therefore, since h' contains h'' (as a set), phi is a theorem of h'. -| Combining Lemma. Suppose that h0 and h1 are histories, that h2 is the subsequence of h1 obtained by removing elements of h0 from h1, and that h0,h2 is a pseudo-history. Then h0,h2 is a history. Proof. This is an an immediate consequence of the History Sufficiency Lemma. -| Ancestors Preserve History Lemma. Suppose h is a history and h' is a subsequence of h that is a pseudo-history and contains all elements of h labeled by defaxiom. Then h' is a history. Proof. This is an easy induction on the weight of h', using Theorem 1 to guarantee that the proof obligations from the measure theorem are discharged. -| Theorem 3. Let s be a chronology. Then H(s) is a history, s is a pseudo-chronology, and THM(s) is a subset of the theory of H(s). Proof: by induction on the construction of the class of chronologies. The Ancestors Preserve History Lemma guarantees that the [Delete] rule preserves the first property, while Theorem 1 guarantees that it preserves the third property. The only other step requiring a bit of thought is the justification that H(s0,s2) is a history in the application of the [Include] rule. But it is a pseudo-history because s0,s2 is assumed to be a pseudo-chronology, so this follows from the Combining Lemma. -| Corollary . Let s be a chronology such that H(s) is defaxiom-free. Then the set of universal closures of formulas (labeled and unlabeled) of s is consistent. Proof. By the last part of Theorem 3, it suffices to show that H(s) is consistent, and this follows from the fact that H(s) is a history (first part of Theorem 3) together with the Consistency Corollary. -| PART 2: Correctness of ACL2 The ACL2 implementation contains a logical world, which "encodes" in a straightforward way a pseudo-chronology. However, we want to show more: a logical world should ``possess'' the properties guaranteed by Theorem 3, namely that its axiomatic events form a history, and its alleged theorems really are theorems. Hence, we make the following claim. CLAIM. Let w be an ACL2 logical world that is constructed from the initial ACL2 logical world using embedded event forms. Then w encodes a chronology. Remark: Ancestral measures. There is a subtlety here. In the actual implementation there is no check that the deletion of local events suggested by the [Delete] rule results in a logical world in which the original measures still make sense. However, suppose we imagine that every defuns event A only uses measures whose function symbols are proper ancestors of A. Then when the implementation ignores local events, it does not need to make any special check that the measures only use properly ancestral function symbols, because it preserves the invariant that all function symbols occurring in an event have in fact been introduced previously (or belong to PR). So we imagine that ACL2, which does not literally store any measures, in fact stores measures that only mention properly ancestral function symbols. Why may we make this assumption? One can define an interpreter for the union of PR and the ancestors of a defuns using only proper ancestors, where we use the original measure theorem to show that this interpreter is well-defined. By the usual argument, this interpreter is in fact explicitly definable from the set of proper ancestors of the defuns event. The desired measure is then the number of steps required for the interpreter to terminate on given inputs. Interestingly, this measure maps into the natural numbers; however, epsilon-0 induction is still needed in order to admit the interpreter. Note that the remark above justifies the prover's use of induction schemes. We now turn to the verification of the Claim above. For starters, the initial world is a chronology by design (at least that's the intention), at least if one imagines rearranging it as necessary. It remains then to check that each embedded event form is "acceptable" in the sense that it preserves the property that the logical world encodes a chronology. Now, many of the events (such as table events) have nothing to do with the chronology encoded by the logical world. Many others are macros abbreviating other events. It remains to consider the events that are left. Defaxiom is acceptable because of the [Labeled extension] rule. Defun (including mutual-recursion, i.e., defuns) is acceptable because of the [Labeled extension] rule, together with Theorem 3, which guarantees that it's sufficient to prove the necessary proof obligations using THM(s) in addition to H(s), and Theorem 2, which allows us to use functional instantiation. The Remark above shows that we can assume that the measures only use properly ancestral function symbols. Similarly, Defthm is acceptable because of the [Unlabeled extension] rule and Theorems 2 and 3. Include-book is acceptable by the [Delete] rule (which allows us to drop local events, since we do not allow local defaxiom events, to create a new ``book'') followed by the [Include] rule. The remark above justifies our use of the [Delete] rule, since we do not allow local defaxiom events. Verify-termination is acceptable because is is really extending the chronology in the same way that Defun(s) does; similarly for verify-guards, when applied to functions in :program mode. It remains to see that encapsulate is acceptable. The basic argument is not hard. We first apply the [Delete] rule to eliminate local events, since we do not allow local defaxiom events. If at least one local function is introduced, then we apply the [Labeled extension] rule, using the definition of history for axioms labeled by encapsulate. The remark above justifies the implementation's lack of a check that the remaining subsequence of events is truly a pseudo-chronology in the sense that the measures are in the appropriate language. In fact, however, we need to extend this argument slightly, because we employ certain "optimizations" in the implementation. First of all, if a function f is non-locally defined in the scope of an encapsulate, and f does not have any functions from the signature among its ancestors, then we do not store a constraint for f. Why is this "optimization" justified? First, suppose for simplicity that there is only one such function. As remarked above, we may assume that its measure (if the definition is recursive) is defined using only function symbols ancestral in the definition. The measure theorem is then a theorem of the pre-encapsulate history, by the Conservativity Lemma. By the Ancestors Preserve History Lemma, it is easy to see that if we leave the encapsulate "unwrapped" and move this defun in front of it, the result is still a history. Now we can apply the argument of the preceding paragraph to show that the encapsulate is acceptable. The argument above may be extended in the obvious way to several defuns and defchooses, by moving them out front one at a time. It may also be extended to defthm and encapsulate events, using the same conservativity argument used above for measure theorems. Thus, we conclude that every encapsulate may be replaced by moving, just in front of it, all definitions and theorems for which none of the functions declared in the signature are ancestral. In fact this process may be done recursively, to handle nested encapsulates. In the implementation we do not actually move events, but we create constraints that pretend that we did. The argument above also justifies the implementation's check for so-called ``subversive inductions,'' in which we disallow induction schemes for which a newly-constrained function is ancestral. It's clear that we need only check such schemes if we imagine moving definitions in front of the encapsulate, in the sense described above, whenever possible. Having moved certain events to in front of the encapsulate, we now imagine moving certain events to the back. Suppose that, after moving whatever we can in front of the encapsulate, we collect up all formulas introduced in the encapsulate except for those introduced by defuns and defchoose, where the symbols introduced have no other constraints. We claim that it is OK to imagine moving, to after the encapsulate, all of those defuns and defchoose events for symbols not ancestral in any of those collected up formulas. For, first note that the remaining events form (with the pre-existing world before the encapsulate) a pseudo-chronology, so we may still form an encapsulate from those, by the [Delete] rule. Then, if we extend the resulting chronology by the omitted defuns and defchoose events, in their same order, then we may apply the [Labeled extension] rule. Why? First observe that the Conservativity Lemma guarantees that the defuns' proof obligations are met. This allows us to apply the Conservativity of Defuns Lemma and the Conservativity of Defchoose Lemma to ensure that we are correctly applying the [Labeled extension] rule. APPENDIX: Conservativity of Skolemization We wish to check the conservativity of Skolemization in our context, where each time a function symbol is introduced, so are all the epsilon-0 induction axioms about the symbol (and the existing function symbols). If we were dealing with a logic that precluded non-standard numbers, we could manage more simply, because there would be no need to worry about the epsilon-0 induction axioms introduced when we add a new function symbol (a Skolem function). That is: every sort of induction scheme is automatically true when the natural numbers of the model are standard! But we do not want to leave the realm of first-order logic if we can avoid it; for example, that would eliminate the potential for integrating some non-standard analysis into the system, and it would require us to re-think our proof theory. Fortunately, we'll see that we can assume that there is a definable enumeration of the universe, which allows us to define a Skolem function explicitly: it picks out the least witness in the sense of this enumeration. The remainder of this Appendix works out this argument reasonably carefully. We thank Jim Schmerl for suggesting the key ideas that allow us to carry out the argument allowing for an enumeration of the model. Definition. For any first-order formula phi with free variables contained in the sequence v,x1,..,xk of distinct variables, and any function symbol f of arity k, the "Skolem axiom introducing" f for phi with respect to v is defined to be the following formula. (implies phi (let ((v (f x1 ... xk))) phi)) We also allow more than one bound variable: if phi has free variables among the distinct variables v1,...,vn,x1,..,xk (n>1) and f is a function symbol of arity k, the "Skolem axiom introducing" f for phi with respect to v1,...,vn is defined to be the following formula. (implies phi (mv-let (v1 ... vn) (f x1 ... xk) phi)) -| Notation. Let F be a set of function and relation symbols that includes the unary relation symbol N. We write IND(N,F) for the theory containing all epsilon-0 induction axioms in the language of F. -| The following easy lemma is surely well known. Lemma. Suppose that T1 is a subtheory of the first-order theory T2 such that for every model M of T1, every sentence A true in M, and every finite subset T2' of T2, there is a model of T2' satisfying A. Then T2 is a conservative extension of T1. Proof. Suppose for a contradiction that T2 is not a conservative extension of T1; say, phi is in the language of T1 and is a theorem of T2, but phi is not a theorem of T1. By the Completeness Theorem for first-order logic, Let M be a model of T1 that satisfies the negation A of phi. By hypothesis and the Compactness Theorem of first-order logic, we may choose of model of T2 that satisfies A, i.e., does not satisfy phi. This contradicts the choice of phi. -| The next lemma is not at all obvious. If we were not concerned about induction axioms, it would be trivial to conservatively extend a theory by adding a bijection between the universe and its natural numbers, by the downward Lowenheim-Skolem theorem of first-order logic. Something fancier is needed, however, if we want to preserve induction. Lemma. Suppose that T is a first-order theory in the finite language F containing PR, which contains GZ as well as IND(N,F). Then it is conservative to extend T by adding an axiom introducing a new unary function symbol g, asserting that g maps the universe 1-1 onto N, together with IND(N,FU{g}). Proof sketch. We sketch two arguments, both of which are quite technical and model-theoretic, and both of which were suggested by Jim Schmerl. Let M be a model of T. In each case we show how to expand it to a model of the desired assertion on g together with IND(N,FU{g}) (or, in the second argument, an arbitrary finite subset of this set). Thus, the preceding lemma yields the desired conservativity claim, by applying it to the two theories described in the present theorem. Both arguments only require that the usual induction axioms hold in the model M, not epsilon-0 induction. The more standard and direct argument uses a variant of Cohen's forcing technique from set theory, adapted to models of arithmetic. Thus, fix a countable model M of T. The partial order here consists of 1-1 ``finite'' (in the sense of M) functions from an initial segment of the interpretation of N in M, that are coded in M. A standard argument shows that a function through this partial order, generic with respect to all dense sets definable with parameters in M, gives the desired expansion of M. Details are omitted here. The main ideas (given here only briefly, for experts) are to prove first the usual truth lemma, and then to show that if p forces that phi(x) defines an inductive subset of N, and if n is in N, then the set of conditions that force all predecessors of n to satisfy phi is dense below p. Hence if p is in the generic set, then a member of that dense set is also in the generic set, and hence phi holds for all predecessors of n in the generic model. Since n is arbitrary, then phi holds for all elements of N in the generic model. The second argument uses a theorem of Jim Schmerl, in ``A reflection princple and its applications to nonstandard models'' (to appear in the Journal of Symbolic Logic). That theorem tells us that given any sentence phi in the language of Peano Arithmetic extended by F, any model M of IND(N,F) that satisfies phi, and any finite subset T' of T, there is a model M1 of phi satisfying T' that is definable inside M and is contained in M's interpretation of N, such that M1's interpretation of N is isomorphic, via an isomorphism j definable in M, to M's interpretation of N. (The presence of CONS, CAR, CDR, and MEMBER in GZ allows us to code up finite sequences in the manner required by Schmerl's theorem.) Because M1 is definable in M, it follows follows that M1 is also a model of IND(N,FU{g}), for any function g on M1 definable in M. Now since M1 is contained in the interpretation of N in M, there exists a 1-1 enumeration of the elements of M1 that is definable in M. By composing it appropriately with the aforementioned definable isomorphism j, we have a 1-1 function g from M1 onto the interpretation of N in M1, which is definable in M and thus expands M1 to a model of IND(N,FU{g}), as argued above. -| Theorem. Suppose that T is a first-order theory in the language F containing the relativization of Peano Arithmetic to N as well as IND(N,F). Then it is conservative to extend T by adding a Skolem axiom introducing a new function symbol f together with IND(N,FU{f}). Proof. The preceding lemma allows us extend the given theory conservatively to include a function g mapping the universe 1-1 onto N, together with IND(N,FU{g}). Thus, by transitivity of conservativity it suffices to extend this new theory in the manner indicated. But this is easy because in the indicated theory with g, we may explicitly define the desired Skolem function f. We do so simply by picking the least witness, i.e., that value g(n) witnessing the given condition for which n is least (if any witness exists; else, 0, say). -| The theorem above implies the following lemma from Part 1, whose proof we deferred. Conservativity of Defchoose Lemma. Suppose that h is a sequence of labeled formulas. Suppose also that A is a formula labeled by defchoose, all of whose function symbols are function symbols of h. Then h,A conservatively extends h. -| [end]