Structured Theory and the Axiom of Choice
                                 Matt Kaufmann
                                 April 6, 2005

Abstract:

Briefly put, this talk will provide a self-contained, high-level tour of two
papers:

  (1) Matt Kaufmann and J Moore, Structured Theory Development for a Mechanized
      Logic.  Journal of Automated Reasoning 26, no. 2 (2001) 161-203.
      Available at:
      http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Foundations

  (2) :DOC CONSERVATIVITY-OF-DEFCHOOSE in (the upcoming) ACL2 Release 2.9.2.

The first part of this talk will discuss the ACL2 logic as it fits into the
framework of first-order logic.  The notions of "conservative extension" and
"soundness" will be presented, and will both be shown to be critical for ACL2.
A very high-level tour of (1) will be given, providing an informal argument
that these properties are satisfied by the ACL2 logic.

The second part of this talk will introduce (2).  First, the Axiom of Choice (of
set theory) will be presented.  The critical point will be raised that the
"obvious" use of the Axiom of Choice to justify ACL2's defchoose event is
insufficient, because it does not address ACL2's induction axioms.  A
high-level guide will be provided to the proof in (2), which is a
model-theoretic forcing argument.  However, details unsuitable for a one-hour
talk will be omitted (that's a promise!).

The question will then be raised:  Should we add a function to the ground-zero
theory that is a bijection from the ACL2 universe onto the natural numbers?
Paper (2) will be shown to provide justification for such an addition.

The first part of this talk will overlap a related ACL2 seminar talk given on
10/23/03.  However, the present talk is intended to be self-contained.
Questions will be highly encouraged.

======================================================================

Feel free to ask questions for clarification!

======================================================================

(1) Structured Theory

This part of the talk addresses the question:

     What does it mean when we prove a theorem with ACL2?

It attempts to provide some intuition, by way of a high-level overview, in case
you care to read the "Structured Theory" paper for details.

Simple answer:  The theorem is a logical consequence of the definitions.

For example:

(defun foo (x) <foo-body>)
(defun bar (x) <bar-body>)
(defthm foo-bar <foo-bar-body>)

means that <foo-bar-body> is provable from two axioms:

(equal (foo x) <foo-body>)
(equal (bar x) <bar-body>)

What's missing here?  Some possibilities:

1. What does "provable" mean?
2. Need to include ground-zero theory (e.g., (car (cons x y)) = x).
3. Formulas here are to be replaced by their so-called "universal closure"s.
4. How about defchoose; why is it OK (and what does "OK" mean)?
5. How about structuring devices:  encapsulate, books, local?
6. How should we think about defaxiom?
7. Miscellaneous questions about reasoning devices used by ACL2:
   a. The whole reasoning engine (beyond our logical scope)
   b. Functional instantiation: a correct derived rule?
   c. Packages (not in the paper, but interesting).
8. How does soundness come in, and is it enough?
9. What is the logical role of induction?  The proof of a theorem may employ
   induction for user-defined function symbols, but induction axioms are
   somehow not explicit (they rarely occur explicitly in books, for example).

Basic ideas:

1. We use first-order logic.  (Enables non-standard analysis, for example,
   where second-order logic would be more problematic.)

2. The theorems of an ACL2 session should be logical consequences of the
   definitions together with all induction axioms for the function symbols of
   the session.

Problem with #2.  Imagine the following books, where <bar-body-1> and
<bar-body-2> have instances that are provably unequal.  If we include all local
events in our notion of the current underlying theory, then that theory is
inconsistent and hence the theorem foo-property is meaningless!

============================== top.lisp ==============================
(in-package "ACL2")
(defun foo (x) ...)
(local (include-book "sub1"))
(local (defthm lemma-1 ...)) ; doesn't mention bar
(local (include-book "sub2"))
(local (defthm lemma-2 ...)) ; doesn't mention bar
(defthm foo-property (... (foo ...) ...)) ; doesn't mention bar
============================== sub1.lisp ==============================
(in-package "ACL2")
(local (include-book "sub-sub1"))
(defthm lemma-1) ; doesn't mention bar
============================== sub-sub1.lisp ==============================
(in-package "ACL2")
(local (defun bar <bar-body-1>))
...
(defthm lemma-1) ; doesn't mention bar
============================== sub2.lisp ==============================
(in-package "ACL2")
(local (include-book "sub-sub2"))
(defthm lemma-2) ; doesn't mention bar
============================== sub-sub2.lisp ==============================
(in-package "ACL2")
(local (defun bar <bar-body-2>))
...
(defthm lemma-2) ; doesn't mention bar
======================================================================

But since both definitions of bar are local events, we believe the following:

(*) foo-property follows logically from the definition of foo.

The two definitions of bar are thus just auxiliary, to help us get the proof
through ACL2.  We don't want to include the local definitions in our theory, or
else it would be inconsistent.  But more than that, we really want to claim (*)
without depending on any definition of local functions.

The idea of the "Structured Theory" paper is to make sense of all this.  The
basic concepts are:

+ History: All axiomatic events (defun, defaxiom, encapsulate, defchoose) of
  the session, along with induction axioms.  Does _not_ include defthm, but
  does include the built-in "ground-zero" theory.

+ Chronology: Includes the history and also the proved theorems (defthm
  events).

Main result:  Every theorem in the chronology is a first-order consequence of
the history part of the chronology (the axioms).

Crucial concept: Conservative extension.  The idea is that even though it was
handy to introduce bar in our example above, nevertheless, from a (first-order)
logical standpoint, foo-property follows from the definition of foo, without a
logical dependence on any definition of bar.

Observation: If T1 is a conservative extension of T0 and T0 is consistent, then
T1 is consistent.  Proof by contradiction:  If T1 proves nil then T0 proves
nil.

Let T0 extend the ground-zero theory with the definition of foo, and let T1
extend T0 with the definition of bar.  T1 is a _conservative extension_ of T0
because it doesn't allow us to prove any new theorems about foo.

Definition.  Suppose T0 and T1 are sets of first-order sentences such that T0
is a subset of T1.  T1 is a _conservative extension_ of T0 if for every
first-order sentence A in the language of T0, if A is provable from T1 then A
is provable from T0.

Conservativity result: Defun, encapsulate, and defchoose events give
conservative extensions.

Corollary:  Defun, encapsulate, and defchoose events preserve consistency.

Main result: When local events are ignored, the theorems are still first-order
consequences of what's left!

Extremely brief proof sketch for conservativity result (see "Structured Theory"
paper for details):

Defun events are clearly conservative if there is no recursion, because calls
of f can be eliminated in proofs in favor of the body of f.  In the recursive
case, the termination proof allows a sort of fancy explicit definition of f
using computation trees.

Encapsulate events just weaken what would otherwise be the theory, so they are
also conservative.  (Roughly: If you can prove something in the original theory
after throwing away the local definitions using only some theorems following
from those definitions, then you could prove it just from the definitions and
hence from the original theory, by conservativity of defun.)

[Note: What we have really just shown is that the following "restriction of
conservativity" result: if T0 \subset \T1 \subset T2 and T2 is conservative
over T0, then T1 is conservative over T0.  This is simple to prove.]

Defchoose:  Second part of talk.

Final remark.  As mentioned above, the current chronology is independent of
events local to encapsulate and include-book events.  However, defpkg events
are necessarily tracked even when they are executed under a local include-book.
See :doc hidden-defpkg for more information on this point.

======================================================================

(2) Conservativity of defchoose

Here we discuss defchoose events, which are used in ACL2 to implement
quantifiers (via the defun-sk macro).

By "conservativity of defchoose" we mean that the extension of the current
theory (history) with the axiom introduced by a defchoose event is a
conservative extension.

Consider:

     (defchoose fn (bound-var) (free-var1 ... free-vark)
       body)

Example:

     (defchoose choose-x-for-p1-and-p2 (x) (y z)
       (and (p1 x y z)
            (p2 x y z)))

Axiom added:

     ACL2 !>:pf CHOOSE-X-FOR-P1-AND-P2
     (IMPLIES (AND (P1 X Y Z) (P2 X Y Z))
              (LET ((X (CHOOSE-X-FOR-P1-AND-P2 Y Z)))
                   (AND (P1 X Y Z) (P2 X Y Z))))
     ACL2 !>

Why is defchoose conservative?  Here is a vague, and flawed, argument.  The
Axiom of Choice in set theory states (in one of its many forms) that every
binary relation contains a function with the same domain.  (Think of it this
way: out of the many ordered pairs <x,y1>, <x,y2>, ... for a given x, the
function chooses a particular <x,y>.)  So, given a model for the current
theory, we can interpret CHOOSE-X-FOR-P1-AND-P2 (or any other function
introduced by defchoose) similarly to refine the relation that maps the given
list of free-vars to any suitable bound-var (or, nil if there is no suitable
bound-var).

What's wrong with this argument (other than being too terse, for example in
explaining the connection to conservativity)?

