Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic
摘要
I formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. The formalization precisely details the structure of this proof method.