Mechanizing the Godel Numbering Theory in Isabelle/HOL

Machined-assisted verification of Godel Coding formulas of PC (Propositional Calculus) formal system is investigated in this paper. Our formalization work of the Godel numbering theory is based on prime theory in the theorem prover Isabelle. First we present the formal definition of the n-th prime in Isabelle/HOL and verify the main properties of primes at the same time. Rely on this definitons a plan of Godel Coding PC has been offered. Then we provide a feasible decoding policy. Using this policy, it is shown that our method of encoding formula of PC is correct. These proofs are completely formal. Isabelle scripts of this verification are available on demand. Additionally, our work is more reliable because all preceding works are pencil and paper ones outside object logic, while ours is inside the object logic Isabelle/HOL, machine-checked and coexisting with concrete verifications. Therefore our work enriches Prime theory, Factorial theory and Exponent theory in the original HOL library. This work also gives a firmer basis for the future formal verification work of other formal systems.