Higher Order Logic (HOL) is an expressive language for
mathematical statements. It is employed by several
proof assistants used for formal verification.
We are investigating an axiomatization of HOL in a pure
equational logic S, which is a slight refinement of the
simply typed lambda calculus. This approach has the
advantage of modularity. The semantics and proof rules
of the logical constants (Boolean connectives,
quantifiers, identity) are no longer hard wired in, but
are obtained by equational axiomatization in the same
way this is done for ordinary constants. A second
advantage is the fact that all deduction is equational
deduction, which is a simple, familiar and powerful
form of mathematical reasoning. As it turns out,
treating quantifiers by equational deduction is
convenient for humans.
The talk will outline our approach and identify some
open problems. Familiarity with HOL is not required.