Proving isomorphism of first-order logic proof systems in HOL
We prove in HOL that three proof systems for classical first-order predicate logic, the Hilbertian axiomatization, the system of natural deduction, and a variant of sequent calculus, are isomorphic. The isomorphism is in the sense that provability of a conclusion from hypotheses in one of these proof systems is equivalent to provability of this conclusion from the same hypotheses in the others. Proving isomorphism of these three proof systems allows us to guarantee that meta-logical provability properties about one of them would also hold in relation to the others. We prove the deduction, monotonicity, and compactness theorems for Hilbertian axiomatization, and the substitution theorem for the system of natural deduction. Then we show how these properties can be translated between the proof systems. Besides, by proving a theorem which states that provability in flattened sequent calculus implies provability in standard sequent calculus, we show how some meta-logical provability results about Hilbertian axiomatization and natural deduction can be translated to sequent calculus. We use higher-order logic as the metalogic for reasoning about first-order proof systems and formalize proofs in a theorem-proving environment, thereupon reducing susceptibility to errors and bringing up subtle issues which are usually overlooked when the reasoning is done in a natural language.
KeywordsInference Rule Proof System Compactness Theorem Natural Deduction Sequent Calculus
Unable to display preview. Download preview PDF.
- 1.N. G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381–392, 1972.Google Scholar
- 2.H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, Inc., Orlando, Florida, 1972.Google Scholar
- 3.J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1989.Google Scholar
- 4.M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.Google Scholar
- 5.J. Harrison. Formalized mathematics. Technical Report TUCS-TR-36, Turku Centre for Computer Science, Finland, Aug. 14, 1996.Google Scholar
- 6.S. C. Kleene. Mathematical Logic. Wiley and Sons, 1968.Google Scholar
- 7.N. Megill. Metamath: A computer language for pure mathematics. Unpublished; available from ftp://sparky.shore.net/members/ndm/metamath.tex.Z, 1996.Google Scholar
- 8.A. Mikhajlova and J. von Wright. Proving isomorphism of first-order logic proof systems in HOL. Technical Report 169, Turku Centre for Computer Science, March 1998.Google Scholar
- 9.F. Pfenning. A structural proof of cut elimination and its representation in a logical framework. Technical Report CMU-CS-94-218, Department of Computer Science, Carnegie Mellon University, Nov. 1994.Google Scholar
- 10.D. van Dalen. Logic and Structure. Universitext. Springer-Verlag, Berlin, 3rd edition, 1994.Google Scholar
- 11.J. von Wright. Representing higher order logic proofs in HOL. Lecture Notes in Computer Science, 859:456–469, 1994.Google Scholar