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.