The Mathematics and Mechanics of Relating Formal Theories

Robert L. Constable
Cornell University

1997

Abstract:

These lectures sketch a formalization of several theorems from automata theory in two distinct formal theories. One theory is a constructive type theory (representative of Alf, Coq and Nuprl), and the other is a classical set theory (representative of ZF, or BG or the set theory of Mizar). The lectures will explore formal relationships between these theories. The mathematical basis for the comparison is the formal module mechanism of the Nuprl 5 proof development system. It will be possible to discuss the relative expressive power of the two theories. The lectures will also explore the structure of the module system. If time permits there will be a discussion of formalizing Aczel's embedding of a constructive fragment of the set theory into the type theory.

References

1. Peter Aczel. The type theoretic interpretation of constructive set theory. In Logic, Methodology and Philosophy of Science VII , pages 17-49. Elsevier Science Publishers B.V., 1986.
2. Robert L. Constable. Constructing and applying formal theories using the Nuprl mathematics environment. Working Material, Marktoberdorf Summer School, NATO Science Committee, 1995.
3. Robert L. Constable, Paul B. Jackson, Pavel Naumov, and Juan Uribe. Formalizing Automata Theory I: Finite Automata. Unpublished, November 1996.
4. Jason J. Hickey. Nuprl-Light: An Implementation Framework for Higher-Order Logics. Unpublished, 1997.
5. Douglas J. Howe. Importing mathematics from HOL into Nuprl. In Proceedings of The 1996 International Conference on Theorem Proving in Higher Order Logics , 1996. To appear.
6. Paul B. Jackson. Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra . PhD thesis, Cornell University, Ithaca, NY, January 1995.