Formal Proof of Meta-Theorem in First-Order Logic in Coq

Formal mathematics is a method to accurately describe and prove mathematical structures and propositions through symbols and inference rules. Formal mathematics is an important part of mathematical mechanization. This paper aims to complete the formal proof of important meta-theorems in first-order logic system within the theorem proving tool Coq. Starting from the symbols of first-order logic language, this paper formally describes the concepts of formula, proof and deduction of first-order logic, and gives the formal verification of the related properties of these concepts. On this basis, the formal proof of important meta-theorems is completed, and the simplification of formula proof sequence is finally realized. The successful verification of the meta-theorem serves as a vital step towards substantiating the validity of first-order logic formulas and culminating in the creation of a comprehensive logical framework. All the codes in this paper are verified by Coq, which fully embodies the reliability, intelligence and interactivity of mathematical theorem proving in Coq.