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 talk, I introduce a natural Henkin-style notion of general model corresponding to the standard models. By following the Henkin route of proving completeness, I discover an enrichment of HOL deduction that is sound and complete w.r.t. these general models.
Variations of my proof also yield completeness results for weaker deduction systems located between standard and (fully) enriched HOL deduction, relative to less constrained models.
=== Hybrid talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqen...
Meeting ID: 871 4336 5195
Passcode: 541180