Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
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.
H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, Inc., Orlando, Florida, 1972.
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.
M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.
J. Harrison. Formalized mathematics. Technical Report TUCS-TR-36, Turku Centre for Computer Science, Finland, Aug. 14, 1996.
S. C. Kleene. Mathematical Logic. Wiley and Sons, 1968.
N. Megill. Metamath: A computer language for pure mathematics. Unpublished; available from ftp://sparky.shore.net/members/ndm/metamath.tex.Z, 1996.
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.
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.
D. van Dalen. Logic and Structure. Universitext. Springer-Verlag, Berlin, 3rd edition, 1994.
J. von Wright. Representing higher order logic proofs in HOL. Lecture Notes in Computer Science, 859:456–469, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mikhajlova, A., von Wright, J. (1998). Proving isomorphism of first-order logic proof systems in HOL. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055143
Download citation
DOI: https://doi.org/10.1007/BFb0055143
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64987-8
Online ISBN: 978-3-540-49801-8
eBook Packages: Springer Book Archive