A Succinct Formalization of the Completeness of First-Order Logic

Asta Halkjær From*

*Corresponding author for this work

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

41 Downloads (Pure)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of 27th International Conference on Types for Proofs and Programs
EditorsHenning Basold, Jesper Cockx, Silvia Ghilezan
PublisherSchloß Dagstuhl
Publication date1 Aug 2022
Pages8:1-8:24
Article number8
ISBN (Electronic)9783959772549
DOIs
Publication statusPublished - 1 Aug 2022
Event27th International Conference on Types for Proofs and Programs - Virtual Event
Duration: 14 Jun 202118 Jun 2021
Conference number: 27
https://types21.liacs.nl/

Conference

Conference27th International Conference on Types for Proofs and Programs
Number27
LocationVirtual Event
Period14/06/202118/06/2021
Internet address
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume239
ISSN1868-8969

Keywords

  • Completeness
  • First-Order Logic
  • Isabelle/HOL

Fingerprint

Dive into the research topics of 'A Succinct Formalization of the Completeness of First-Order Logic'. Together they form a unique fingerprint.

Cite this