		Search-engine friendly clone of the ACL2 documentation.

Zfc-model

Justification for integrating set theory with ACL2

See zfc for an introduction to the integration of set theory with ACL2. The present topic provides intuition and sketches a foundation for that integration.

This documentation topic displays events as though the current-package is "ZF".

Our first-order set theory

Before we get to the question of how set theory and ACL2 are integrated, let's discuss the relevant set theory.

Our formalization of set theory starts with Zermelo-Fraenkel set theory, typically known as ZF. It is a first-order theory that formalizes familiar properties of sets: given x and y there is a pair set {x,y} (i.e., unordered pairs exist), there is an infinite set, and so on. Our foundation is actually ZFG, which is ZF extended by the axiom of global choice. ZFG adds a function symbol, say G, to the language of ZF and adds the axiom that G(x) is an element of x for every non-empty x. (Our formalization actually uses the name min-in rather than G; see zfc.)

ZF captures the notion of set provided by the so-called cumulative hierarchy: start with the empty set, and then iterate the powerset (set of all subsets) operation. Iteration is through the ordinals, which can be viewed as follows. The least ordinal is 0, which is the empty set. More generally, each natural number n is an ordinal, namely, the set of natural numbers less than n. Thus, the less-than relation (<) on natural numbers is simply set membership. Yet more generally, an ordinal is any set that is transitive — every element of an element is an element — and is linearly ordered by set membership. The first infinite ordinal, ω, is the set of all natural numbers; next is ω+1, which is the union of ω and {ω}, next, ω+2, and so on, with ω+n+1 equal to the union of ω+n and {ω+n}. The union of all these ω+i is ω+ω, also known as ω*2; and so on. See o-p for more about ordinals.

In ZF, every object is a set that is contained in a member of the cumulative hierarchy V_0, V_1, V_2, ..., V_ω, V_{ω+1}, ..., V_{ω*2}, .... In general V_{α+1} is the powerset of V_α, and for a limit ordinal α — one that is not an immediate successor, such as ω — V_α is the union of {V_β: β \in α}.

Defining ACL2 objects in set theory

Recall (see zfc) the notion of a hypothesis function: a zero-ary function constrained by an encapsulate event that serves as a hypothesis for most of the theorems exported from that encapsulate event. Thus, zfc, as well as hypothesis functions introduced by calls of zsub and zfn, may appear in :props arguments of defthmz events. Those arguments generate hypotheses that are necessary for provability, but we would like a logical basis for ignoring them. The rest of this documentation topic gives that logical basis.

In a nutshell, that logical basis is provided by showing how ACL2 data and functions can be defined in the ZFG universe of sets, with all hypothesis function calls being true. Then assuming ZF is consistent — hence, as is well-known, so are ZFC and also ZFG — every defaxiom-free ACL2 theory extended by all :props calls, including (zfc), is consistent by virtue of being true in that universe. We give more details in the next section, but for now we simply explain how ACL2 objects are defined in set theory.

The first step is to identify each ACL2 natural number with the corresponding finite ordinal. We next define the other usual atoms — integers, rationals, complex rationals, characters, strings, and symbols — by encoding them as sets. By treating cons as the set-theoretic ordered-pair constructor as explained below, we are able to identify all good ACL2 objects — those built up from those atoms using cons — as sets, hence, those ACL2 objects that are definable in ZFG. Here is the recognizer for the good ACL2 objects.

(defun acl2p (x)
  (declare (xargs :guard t))
  (cond ((consp x) (and (acl2p (car x))
                        (acl2p (cdr x))))
        ((bad-atom x) nil)
        (t t)))

Every good ACL2 object, when interpreted as a set as described below, is in a finite stage of the cumulative hierarchy.

(defthmz v-omega-contains-acl2p
  (implies (acl2p x)
           (in x (v-omega)))
  :props (zfc v$prop domain$prop prod2$prop inverse$prop)
  :hints ...)

The encapsulate event introducing zfc exports many basic theorems. Many of those are noted in the documentation topic, zfc, but not mentioned there are those exported theorems pertaining to the encoding of good ACL2 objects as sets. A key property, alluded to above, is to interpret (cons x y) as the set-theoretic ordered pair. That is traditionally the set {{x},{x,y}}, formalized as follows.

(defthmdz cons-as-ordered-pair
  (equal (cons x y)
         (pair (singleton x)
               (pair x y))))

Note that a cons is never a natural number, because (cons x y) = {{x},{x,y}} is always a non-empty set that does not contain 0 (the empty set), but no finite ordinal has that property. Also note that a cons always has at most two elements.

We encode the other atoms as sets of the form (zf::ztriple y z) = {0,y,z}, where y is a positive natural number and z is not a natural number — in fact z will always be a cons. Thus each such set is a three-element set, hence is not a cons. It is also not a natural number (finite ordinal) since its element z is not a natural number. And finally, these are clearly distinct for different natural numbers y. The interpretations are as follows, where make-listp0 creates a list terminated with 0 rather than nil, to avoid potential circularity in the encoding of the symbol, nil.

(defun negative-int-as-ztriple (x)
  (declare (xargs :guard (and (integerp x)
                              (< x 0))))
  (ztriple 1 (cons (- x) 0)))

(defun integer-as-ztriple (x)
  (declare (xargs :guard (integerp x)))
  (if (< x 0)
      (negative-int-as-ztriple x)
    x))

(defun numerator-as-ztriple (x)
  (declare (xargs :guard (rationalp x)))
  (integer-as-ztriple (numerator x)))

(defun ratio-as-ztriple (x)
  (declare (xargs :guard (and (rationalp x)
                              (not (integerp x)))))
  (ztriple 2 (cons (numerator-as-ztriple x) (denominator x))))

