# 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.