{"id":"arxiv/2606.19761","url":"https://arxiv.org/abs/2606.19761","tags":["cs.LO","math.LO"],"score":0,"title":"Finishing Oltean's Completeness Proof in Lean 4 for Hybrid Logic $L(\\forall)$","domain":"cs.LO","source":"arxiv","authors":["Lars Warren Ericson"],"reviews":0,"subject":"cs.LO","summary":"We present a machine-checked completeness theorem, in Lean 4, for the hybrid logic $L(\\forall)$: propositional modal logic with nominals, the satisfaction-style binder $\\forall$, and the box modality. (Machine-checked completeness for basic hybrid logic, without binders, was pioneered by Asta Halkjær From in Isabelle/HOL.) We build on Alex Oltean's 2023 Lean 4 formalization, which mechanized the syntax, semantics, Hilbert-style proof system, and soundness following Blackburn's Hybrid Completeness (1998), but left completeness unfinished. Finishing it requires manufacturing fresh names at two…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-06-18","reactions":{}}