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.