Answer: Our notion of history includes the induction axioms.  There is no
guarantee that induction holds in the resulting model, for formulas that
mention the new function symbol.

Let's slow down and attack the problem of conservativity of defchoose from a
slightly different angle.

Suppose the ground-zero theory had a function symbol assign-natp that mapped
every object to a unique natural number, i.e., with this axiom.

(ENUM)  (implies (equal (assign-natp x) (assign-natp y))
                 (equal x y))

Then each defchoose event could be eliminated in favor of an explicit
first-order definition.  For example,

     (defchoose fn bound-var (free-var) body)

can be replaced by the following definition.

     (equal (fn free-var) bound-var)
      <==>
     body &
     (forall y) (implies (< (assign-natp y) (assign-natp bound-var))
                         (let ((bound-var y))
                              (not body)))

So we have two solutions.

(A) Make assign-natp and its axiom, above, part of the ground-zero theory.

OR

(B) Prove that for any ACL2 theory, there is a conservative extension in which
    the assign-natp axiom holds (for some new function symbol, if necessary, in
    place of assign-natp).

Although (A) is easy, it makes me a bit nervous.  But I think we should do it,
because in fact we can prove (B), and hence (A) is harmless.  Any thoughts on
this?

The proof of (B) is in :doc conservativity-of-defchoose.  But here is a BOGUS
proof that is instructive, since part of this argument appears in the actual
proof.

