A cut-free Gentzen formulation of basic propositional calculus
Journal of Logic, Language and Information 12 (2):213-225 (2003)
| Abstract | We introduce a Gentzen style formulation of Basic Propositional Calculus(BPC), the logic that is interpreted in Kripke models similarly tointuitionistic logic except that the accessibility relation of eachmodel is not necessarily reflexive. The formulation is presented as adual-context style system, in which the left hand side of a sequent isdivided into two parts. Giving an interpretation of the sequents inKripke models, we show the soundness and completeness of the system withrespect to the class of Kripke models. The cut-elimination theorem isproved in a syntactic way by modifying Gentzen's method. Thisdual-context style system exemplifies the effectiveness of dual-contextformulation in formalizing various non-classical logics. | |||||||||
| 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,679 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesAndreja Prijatelj (1996). Bounded Contraction and Gentzen-Style Formulation of Łukasiewicz Logics. Studia Logica 57 (2-3):437 - 456.
Matthias Baaz & Rosalie Iemhoff (2006). Gentzen Calculi for the Existence Predicate. Studia Logica 82 (1):7 - 23.
Grigori Mints (1997). Indexed Systems of Sequents and Cut-Elimination. Journal of Philosophical Logic 26 (6):671-696.
Francesco Belardinelli, Peter Jipsen & Hiroakira Ono (2004). Algebraic Aspects of Cut Elimination. Studia Logica 77 (2):209 - 240.
Brian Hill & Francesca Poggiolesi (2010). A Contraction-Free and Cut-Free Sequent Calculus for Propositional Dynamic Logic. Studia Logica 94 (1).
Tsutomu Hosoi (1988). Gentzen-Type Formulation of the Prepositional Logic LQ. Studia Logica 47 (1):41 - 48.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Branislav 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.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads3 ( #201,837 of 549,070 )Recent downloads (6 months)1 ( #63,185 of 549,070 )How can I increase my downloads? |
My notes
Discussion
