BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Completeness Theorems for Variations of Higher-Order Logic - Andre
 i Popescu (University of Sheffield)
DTSTART:20250522T160000Z
DTEND:20250522T170000Z
UID:TALK224869@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:Mike Gordon’s Higher-Order Logic (HOL) is one of the most im
 portant logical foundations for interactive theorem proving. The standard 
 semantics of HOL\, due to Andrew Pitts\, employs a downward closed univers
 e of sets\, and interprets HOL’s Hilbert choice operator via a\nglobal c
 hoice function on the universe.\n\nIn this talk\, I introduce a natural He
 nkin-style notion of general model corresponding to the standard models. B
 y following the Henkin route of proving completeness\, I discover an enric
 hment of HOL deduction that is sound and complete w.r.t. these general mod
 els.\nVariations of my proof also yield completeness results for weaker de
 duction systems located between standard and (fully) enriched HOL deductio
 n\, relative to less constrained models.\n\n=== Online talk ===\n\nJoin Zo
 om Meeting\nhttps://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6
 PjAmbXLO8HbY.1\n\nMeeting ID: 898 5609 1954\nPasscode: ITPtalk
LOCATION:Online\; live-streamed at MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR