Open AccessExperiments with ZF Set Theory in HOL and Isabelle
Author(s) -
Sten Agerholm,
Mike Gordon
Publication year - 1995
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v2i37.19940
Subject(s) - hol , proof assistant , semantics (computer science) , set (abstract data type) , set theory , proof theory , programming language , computer science , mathematics , natural number , discrete mathematics , calculus (dental) , mathematical proof , medicine , geometry , dentistry
Most general purpose proof assistants support versions of typed higher order logic. Experience has shown that these logics are capable of representing most of the mathematical models needed in Computer Science. However, perhaps there exist applications where ZF-style set theory is more natural, or even necessary. Examples may include Scott's classical inverse-limit construction of a model of the untyped lambda-calculus (D_inf) and the semantics of parts of the Z specification notation. This paper compares the representation and use of ZF set theory within both HOL and Isabelle. The main case study is the construction of D_inf. The advantages and disadvantages of higher-order set theory versus first-order set theory are explored experimentally. This study also provides a comparison of the proof infrastructure of HOL and Isabelle.