UP

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


UP © RBJ created 1996/10/9 modified 1997/12/8 HOME