Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

71 Downloads (Pure)


We formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. Our formalization precisely details the structure of this proof method.
Original languageEnglish
Title of host publicationProceedings of the ESSLLI & WeSSLLI Student Session 2020
Publication date2020
Publication statusPublished - 2020
EventWeb Summer School in Logic, Language, and Information
- Virtual event
Duration: 11 Jul 202017 Jul 2020


WorkshopWeb Summer School in Logic, Language, and Information
LocationVirtual event
Internet address


  • Propositional logic
  • Henkin-style completeness
  • Isabelle/HOL

Cite this