This is an old revision of the document!
Axioms of Classical HOL
Axiom system that is sound (but necessarily incomplete with respect to standard semantics) is the following:
- (domain 'o' has only true,false as elements)
- (congruence)
- (beta reduction)
- (selecting element from gives )
Inference rule: \[
\frac{C\ \ ; \ \ A=B} {C[A:=B]}
\] which replaces one occurrence of in with (we cannot replace variables under )