ISSN 1519-9681

ARTICLES
EDITORIAL BOARD
RULES AND INSTRUCTIONS
SITES POINTING TO CLE e-PRINTS

Articles
Vol. 14(1), 2014

..
.



Vol. 15(6), 2015
Cuts and cut-elimination for complementary classical logic
Walter Carnielli (1) and Gabriele Pulcini (2)

(1) CLE and Department of Philosophy - State University of Campinas
(2) CLE post-doctoral researcher, State University of Campinas


Date Posted: October 21, 2015

Revised Version - February 24th, 2016  

vol. 15, n. 6, 2015

   
Abstract:

This paper introduces LK, a cut-free sequent calculus able to faithfully characterize classical (propositional) non-theorems, in the sense that a formula a is provable in LK if, and only if, a is not provable in LK (i.e. a is not a tautology) [Tiomkin(1988), Bonatti(1993)]. This calculus is enriched with a set of admissible cut rules, which provide a cut-elimination algorithm. The calculus is also proved to be strong normalizing and strongly confluent.



|   Home   | 2014  |  2013 2012  |  2011   |   2010   |   2009   |   2008   |   2007   |    2005   |   2004   |   2003   |   2002   |   2001   |

2001-2015 - Centre for Logic, Epistemology and the History of Science – CLE