Technical reports

Mechanising set theory

Francisco Corella

July 1991, 217 pages

This technical report is based on a dissertation submitted June 1989 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Corpus Christi College.

DOI: 10.48456/tr-232

Abstract

Set theory is today the standard foundation of mathematics, but most proof development sysems (PDS) are based on type theory rather than set theory. This is due in part to the difficulty of reducing the rich mathematical vocabulary to the economical vocabulary of the set theory. It is known how to do this in principle, but traditional explanations of mathematical notations in set theoretic terms do not lead themselves easily to mechanical treatment.

We advocate the representation of mathematical notations in a formal system consisting of the axioms of any version of ordinary set theory, such as ZF, but within the framework of higher-order logic with λ-conversion (H.O.L.) rather than first-order logic (F.O.L.). In this system each notation can be represented by a constant, which has a higher-order type when the notation binds variables. The meaning of the notation is given by an axiom which defines the representing constant, and the correspondence between the ordinary syntax of the notation and its representation in the formal language is specified by a rewrite rule. The collection of rewrite rules comprises a rewriting system of a kind which is computationally well behaved.

The formal system is justified by the fact than set theory within H.O.L. is a conservative extension of set theory within F.O.L. Besides facilitating the representation of notations, the formal system is of interestbecause it permits the use of mathematical methods which do not seem to be available in set theory within F.O.L.

A PDS, called Watson, has been built to demonstrate this approach to the mechanization of mathematics. Watson embodies a methodology for interactive proof which provides both flexibility of use and a relative guarantee of correctness. Results and proofs can be saved, and can be perused and modified with an ordinary text editor. The user can specify his own notations as rewrite rules and adapt the mix of notations to suit the problem at hand; it is easy to switch from one set of notations to another. As a case study, Watson has been used to prove the correctness of a latch implemented as two cross-coupled nor-gates, with an approximation of time as a continuum.

Full text

PDF (9.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-232,
  author =	 {Corella, Francisco},
  title = 	 {{Mechanising set theory}},
  year = 	 1991,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-232.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-232},
  number = 	 {UCAM-CL-TR-232}
}