The leitmotif of this book was to pursue and extend Gentzen's work in proof theory. Gentzen's research was guided by Hilbert's program. Therefore, it is likely that already his work in pure logic was inspired by the observation that the consistency of a formal system could only be obtained by scrutinizing deviation free derivations. According to Theorem 7.5.4, it suffices to find a single formula which is underivable within a formal system to establish its consistency. The obvious strategy for finding such a formula is to show that an atomic formula, which is not among the axioms of the formal system, cannot be the end-formula of any derivation. This, however, is only obvious if the derivation is deviation free.
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.
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
(2009). Epilogue. In: Proof Theory. Universitext. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69319-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-69319-2_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69318-5
Online ISBN: 978-3-540-69319-2
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)