Completing Gordon’s Higher-Order Logic

Mike Gordon’s Higher-Order Logic (HOL) is one of the most important logical foundations for interactive theorem proving. The standard semantics of HOL, due to Andrew Pitts, employs a downward closed universe of sets, and interprets HOL’s Hilbert choice operator via a global choice function on the universe. In this paper we fill a gap in the meta-theory of HOL: We provide a natural Henkin-style notion of general model corresponding to the standard models, and discover an enrichment of HOL deduction that we prove to be sound and complete w.r.t. these general models.