Abstract
The objective of the chapter is to provide a usable way to deduce logical consequences from a given theory. We adopt Gentzen calculus (other alternatives for reasoning with theories are, namely, natural deduction and tableaux, see [1, 2] and [3], respectively) inspired by the presentation in [4] and in [5] (see also [6]) and analyze how to use the calculus for reasoning with theories. After proving some technical lemmas and providing several examples, we show that the calculus is sound and, based on Hintikka sets (see [5, 7]), we also prove completeness. Then we establish in detail Gentzen’s Hauptsatz, i.e., the Cut Elimination Theorem (see [4, 8] and for more advanced topics on cut elimination see also [9,10,11]). Finally, we conclude the chapter with a constructive proof of Craig’s Interpolation Theorem (see [5, 12, 13]).
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
References
D. Prawitz, Natural Deduction. A Proof-Theoretical Study. Acta Universitatis Stockholmiensis. Stockholm Studies in Philosophy, vol. 3 (Almqvist & Wiksell, 1965)
D. van Dalen, Logic and Structure, 5th edn. (Springer, 2013)
J.L. Bell, M. Machover, A Course in Mathematical Logic (North-Holland, 1977)
A.S. Troelstra, H. Schwichtenberg, Basic Proof Theory, vol. 43, 2nd edn. (Cambridge University Press, 2000)
J. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving (Dover, 2015)
S.R. Buss, An introduction to proof theory, in Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics, vol. 137 (North-Holland, 1998), pp. 1–78
R.M. Smullyan, First-Order Logic (Springer, 1968)
G. Gentzen, The Collected Papers of Gerhard Gentzen, ed. by M.E. Szabo. Studies in Logic and the Foundations of Mathematics (North-Holland, 1969)
M. Baaz, A. Leitsch, Methods of Cut-Elimination (Springer, 2013)
A. Carbone, S. Semmes, A Graphic Apology for Symmetry and Implicitness (Oxford University Press, 2000)
T. Kowalski, H. Ono, Analytic cut and interpolation for bi-intuitionistic logic. Rev. Symb. Logic 10(2), 259–283 (2017)
W. Craig, Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Logic 22, 269–285 (1957)
S. Maehara, On the interpolation theorem of Craig. Sûgaku 12, 235–237 (1960)
J.L. Hein, Discrete Mathematics (Jones & Bartlett Publishers, 2003)
A. Sernadas, C. Sernadas, Foundations of Logic and Theory of Computation, 2nd edn. (College Publications, 2012)
W. Craig, On axiomatizability within a system. J. Symb. Logic 18, 30–32 (1953)
W. Craig, Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Logic 22, 250–268 (1957)
E.W. Beth, On Padoa’s method in the theory of definition. Indagationes Mathematicae 15, 330–339 (1953)
H. Kihara, H. Ono, Interpolation properties, Beth definability properties and amalgamation properties for substructural logics. J. Logic Comput. 20(4), 823–875 (2010)
C.C. Chang, H.J. Keisler, Model Theory (Dover, 2012)
J.R. Shoenfield, Mathematical Logic (Association for Symbolic Logic, 2001)
A. Robinson, A result on consistency and its application to the theory of definition. Indagationes Mathematicae 18, 47–58 (1956)
J. Bicarregui, T. Dimitrakos, D. Gabbay, T. Maibaum, Interpolation in practical formal development. Logic J. IGPL 9(2), 231–243 (2001)
M.P. Bonacina, M. Johansson, On interpolation in automated theorem proving. J. Autom. Reason. 54(1), 69–97 (2015)
J. Harrison, Handbook of Practical Logic and Automated Reasoning (Cambridge University Press, 2009)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Rasga, J., Sernadas, C. (2020). Reasoning with Theories. In: Decidability of Logical Theories and Their Combination. Studies in Universal Logic. Birkhäuser, Cham. https://doi.org/10.1007/978-3-030-56554-1_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-56554-1_2
Published:
Publisher Name: Birkhäuser, Cham
Print ISBN: 978-3-030-56553-4
Online ISBN: 978-3-030-56554-1
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)