KnowledgeBase » SEMINAR » ID = 407

Developing Set Theory in HOL

by Paul B. Jackson
1994-1995

Most mathematicians and logicians take some set theory to be the foundation of mathematics, though many theorem proving systems (e.g. Nuprl, Coq, HOL, IMPS) have instead adopted some kind of type theory. Attractions of type theories include that they provide more structured languages of useful primitive objects to reason with, and that much trivial reasoning is taken care of by automatic type checking. Also, constructive type theories provide a way of automatically witnessing constructions in constructive mathematics.

However, type theories can be limiting and awkward to use for general-purpose mathematics, and there have been several efforts to combine features of type theories and set theories (e.g. in Isabelle and Mizar, and with the work of Howe). I'll be talking about a recent paper by Mike Gordon describing experiments in developing set theory in HOL. Gordon introduced a type of sets into HOL together with a collection of axioms. He then explored `transfer principles' that would allow theorems proved about sets to be lifted so that they also applied to HOL types, and also would allow the movement of theorems proved about types into the language of sets.

I'll try to comment on whether or not similar techniques would work in Nuprl.