Indexed systems of sequents and cut-elimination
Journal of Philosophical Logic 26 (6):671-696 (1997)
| Abstract | Cut reductions are defined for a Kripke-style formulation of modal logic in terms of indexed systems of sequents. A detailed proof of the normalization (cut-elimination) theorem is given. The proof is uniform for the propositional modal systems with all combinations of reflexivity, symmetry and transitivity for the accessibility relation. Some new transformations of derivations (compared to standard sequent formulations) are needed, and some additional properties are to be checked. The display formulations of the systems considered can be presented as encodings of Kripke-style formulations. | |||||||||
| 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,664 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesGrigori Mints (2006). Cut Elimination for S4c: A Case Study. Studia Logica 82 (1):121 - 132.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Gilles Dowek & Benjamin Werner (2003). Proof Normalization Modulo. Journal of Symbolic Logic 68 (4):1289-1316.
Marco Borga (1983). On Some Proof Theoretical Properties of the Modal Logic GL. Studia Logica 42 (4):453 - 459.
Àngel J. Gil & Jordi Rebagliato (2000). Protoalgebraic Gentzen Systems and the Cut Rule. Studia Logica 65 (1):53-89.
Kentaro Kikuchi & Katsumi Sasaki (2003). A Cut-Free Gentzen Formulation of Basic Propositional Calculus. Journal of Logic, Language and Information 12 (2):213-225.
J. W. Degen (1999). Complete Infinitary Type Logics. Studia Logica 63 (1):85-119.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads14 ( #83,035 of 549,005 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
