Cut-elimination for simple type theory with an axiom of choice
Journal of Symbolic Logic 64 (2):479-485 (1999)
| Abstract | We present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,865 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesBranislav R. Boričić (1986). A Cut-Free Gentzen-Type System for the Logic of the Weak Law of Excluded Middle. Studia Logica 45 (1):39 - 53.
J. W. Degen (1999). Complete Infinitary Type Logics. Studia Logica 63 (1):85-119.
Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Paul C. Gilmore (2001). An Intensional Type Theory: Motivation and Cut-Elimination. Journal of Symbolic Logic 66 (1):383-400.
Satoko Titani (1973). A Proof of the Cut-Elimination Theorem in Simple Type Theory. Journal of Symbolic Logic 38 (2):215-226.
Gilles Dowek & Benjamin Werner (2003). Proof Normalization Modulo. Journal of Symbolic Logic 68 (4):1289-1316.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads10 ( #107,683 of 556,815 )Recent downloads (6 months)1 ( #64,847 of 556,815 )How can I increase my downloads? |
My notes
Discussion
