Abstract
It is not difficult to see that usual inductive cut-elimination proof fails for higher-order logics. The cause is that the induction goes to the ruin in the case of quantifier rules in logics with the impredicative comprehension shema. In fact, it follows from one Takeuti’s result, that finite proof of cut-elimination is impossible in this case (see, for example,[I], chapter 5, point 4). At the end of sixties some nonelementary set-theoretical proofs was worked out for higher-order logics by Tait, Prawitz, Takahasi, Girard (see [2] and [3] for the further information). Especially remarkable success was reached in the case of higher-order intuitionistic logic, where owing to Girard’s invention developed by Prawitz, Martin-Löf et al. there is an intuitionistic proof of the cut elimination result.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A.G. Dragalin, Mathematical intuitionism. Introduction to proof theory in Russian, Nauka pbl., Moscow, 1979.
Takahashi Moto-o, A system of simple type theory of Gentzen style with inference of extensionality and cut-elimination in it, Comment, math. Univ. St. Pauli, I970, I8, p. I29–I47.
Takahashi Moto-o, Cut-elimination theorem and Brouweri-an-valued models for intuitionistic type theory, Comment, math. Univ. St. Pauli, I970, I9, p. 55–72.
H. Rasiowa, R. Sikorski, The Mathematics of Metamathematics, second ed., PWN pbl., Warszawa, I968.
A.G. Dragalin, A completeness theorem for higher-order intuitionistic logic. An intuitionistic proof, this volume.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1987 Plenum Press, New York
About this chapter
Cite this chapter
Dragalin, A.G. (1987). Cut-Elimination Theorem for Higher-Order Classical Logic: An Intuitionistic Proof. In: Skordev, D.G. (eds) Mathematical Logic and Its Applications. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-0897-3_16
Download citation
DOI: https://doi.org/10.1007/978-1-4613-0897-3_16
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4612-8234-1
Online ISBN: 978-1-4613-0897-3
eBook Packages: Springer Book Archive