HOST pedigree

Higher Order Logic
  • Bertrand Russell invents The Theory of Types [Russell08].
  • Alonzo Church invents first the lambda calculus and then his Simple Theory of Types (STT), a radically simplfied but powerful type theory.
  • Robin Milner invents a simple form of polymorphism for typed lambda cacluli in the course of implementing a proof tool for Scott's Logic for Computable Functions (LCF).
  • Mike Gordon combines Church's STT with Milner polymorphism and conservative extension features in his LCF derived implementation of HOL.

Set Theory
  • Cantor is the originator of informal modern set theory.
  • Ernst Zermelo provided the first consistent axiomatisation in 1908
  • Fraenkel adds the replacement axiom to increase the proof theoretic strength of Zermelo's system.
  • Jean Raymond Abrial elaborates ZF set theory into the Z specification language which is used with freewheeling axiomatic extension and no apparent regard for conservative extension.
Combining the paradigms
  • Carnap (for one) uses higher order set theory.
  • Liberal conservative extension added to HOL.
  • ZF/HOL.
HOST rationale
HOST is a Mathematical Foundation System,
Are Foundations Necessary?
HOST features

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