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 )