An Isabelle/HOL Framework for Synthetic Completeness Proofs
summary
Mechanization in Isabelle/HOL encodes a transfinite Lindenbaum construction that builds maximal consistent sets from any consistency predicate satisfying subset-closure, compactness (finite inconsistency), and witness-preservation; construction uses well‑order recursion on an infinite cardinal and choice of fresh parameters. The framework produces syntactic reflection lemmas for rules, a procedure to compute saturated set conditions from semantics, and machine‑checked strong completeness proofs for propositional, first‑order, modal and hybrid logics (artifacts available).
AI-written summary · about