Formalizing the Independence of Propositional Logic Axiom System in Coq

The development of computer science has promoted the formalization of mathematical theorem proofs, making it especially crucial to use machine verification for the reliability of mathematical theorems. In this paper, we use the Coq interactive theorem prover to formalize the propositional formulas, axiom system, and axiom independence of propositional logic. We use arithmetic interpretation to prove the independence of each set of axiom patterns, and then accurately verify the independence of the axiom system, which is an important logical property. The formal verification method given in this paper is helpful to verify whether the axiom system of propositional logic is independent, meanwhile, the semantics of the formula are given by Coq, which is helpful for the development of propositional logic in the engineering direction of digital circuit design.