Repository | Book | Chapter
(1987) Mathematical logic and its applications, Dordrecht, Springer.
Cut-elimination theorem for higher-order classical logic
an intuitionistic proof
A. G. Dragalin
pp. 243-251
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.
Publication details
DOI: 10.1007/978-1-4613-0897-3_16
Full citation:
Dragalin, A. G. (1987)., Cut-elimination theorem for higher-order classical logic: an intuitionistic proof, in D. G. Skordev (ed.), Mathematical logic and its applications, Dordrecht, Springer, pp. 243-251.
This document is unfortunately not available for download at the moment.