Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
This conference talk presents a framework for synthetic completeness proofs in Isabelle/HOL, delivered by Asta Halkjær From from the University of Copenhagen at CPP 2025. Explore how proof assistants can be leveraged beyond one-off formalizations to create reusable frameworks for logical calculi. The presentation details the mechanization of an abstract, transfinite version of Lindenbaum's lemma used to build witnessed, maximal consistent sets for various notions of consistency. Learn about the formalized process for mechanically calculating saturated set conditions from a logic's semantics, which separates the truth lemma into semantic and syntactic components. The framework's versatility is demonstrated through instantiations with propositional, first-order, modal, and hybrid logic examples, showing how strong completeness can be mechanized even for uncountably large languages. The talk includes proof that if a formula is valid under a set of assumptions, it can be derived from a finite subset. Supplementary materials and the full article are available through provided links.
