University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Completeness Theorems for Variations of Higher-Order Logic

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Completeness Theorems for Variations of Higher-Order Logic

Download to your calendar using vCal

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

CANCELLED

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.

=== Online talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk

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

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Salisbury Arms LR10, Engineering, Department of Department of Chemistry (Wolfson lecture theatre)

Other talks

Zooming in on the assembly of galaxies in the early Universe Title TBC "That's History. That's Truth. I Seen It Myself": T'tc~tsa (Wailaki) and the Enslavement of California Native Americans. The Gardens of the Western Cape CSAR lecture: 46&: Development of a probiotic that supports the natural removal of forever chemicals from the body Title TBC
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity