HOST - Higher Order Set Theory

Overview:

Single powerful classical logical foundation system provides a touchstone for analytic truth.
Features
Classical set theory formalised in a polymorphic higher order logic based on the typed lambda calculus.
Rationale
Set theory gives clean semantics with logical strength, polymorphic higher order logic enables all operators to be in the domain of discourse, building on the lambda calculus gives open-ended uniform support for variable binding constructs.
Pedigree
Cantor, Zermelo and Fraenkel were the main sources of the set theory, Frege, Russell and Church contributed the predicate calculus, the type theory, and its realisation throught the lambda calculus. Robin Milner contributed the polymorphism, Mike Gordon first applied it to Church's logic.
Implementation
to adopt the LCF paradigm, with some further innovations, the most radical being the incorporation of a programming language in the logical kernel.

Features:

  • Polymorphic Higher Order Logic
  • Classical Well-Founded Set Theory

FIRST HOL:
  • take the essence of functional abstraction, the pure lambda-calculus
  • add the simplest of type systems, with a sprinkling of variables
  • add logical constants, axioms and rules as required
Now you have the polymorphic variant of Alonzo Church's Simple Theory of Types
THEN ZF:
  • define a new type SET, polymorphic in its urelements
  • axiomatise so that it is a well-founded collection of sets at least as large as the universe of Zermelo-Fraenkel

Giving a strong polymorphic higher order set theory. If the type of urelements is instantiated to a single point type the set theory is a pure set theory.

Rationale:

  • HOL for the pragmatic value of its polymorphic, higher-order, type system
  • ZF for power, flexibility, and fit with modern mathematics

WHY HOL:
  • uniform system of variables, binding, substitution
  • no need for schemas
  • diagnostic value of polymorphic types
WHY ZF:
  • ability to implement all modern mathematics as is, without change
  • flexibility to provide semantics for embedding any other language
  • high proof theoretic strength, easily further strengthened
  • intuitive semantics

Pedigree:

confluence of:
  • classical type and set theory
  • pragmatic features from computer science
type theory: the logic derives from Frege's Begriffschrift and Peano's logical notations. Russell introduced his Theory of Types to ensure consistency by eliminating vicious circles, but the same effects are achieved with much greater economy in Church's Simple Theory of Types, later improved pragmatically by Milner's polymorphism.
set theory: Cantor's creation, complete with Russell's paradox. Zermelo provides the simplest fix as an axiomatic set theory in which set abstraction is constrained to "separation". Fraenkel gives an extra ontological boost to give the power for modern mathematics through the replacement axiom, and we also adopt a variant on Grothendiek Universes.
cs pragmatics: mainly from the LCF tradition, particularly polymorphism, modularity, and techniques for defining and implementing the foundation system

Implementation:

  • evolution of LCF paradigm
  • notational genericism
  • power-kernel
LCF style proof by safe computation of theorems, evolved to emphasise proof by evaluation (as an alternative to tactical proof), context sensitive extendable proof automation, and a reflection principle.
notational genericism: flexible graphical mix-fix notations definable for each new operator introduced. Special support for semantic embedding of arbitrary formal notations, including language support for defining functions over abstract syntax datatypes and multilingual quotation conventions.
power-kernel incorporates an effective functional programming language embedded into the HOST logic with evaluation of compiled object language function definitions invoked by the kernel during rewriting. This includes arbitrary sized natural numbers and exact real arithmetic.


© RBJ created 1998/01/02 modified 1999/7/19