I succinctly formalize the soundness and completeness of a small Hilbert system for first-order logic in the proof assistant Isabelle/HOL. The proof combines and details ideas from de Bruijn, Henkin, Herbrand, Hilbert, Hintikka, Lindenbaum, Smullyan and others in a novel way, and I use a declarative style, custom notation and proof automation to obtain a readable formalization. The formalized definitions of Hintikka sets and Herbrand structures allow open and closed formulas to be treated uniformly, making free variables a non-concern. This paper collects important techniques in mathematical logic in a way suited for both study and further work.
@InProceedings{from:LIPIcs.TYPES.2021.8, author = {From, Asta Halkj{\ae}r}, title = {{A Succinct Formalization of the Completeness of First-Order Logic}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {8:1--8:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.8}, URN = {urn:nbn:de:0030-drops-167771}, doi = {10.4230/LIPIcs.TYPES.2021.8}, annote = {Keywords: First-Order Logic, Completeness, Isabelle/HOL} }
Feedback for Dagstuhl Publishing