Completeness Theorems for Variations of Higher-Order Logic

Add to your list(s) Download to your calendar using vCal

• Andrei Popescu (University of Sheffield)
• Thursday 15 May 2025, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

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=SELTNkOcfVrIE1IppYCsbooOVqenzI.1

Meeting ID: 871 4336 5195

Passcode: 541180

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.