Cut-Elimination Theorem for Higher-Order Classical Logic: An Intuitionistic Proof

A. G. Dragalin
Additional contact information
A. G. Dragalin: Debrecen University

A chapter in Mathematical Logic and Its Applications, 1987, pp 243-251 from Springer

Abstract: 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.

Date: 1987
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-1-4613-0897-3_16

Ordering information: This item can be ordered from
http://www.springer.com/9781461308973

DOI: 10.1007/978-1-4613-0897-3_16

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().