A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation Tactics

Dakai Guo () and Wensheng Yu ()
Additional contact information
Dakai Guo: Beijing Key Laboratory of Space-Ground Interconnection and Convergence, Beijing University of Posts and Telecommunications, Beijing 100876, China
Wensheng Yu: Beijing Key Laboratory of Space-Ground Interconnection and Convergence, Beijing University of Posts and Telecommunications, Beijing 100876, China

Mathematics, 2023, vol. 11, issue 11, 1-28

Abstract: The increasing significance of theorem proving-based formalization in mathematics and computer science highlights the necessity for formalizing foundational mathematical theories. In this work, we employ the Coq interactive theorem prover to methodically formalize the language, semantics, and syntax of propositional logic, a fundamental aspect of mathematical reasoning and proof construction. We construct four Hilbert-style axiom systems and a natural deduction system for propositional logic, and establish their equivalences through meticulous proofs. Moreover, we provide formal proofs for essential meta-theorems in propositional logic, including the Deduction Theorem, Soundness Theorem, Completeness Theorem, and Compactness Theorem. Importantly, we present an exhaustive formal proof of the Completeness Theorem in this paper. To bolster the proof of the Completeness Theorem, we also formalize concepts related to mappings and countability, and deliver a formal proof of the Cantor–Bernstein–Schröder theorem. Additionally, we devise automated Coq tactics explicitly designed for the propositional logic inference system delineated in this study, enabling the automatic verification of all tautologies, all internal theorems, and the majority of syntactic and semantic inferences within the system. This research contributes a versatile and reusable Coq library for propositional logic, presenting a solid foundation for numerous applications in mathematics, such as the accurate expression and verification of properties in software programs and digital circuits. This work holds particular importance in the domains of mathematical formalization, verification of software and hardware security, and in enhancing comprehension of the principles of logical reasoning.

Keywords: Coq; formalization; propositional logic; theorem proving; Hilbert-style axiom system; natural deduction system; completeness theorem; automated tactics (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2023
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/11/11/2504/pdf (application/pdf)
https://www.mdpi.com/2227-7390/11/11/2504/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:11:y:2023:i:11:p:2504-:d:1158916

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().