Formalizing the Equivalence of Formal Systems in Propositional Logic in Coq

In the field of artificial intelligence, propositional logic provides a precise and efficient reasoning structure for computers to simulate human thought. Axiom systems and natural deduction systems represent two distinct formal systems within propositional logic. The equivalence between axiom systems and natural deduction systems plays a crucial role in maintaining the consistency of the reasoning systems, ensuring the accuracy and validity of the reasoning process and simplying the proof process of theorems. This paper utilizes the Coq interactive theorem prover to formalize an axiom system and a natural deduction system, with the formalization of the language and syntax of propositional logic. Additionally, it rigorously verifies specific inner theorems. In this paper, the equivalence of the two systems is verified through a detailed formal proof based on the formalized axiom system and natural deduction system in Coq, which helps to explore and leverage the advantages of these two formal systems deeply.