Zfc
Integration of set theory with ACL2
This project, in community-books directory
projects/set-theory/, develops an integration of first-order set theory
with ACL2. As a result, ACL2 can be used as a theorem prover for
Zermelo-Fraenkel set theory (ZF) with choice (so, ZFC), as explained
below.
PLEASE NOTE:
- This remains work in progress as of April 2025, so substantial changes are
still possible. Links to slides used in three 1.5 hour talks that month,
together with links to videos of those talks, may be found at this
entry of the ACL2 seminar website.
- This documentation is intended to be reasonably self-contained. Basic
familiarity with ZF set theory may be helpful but is probably not
necessary.
- As discussed below, first-order set theory provides the ability to treat
functions as first-class objects. In that sense this work provides a
“higher-order” capability that is somewhat like what is provided
by apply$. However, the two approaches have different strengths.
Apply$ has the advantage of supporting lambda-bindings and also
the powerful and efficient loop$ utility. The set-theoretic approach
described here truly provides functions as first-class objects (not merely as
symbols to be applied) and is more in line with classical mathematics; in
particular it avoids the notion of tameness used with apply$.
To use ACL2 as a set-theory prover one starts with the following command,
which includes introduction of the "ZF" package used by the
set-theory books. This documentation topic displays events as though the
current-package is "ZF".
(include-book "projects/set-theory/top" :dir :system)
There is no use of trust tags (see defttag), so ACL2 support for set
theory may seem like magic, as no changes were made to ACL2 that provide such
support. How can this be?
The foundations are laid in the book base.lisp using a zero-ary
predicate, zfc. Key functions and theorems (really, axioms) are
introduced in an encapsulate event along with zfc. The theorems
have (zfc) as a hypothesis, so they trivially hold in the first pass of
the encapsulate event because the local witness to zfc is as
follows.
(local (defun zfc () nil))
This simple trick allows an encapsulate event to export interesting
theorems, that is, by introducing a zero-ary function whose local
witness returns nil, where that function serves as a hypothesis for
exported theorems. We will call such a function — for example, zfc
— a hypothesis function.
Of course, one can always use a hypothesis function to produce any sort of
theory, reasonable or not. But we claim that the theorems exported by the
encapsulate event introducing zfc are meaningful because (zfc)
can be true! This claim is the subject of a separate documentation topic; see
zfc-model; the idea is to represent each concrete ACL2 object as a set.
Thus, ACL2 natural numbers are finite ordinals, and in particular 0 is the
empty set; and cons is the ordered-pair constructor. The key thing to
understand at this point about this representation is that everything
is a set: indeed, one can get all sets by starting with the empty set and
iterating the powerset operation through the ordinals. See zfc-model.
A nice consequence of this hypothesis function approach (again: use
of a constrained zero-ary function in hypotheses, witnessed with nil), as
opposed to using defaxiom, is that everything we prove is indeed a
theorem. We still need a metatheoretic argument to justify ignoring the
(zfc) hypotheses; again, see zfc-model. Another benefit is that
unlike defaxiom, this approach does not interfere with functional
instantiation (though it's not clear as of this writing whether that is
important).
The events that are exported by the encapsulate introducing
zfc may be seen by submitting the command :pe zfc (after evaluating
the include-book form displayed above). The next section summarizes
most of those events, and is followed by sections that further explore the
integration of set theory with ACL2.
Events exported with zfc
The encapsulate event introducing zfc introduces set-theoretic
primitives along with zfc, with the following list of signatures.
(((zfc) => *)
((in * *) => *)
((pair * *) => *)
((min-in *) => *)
((union *) => *)
((omega) => *)
((powerset *) => *)
)
These are mainly as expected, but here is a summary.
- zfc: discussed above
- (in a x): set membership — a is an element of the set
x
- (pair x y): unordered pair {x,y}
- (min-in x): chooses a minimal element of non-empty x (see
below)
- (union x): union of the elements of x
- (omega): the set of natural numbers (finite ordinals)
- (powerset x): the set of all subsets of x
That encapsulate event also introduces the following key definitions.
Others are discussed in our presentation of the model; see zfc-model.
(defun-sk subset (x y) ; x is a subset of y
(forall a
(implies (in a x) (in a y))))
(defun singleton (x) ; {x}
(pair x x))
(defun union2 (x y) ; x U y
(union (pair x y)))
(defun-sk in-in (a x) ; a is an element of an element of x
(exists y (and (in a y) (in y x))))
Convenient macros defthmz, defthmdz, and thmz generate calls
of defthm, defthmd, and thm, respectively, in which
(force (zfc)) has been added as a hypothesis. These macros are used in
most of the theorems exported from the encapsulate that introduces
zfc. Here is one of those, stating that two sets are equal when they
have the same elements. (Recall that in our setting, everything is a
set.)
(defthmdz extensionality
(implies (and (subset x y)
(subset y x))
(equal (equal x y)
t)))
And here is its expansion (as seen using :trans1), where
(force? x) is a macro call expanding to (force x) if x is
either (zfc) or of the form (foo$prop) for some symbol foo, and
is x otherwise.
(defthmd extensionality
(implies (and (subset x y)
(subset y x)
(force? (zfc)))
(equal (equal x y) t)))
Here are other exported theorems. Those that pertain to the representation
of ACL2 objects as sets are omitted here; see zfc-model.
(defthm booleanp-in
(booleanp (in x y))
:rule-classes :type-prescription)
(defthmz min-in-1 ; (min-in z) picks an element of z when z is non-empty
(equal (in (min-in z) z)
(not (equal z 0))))
(defthmz min-in-2 ; (min-in z) is minimal in that it does not intersect z
(implies (in a z)
(not (in a (min-in z)))))
(defthm min-in-0 ; just a default
(equal (min-in 0) 0))
(defthmz in-pair ; the unordered pair {x,y} contains just x and y
(equal (in a (pair x y))
(or (equal a x) (equal a y))))
(defthmz in-union ; (union x) contains the elements of elements of x
(equal (in a (union x))
(in-in a x)))
(defthmz infinity ; our version of the axiom of infinity from ZF
(equal (in n (omega)) (natp n)))
(defthmz in-powerset
(equal (in a (powerset x))
(subset a x)))
(defthm 0-is-emptyset
(not (in a 0)))
All of these theorems are essentially trivial consequences of ZF, except
that the ones using min-in implement not only ZF's Axiom of Regularity
but also a form of global choice. It is well known that this puts us in a
conservative extension of ZFC (also see zfc-model).
Relations, functions, and their application
As usual, we consider a set to be a relation if it is a set of
ordered pairs; this set is a function if furthermore, there is always
at most one such y for each x. Recall that in our setting, cons is the ordered-pair constructor; thus the ordered pair of x and
y, which in set theory is generally defined as {{x},{x,y}}, is given
by (cons x y).
(defun-sk relation-p (r)
(forall p
(implies (in p r) (consp p)))
:rewrite :direct)
(defun-sk funp (f)
(forall (p1 p2)
(non-exec (and (relation-p f)
(implies (and (in p1 f)
(in p2 f)
(not (equal p1 p2)))
(not (equal (car p1) (car p2)))))))
:rewrite :direct)
We next introduce function application, (apply r x), not only for
functions but for relations. (Aside: Recall that we are working in the
"ZF" package; so here, apply refers to zf::apply, which is
different from common-lisp::apply.) The idea is that (apply r x) is
some y such that the ordered pair (cons x y) is an element of
r. The following event captures that idea.
(defchoose apply-base (y)
(r x)
(in (cons x y) r))
However, it seems convenient to provide a default for the case that x
is not in the domain of r. (We discuss formalization of domains further
below.) So we actually define function (and relation) application as
follows.
(defun apply (r x)
(declare (xargs :guard t))
(let ((y (apply-base r x)))
(if (in (cons x y) r)
y
0)))
Axiom schemes and their implementation with zsub and zfn
ZF is typically formulated not only with axioms as discussed above, but
also with two axiom schemes: Comprehension (or Subset), which asserts that
every definable subcollection of a set is a set; and Replacement, which
asserts that a definable function maps into a set. Versions of these schemes
are implemented with macros zsub and zfn, which we now discuss in
turn.
The macro zsub implements the Comprehension scheme. If name is a
new name, (v1..vn) is a formal parameters list, x is a variable, and
s and prop are terms, then (zsub name (v1..vn) x s u)
introduces a function (name v1..vn) = {x in s: u}. Here (v1..vn)
should include all variables occurring free in s or u other than
x, and must not occur in s.
Zsub is used for defining the domain of a relation. Noted above is
that cons is the ordered-pair constructor. Consider an ordered pair
<x,y> = (cons x y). But the traditional set-theoretic definition of
<x,y> is: {{x},{x,y}}. Thus for every <x,y> in a set r,
{x} is in the union of the elements of r, i.e., in (union r);
hence x is in (union (union r)). Thus, the domain of r can
be defined using Comprehension as follows.
{x in (union (union r)): (in (cons x (apply r x)) r)}
That definition is captured by the following invocation of zsub.
(zsub domain (r) ; name, args
x ; x
(union (union r)) ; s
(in (cons x (apply r x)) r) ; u
)
That form generates an encapsulate event that constrains a function
domain$prop of no arguments and a function (domain r), exporting
the following key property of domain.
(defthm domain$comprehension
(implies (force (domain$prop))
(equal (in x (domain r))
(and (in x (union (union r)))
(in (cons x (apply r x)) r)))))
This is a typical use of zsub. Many other uses may be found in the
community-books directory, projects/set-theory/.
Recall our trick of introducing a zero-ary hypothesis function,
zfc, in an encapsulate event, to use in hypotheses of theorems
exported from that encapsulate. Similarly, the use of zsub above
has introduced the zero-ary function domain$prop and used it in the
hypothesis of the key property of domain, displayed above. Our
explanation in documentation topic zfc-model provides consistent ACL2
theories in which (zfc) holds as do all hypothesis functions from
invocations of zsub and zfn. That gives us justification for
ignoring all such hypotheses in our theorems.
This observation, that we can ignore such hypothesis functions, is
supported by a keyword, :props, for the defthmz, defthmdz, and
thmz macros. The value of this keyword defaults is a list of symbols
that defaults to (zfc), but this list can also include hypothesis
functions introduced by zsub or zfn. So we could have written the
defthm event introducing domain$comprehension (above) as
follows.
(defthmz domain$comprehension
(equal (in x (domain r))
(and (in x (union (union r)))
(in (cons x (apply r x)) r)))
:props (domain$prop))
For each symbol p in the list of :props, (force? p) is added
as a hypothesis (after any existing hypotheses). The point of :props is
that if we consider our events to be about the integration of set theory and
ACL2 (see zfc-model), then we can ignore those properties because they
are all true in that integration.
Thus, each symbol in :props undergoes a check that guarantees that it
can be ignored in our intended ZFC integration. The check is that the symbol
either is zfc or is a key p of a certain table,
zfc-table. That table associates p either with an existing
zsub or zfn event introducing p as its hypothesis function, or
else with a form (and (q0) (q1) ... (qk)) where each qi is a key of
zfc-table. An event (extend-zfc-table p q0 q1 ... qk) introduces a
new zero-ary macro name, p, which expands to (and (q0) (q1)
... (qk)) and makes the above table entry. For example, the following event
introduces zify-prop, to be used further below, as the conjunction of
(prod2$prop), (domain$prop), (inverse$prop), and (zfc),
and makes a suitable note in the zfc-table.
(extend-zfc-table zify-prop
prod2$prop domain$prop inverse$prop zfc)
We turn now to the macro zfn, which implements a version of the
Replacement scheme. It will likely be used much less frequently than
zsub. The general form is (zfn fn args x y bound u). Think of
u as a property that associates some values of x in a set,
bound, with corresponding y; then fn is a function associating
each such x with a corresponding y. More precisely, u is a
term typically mentioning x and y and perhaps other variables, where
those others are all in args; then fn has formal parameters list
args and the application (fn . args) produces a set of ordered
pairs, namely a function mapping suitable x in bound to suitable
y, as described above (i.e., satisfying u). Thus, (zfn fn args x
y bound u) introduces the following axioms, each conditionalized with a
hypothesis function obtained by adding suffix "$PROP" to fn. Here
we show the special case (which is actually quite typical) that args is
(); otherwise replace (fn) below by (fn arg1 .. argk) where
args is (arg1 .. argk).
(funp (fn))
(subset (domain (fn)) bound)
(implies (and (in x bound)
u)
(in x (domain (fn))))
(implies (equal y (apply (fn) x))
u)
Let's see a use of zfn in the book base.lisp, to define a
function (as an ACL2 object) with domain the set (omega) of natural
numbers, which maps each natural number x to the value (v-map x),
as described further below.
(zfn v ; name
() ; args
x ; x
y ; y
(omega) ; bound
(equal (equal y (v-map x)) t) ; u
)
The nature of v-map isn't important here, but for those interested, we
note that for a natural number n, (v-map n) is the result of
iterating the powerset operation n times on the empty set, 0. The
definition of v-map is a typical ACL2 recursive definition, which
illustrates a cool benefit of combining ACL2 with ZF in this way: the richness
of ZF is combined with ACL2 mechanization, including induction and
recursion.
(defun v-map (n)
(declare (type (integer 0 *) n))
(if (zp n)
0
(powerset (v-map (1- n)))))
Now that we have an ACL2 object, (v), that is a function mapping each
natural number n to (v-map n), we define the union of these
(v-map n) as follows. See base.lisp for the definition of the image
of a function fn, (image fn).
(defun v-omega nil
(declare (xargs :guard t))
(union (image (v))))
Future work may introduce ordinal recursion to extend this sort of
construction through the ordinals.
Higher-order capabilities using zify and zify*
If an ACL2 function F_A is represented as a constant (F) that
denotes a function object (which is a set of ordered pairs), then (F) can
be applied to an argument s with (apply (F) s). Although that
application will not be executable, nevertheless, during a proof (apply (F)
s) might be rewritten to (F_A s), which may be executable.
We thus see that ACL2 has a sort of “higher-order” capability.
Consider the simple example of a standard mapping function.
(defun map (f lst)
(declare (xargs :guard (true-listp lst)))
(cond ((endp lst) nil)
(t (cons (apply f (car lst))
(map f (cdr lst))))))
It is easy for ACL2 to prove generic properties of map automatically,
like the following.
(defthm map-append
(equal (map f (append x y))
(append (map f x) (map f y))))
A second generic property proved automatically by ACL2 is the following,
about mapping the composition of two functions over a list. (See
base.lisp for the definition of compose using zsub and the
definition of list-to-set.)
(defthmz map-compose
(implies (and (force (funp f))
(force (funp g))
(force (subset (list-to-set lst) (domain g))))
(equal (map (compose f g) lst)
(map f (map g lst))))
:props (zfc domain$prop prod2$prop compose$prop inverse$prop))
Now suppose we want to map a given ACL2 function over a list using
map. For that, we need to create a set-theoretic function object (set of
ordered pairs) corresponding to that ACL2 function. This section uses
examples to describe the use of macros zify and zify* to create such
function objects. These examples should give a good idea of how to use these
macros, but more documentation may appear later, especially if requested by
someone who expects to use these macros. Note that the word
“zify” may be pronounced to rhyme with “reify”, which
is appropriate since zify takes an existing ACL2 function symbol and
essentially realizes (i.e., reifies) it as a set-theoretic (or ZF) function: a
set of ordered pairs. Both zify and zify* invoke zsub to
create the desired function.
Consider for example the standard definition of a Fibonacci function.
(defun fib (n)
(declare ...)
(cond ((zp n) 0)
((= n 1) 1)
(t (+ (fib (- n 1)) (fib (- n 2))))))
Evaluation of the following macro creates a zero-ary function, zfib,
which agrees with fib on the natural numbers. The :dom and
:ran arguments specify the natural numbers as the domain and
codomain (i.e., range, i.e., a set containing the image).
(zify zfib fib :dom (omega) :ran (omega))
Now ACL2 accepts the following events. The first illustrates that
evaluation can be carried out, as explained further below.
(thmz (equal (map (zfib) '(0 1 2 3 4 5 6 7))
'(0 1 1 2 3 5 8 13))
:props (zify-prop zfib$prop))
(defun map-fib (lst)
(declare (xargs :guard (nat-listp lst)))
(cond ((endp lst) nil)
(t (cons (fib (car lst))
(map-fib (cdr lst))))))
(defthmz map-zfib
(implies (nat-listp lst)
(equal (map (zfib) lst)
(map-fib lst)))
:props (zify-prop zfib$prop))
The following lemma is generated by the zify call above, and is used
by the ACL2 rewriter to replace an application of (zfib) by a
corresponding call of fib. That, in particular, supports the use of
evaluation in the proof of the first event in the display just above.
(defthmz zfib-is-fib
(implies (natp n)
(equal (apply (zfib) n)
(fib n)))
:props (zfc prod2$prop zfib$prop domain$prop))
Here is the definition of a version of another common higher-order
function, foldr.
(defun foldr (lst fn init)
(declare (xargs :guard (true-listp lst)))
(if (endp lst)
init
(apply fn
(list (car lst)
(foldr (cdr lst) fn init)))))
That definition may be found in the book foldr.lisp, which also
contains the following events. The function zcons-when-fn* is produced
by an analogue of zify, namely zify*, which is suitable for
functions of more than one argument.
(defun filter (fn lst)
(declare (xargs :guard (true-listp lst)))
(cond ((endp lst) nil)
((apply fn (car lst))
(cons (car lst) (filter fn (cdr lst))))
(t (filter fn (cdr lst)))))
(defun cons-when-fn (x y fn)
(declare (xargs :guard t))
(if (apply fn x)
(cons x y)
y))
(zify* zcons-when-fn* cons-when-fn
2 ; arity
; A function from A to B is a set of ordered pairs <a,b> where a is in A
; and b is in B, hence a subset of A X B. The domain is thus specified
; just below by the Cartesian product of (acl2) with itself, where (acl2)
; is the set of good ACL2 objects as described in the next section.
:dom (prodn (acl2) (acl2))
:params (fn)
:props (v$prop acl2$prop))
(thmz (equal (foldr '(1 4 9 16 25 36 100)
(zcons-when-fn* (zevenp))
nil)
'(4 16 36 100))
:props (foldr-prop zcons-when-fn*$prop zevenp$prop))
(thmz (implies (and (zcons-when-fn*$prop)
(acl2p lst) ; defined in the next section
)
(equal (foldr lst (zcons-when-fn* f) nil)
(filter f lst)))
:props (foldr-prop zcons-fn*$prop))
; A computation example.
(zify zevenp evenp)
(thmz (equal (foldr '(1 4 9 16 25 36 100)
(zcons-when-fn* (zevenp))
nil)
'(4 16 36 100))
:props (foldr-prop zcons-when-fn*$prop zevenp$prop))
The set of ”good” ACL2 objects
A good ACL2 object is one that is built from the usual
atoms (numbers, symbols, characters, and strings) by closing under
cons.
(defun acl2p (x)
(declare (xargs :guard t))
(cond ((consp x) (and (acl2p (car x))
(acl2p (cdr x))))
((bad-atom x) nil)
(t t)))
The set (v-omega), introduced above, is a set containing every good
ACL2 object.
(defthmz v-omega-contains-acl2p
(implies (acl2p x)
(in x (v-omega)))
:props (zfc v$prop domain$prop prod2$prop inverse$prop)
:hints (("Goal" :in-theory (enable bad-atom))))
By Comprehension we may define the set of good ACL2 objects.
(zsub acl2 () ; name, args
x ; x
(v-omega) ; s
(acl2p x) ; u
)
The book prove-acl2p.lisp defines a macro, prove-acl2p, to prove
that a given ACL2 function returns a good ACL2 object on good ACL2 inputs.
For example, the call (prove-acl2p len) generates and proves the
following theorem.
(defthm acl2p-len
(implies (acl2p x) (acl2p (len x)))
:hints (("Goal" :in-theory (enable len))))
That book then proves such a theorem for most ACL2 primitives.
It is useful that there is a set of all good ACL2 objects. An example is
given by the call (zify* zcons-when-fn* cons-when-fn ...) above.
Further remarks and results
A design goal in this project was for ACL2 to be a useful set-theory
prover. A system like Isabelle
ZF may be more foundational. For example, we took the shortcut of
introducing (omega) rather than a more traditional formulation of the
Axiom of Infinity, so that membership in (omega) would be represented by
natp.
(defthmz infinity
(equal (in n (omega))
(natp n)))
Of course ZF proves that the ordinal ω exists, which justifies the
introduction of the constant (omega) with the property displayed
above.
More significantly perhaps, we took the shortcut of using cons for
ordered pairs and consp to recognize them. So for example, destructor
elimination may be used automatically in proofs about ordered pairs. We also
identified finite ordinals with natural numbers, about which there are vast
libraries of rules and built-in linear arithmetic procedures, and of course
efficient evaluation may be performed in ACL2.
Much of the content of the books in projects/set-theory/, and even
content in the key book base.lisp in that directory, is not discussed
here. You are invited to browse those books, which may well be developed
further over time.
Subtopics
- Zfc-model
- Justification for integrating set theory with ACL2
