Computer Laboratory

Technical reports

Merging HOL with set theory

Mike Gordon

November 1994, 40 pages

Abstract

Set theory is the standard foundation for mathematics, but the majority of general purpose mechanized proof assistants support versions of type theory (higher order logic). Examples include Alf, Automath, Coq, Ehdm, HOL, IMPS, Lambda, LEGO, Nuprl, PVS and Veritas. For many applications type theory works well and provides for specification the benefits of type-checking that are well known in programming. However, there are areas where types get in the way or seem unmotivated. Furthermore, most people with a scientific or engineering background already know set theory, whereas type theory may appear inaccessible and so be an obstacle to the uptake of proof assistants based on it. This paper describes some experiments (using HOL) in combining set theory and type theory; the aim is to get the best of both worlds in a single system. Three approaches have been tried, all based on an axiomatically specified type V of ZF-like sets: (i) HOL is used without any additions besides V; (ii) an embedding of the HOL logic into V is provided; (iii) HOL axiomatic theories are automatically translated into set-theoretic definitional theories. These approaches are illustrated with two examples: the construction of lists and a simple lemma in group theory.

Full text

PDF (1.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-353,
  author =	 {Gordon, Mike},
  title = 	 {{Merging HOL with set theory}},
  year = 	 1994,
  month = 	 nov,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-353.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-353}
}