HOST rationale

Why Higher Order Logic? This is just a matter of pragmatics. Its just easier to work formally with set theory if it is axiomatised in a suitable higher order logic. Avoids the need for metavariables, the variables available in HOL suffice. The Polymorphism provided by HOL (or similar) is a practical necessity. Its handy to have the operators (such as set union) as values in the domain of discourse (if not in the universe of sets). HOL provides a nice framework in which to conduct semantic embeddings of special notations.

Why Set Theory? Because engineering mathematics is classical. Because applications of mathematics are the aim and the economic engine of the proposed system. Because proof theoretic strength is what matters, and set theory has it. If it ain't broke, don't fix it.

Why Reflection? To support efficient encoding of systematic methods. To provide a sound framework in which proof obligations arising from the use of efficient algorithms can be deferred.

HOST is a Mathematical Foundation System, What is a "Foundation" for Mathematics?
HOST features	HOST Pedigree	HOST Implementation Features

© created 1996/10/9 modified 1997/12/8