Let ENUM be the name of the axiom displayed above.  We want to prove that ENUM
gives a conservative extension, T1, of the current theory (history), T0.
Conservativity means:

  If A is a formula in the language of T0 that is provable in T1, then A is
  provable in T0.

The contrapositive says:

  If A is a formula in the language of T0 that is not provable in T0, then A is
  not provable in T1.

Replacing A with its negation (let's say B is ~A), this becomes:

  If B is a formula in the language of T0 that is consistent with T0, then B is
  consistent with T1.

So suppose that B is a formula in the language of T0 that is consistent with
T0.  To show that B is consistent with T1, we will show that the union T1 U {B}
has a model; this is sufficient by the Soundness Theorem of first-order logic.
By the Compactness Theorem of first-order logic. it is sufficient to fix an
arbitrary finite subset T1' of T1 and show that the union T1' U {B} has a
model.  Note that T1' U {B} may be written as T0' U {ENUM, B} for some finite
subset T0' of T0.

Now since T0 U {B} has been assumed consistent, then so is its subset
T0' U {B}, which thus has a countable model, M, by the Completeness Theorem and
Lowenheim-Skolem theorems of first-order logic.  Without loss of generality,
T0' is large enough to mention natp and to contain enough axioms to guarantee
that M is infinite.  Since M is countably infinite, there is a bijection from
its universe to its elements that satisfy natp.  If we interpret ENUM by this
bijection, then we have expanded M to a model of T0' U {ENUM, B}, i.e. to a
model of our arbitrary finite subset of T1 U {B}.

What is wrong with the argument above (again, other than its being terse)?

Answer: Our notion of history includes the induction axioms.  There is no
guarantee that the model M above satisfies induction axioms that mention
assign-natp.

Remarks for those who can make sense of them.

1. Suppose that the natural numbers of M are non-standard and that the
interpretation of assign-natp maps all standard integers to themselves but does
not map any other object to itself.  Then the formula (equal (assign-natp x) x)
defines an inductive subset of the naturals that does not include all the
naturals.)

2. Note that the issue is NOT whether the Axiom of Choice holds in the
metatheory.  The argument above used the Compactness and Downward
Lowenheim-Skolem theorems to restrict consideration to countable models.

End of Remarks for those who can make sense of them.

How do we fix the flawed argument so that induction holds even for formulas
mentioning assign-natp?  The idea is to build up assign-natp as a sort of very
careful limit of finite approximations, using a technique known as
model-theoretic forcing.  A draft :doc conservativity-of-defchoose may be found
by clicking on the appropriate link on the seminar page
(http://www.cs.utexas.edu/users/moore/acl2/seminar/).  After ACL2 2.9.2 is
released, that link might go away but you can just see :doc
conservativity-of-defchoose.  The argument there is intended to be
self-contained, and if you read it and have feedback (questions or comments),
I'd be thrilled.

[end]