(defun complex-as-ztriple (x)
  (declare (xargs :guard (and (complex-rationalp x)
                              (not (rationalp x)))))
  (ztriple 3 (cons (realpart x) (imagpart x))))

(defun character-as-ztriple (x)
  (declare (xargs :guard (characterp x)))
  (ztriple 4 (cons (char-code x) 0)))

(defun string-as-ztriple (x)
  (declare (xargs :guard (stringp x)))
  (ztriple 5 (cons (make-listp0 (coerce x 'list)) 0)))

(defun symbol-as-ztriple (x)
  (declare (xargs :guard (symbolp x)))
  (ztriple 6 (cons (string-as-ztriple (symbol-package-name x))
                   (string-as-ztriple (symbol-name x)))))

These functions are then asserted to define the encodings, as follows.

(defthmz negative-int-as-ztriple-identity
  (implies (and (integerp x)
                (< x 0))
           (equal (negative-int-as-ztriple x)
                  x)))

(defthmz integer-as-ztriple-identity
  (implies (integerp x)
           (equal (integer-as-ztriple x)
                  x)))

(defthmz ratio-as-ztriple-identity
  (implies (and (rationalp x)
                (not (integerp x)))
           (equal (ratio-as-ztriple x)
                  x)))

(defthmz complex-as-ztriple-identity
  (implies (and (complex-rationalp x)
                (not (rationalp x)))
           (equal (complex-as-ztriple x)
                  x)))

(defthmz character-as-ztriple-identity
  (implies (characterp x)
           (equal (character-as-ztriple x)
                  x)))

(defthmz string-as-ztriple-identity
  (implies (stringp x)
           (equal (string-as-ztriple x)
                  x)))

(defthmz symbol-as-ztriple-identity
  (implies (symbolp x)
           (equal (symbol-as-ztriple x)
                  x)))

The ACL2 primitives (function symbols without definitions, such as char-code and denominator can easily be defined in set theory so that the ACL2 axioms hold. For example, for a character c = {0,4,{{n},{n,0}}}, (char-code c) = n, and for any set s not of that form, (char-code s) = 0. Terminating recursive definitions present no problem, since in ZFG, they are equivalent to explicit definitions. Even acl2-count can easily be interpreted that way, notwithstanding its lack of a direct termination argument in ACL2, because the set-theoretic rank decreases when taking the car or cdr of a cons {{x},{x,y}}, namely x and y respectively.

Interpreting ACL2 theories in set theory

We have seen how the good ACL2 objects and ACL2 primitives can be defined in ZF. We have also discussed our formalization of ZFG; see zfc. In this section we sketch an argument for how to interpret an ACL2 theory in ZFG so that all hypothesis function calls are true.

We start with the following definitions.

(a) An ACL2 session is a sequence of events where every axiomatic event is admissible and every alleged theorem TH is indeed a theorem of the axiomatic events present at the introduction of TH. Note that include-book events are not part of a session; we essentially consider them to be “puffed” away.

(b) Let EZ be the encapsulate event that introduces the function, zfc. An EZ session is a defaxiom-free ACL2 session that includes EZ.

(c) The zfc props of an EZ session are its hypothesis function calls. These are as defined above, i.e., they include (zfc) and calls of zero-ary hypothesis functions generated by invocations of zsub and zfn. As noted elsewhere (see zfc), the hypothesis functions are exactly the keys of the table, zfc-table.

(d) The ZFG theory of an EZ session is the extension of ZFG by all of the following:

the axiomatic events of the session;

the comprehension and replacement schemes for the extension of the language of ZFG by the function symbols introduced in those axiomatic events; and

all zfc props of the session.

Then we claim the following.

(1) The ZFG theory of an EZ session is consistent, assuming that ZF is consistent.

(2) For every theorem event in an EZ session, if we remove all zfc props from its hypotheses then the result is a theorem of the ZFG theory of the session.

In fact (2) is trivial by (d) above. The import of (1) is that (2) is not vacuous: it is about a consistent theory. Note that (2) allows us to ignore all :props arguments of defthmz, defthmdz, and thmz forms, when considering whether one has a theorem of the ZFG theory of the session.

The proof of (1) is based on the following notion. The puffing procedure modifies an ACL2 session by eliminating all encapsulate events and exposing all local events, renaming as necessary. Note that the result is still an ACL2 session: in particular, there is no concern about functional instantiation, because the notion of ACL2 session is about theoremhood, not provability with ACL2. The ZFG puffing procedure is similar, except that every key of the zfc table is witnessed with the constant function, t. The initial ZFG session is the extension of the boot-strap by EZ. Note that every EZ session has the same theory as one extending the initial ZFG session: simply move the EZ event to be the first after the boot-strap.

Claim. Given an EZ session s1 extending the initial ZFG session, let s2 be the result of applying the ZFG puffing procedure to s1. Then s2 is consistent.

The proof is by induction on sessions. The initial EZ session is no problem, as the definitions in EZ are made explicit in zf plus global choice. As we puff, we can replace each definition with an explicit definition in ZFG; this is true even for (mutually) recursive definitions because of the measure theorem. Each defchoose can be replaced by an explicit definition too, using global choice. The result consists entirely of extensions using explicit definitions, hence preserves consistency, comprehension, and replacement.

Final remarks

Note that we have not worked out such an argument for ACL2(r) (see real).

When one uses trust tags (see defttag) in a session, then as usual, this carries is a responsibility to ensure soundness. In particular, if a partial-encapsulate event is accompanied by raw Lisp definitions, then there is a responsibility to guarantee that the implicit exported theorems hold in the ZFG theory of the session.