HOST features

Higher Order Logic Church's Simple Theory of Types Milner's LCF style polymorphism Heirarchic Theory Database Liberal conservative extension rule Proof deferment feature

Set Theory Any classical set theory will do (e.g. ZFC) Use a natural axiomatisation in higher order logic so that a single new type becomes a universe of the set theory. My preferred axiom: every set is a member of a set closed under replacement (and some other things).

Reflection This shouldn't really be here, since it doesn't need to be part of the primitive logic. I will remove it when I have adequately covered the topic elsewhere. The purpose of a reflection rule is to give computational efficiency in an LCF like proof system by enabling algorithms which are known to be sound to be applied in the derivation of theorems. The implementation of this feature would extend the dependence of the system on the correctness of the compiler used to implement the proof tool (assuming it is also used to implement the reflection principle). Of course, there are potential problems with reflection rules, vide: [Boolos93] or jrh on Metatheory and Reflection. Let HOST-r be HOST minus this reflection rule. Formalise derivability in HOST-r using HOST-r Formalise the notion that a function over conjectures is sound if its result is always derivable from its argument. Add rule permitting a theorem to be derived if it is the result of applying a sound function to a theorem.

HOST is a Mathematical Foundation System, Are Foundations Necessary?
HOST Rationale	HOST Pedigree	HOST Implementation Features

© created 1996/10/9 modified 1996/10/31