Abstract
The method of proof just used is powerful and rather general in its applications. However, it does not give much detailed information about proofs in the system. Also, the system which we were using was specially tailored for the purpose of proving such metatheorems. This is inconvenient, however, if one is concerned with proving object language theorems or in analyzing the various connectives individually, and so in practice one introduces a number of defined expressions. Also, the system in its pure form treats only of theoremhood whereas in practice it is much easier to work with derivability from assumptions. [If you doubt this try proving (p ⊃ q) ⊃ ((q ⊃ r) ⊃ (p ⊃ r)) with and without the deduction theorem.]
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Selected Bibliography
Our presentation in this chapter closely follows that of Gentzen’s 1934–5 papers which have been translated in the American Philosophical Quarterly 1964 and 1965. Discussions of some other related systems and further theorems can be found in Kleene, Introduction to Metamathematics, D. van Nostrand Co., Princeton, N.J., 1952, 550 pp.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1979 D. Reidel Publishing Company, Dordrecht, Holland
About this chapter
Cite this chapter
Grandy, R.E. (1979). Gentzen Systems and Constructive Completeness Proofs. In: Advanced Logic for Applications. A Pallas Paperback, vol 110. Springer, Dordrecht. https://doi.org/10.1007/978-94-010-1191-4_3
Download citation
DOI: https://doi.org/10.1007/978-94-010-1191-4_3
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-277-1034-5
Online ISBN: 978-94-010-1191-4
eBook Packages: Springer Book Archive