Locality for Classical Logic
Brünnler, Kai
Notre Dame J. Formal Logic, Tome 47 (2006) no. 1, p. 557-580 / Harvested from Project Euclid
In this paper we will see deductive systems for classical propositional and predicate logic in the calculus of structures. Like sequent systems, they have a cut rule which is admissible. Unlike sequent systems, they drop the restriction that rules only apply to the main connective of a formula: their rules apply anywhere deeply inside a formula. This allows to observe very clearly the symmetry between identity axiom and the cut rule. This symmetry allows to reduce the cut rule to atomic form in a way which is dual to reducing the identity axiom to atomic form. We also reduce weakening and even contraction to atomic form. This leads to inference rules that are local: they do not require the inspection of expressions of arbitrary size.
Publié le : 2006-10-14
Classification:  cut elimination,  deep inference,  locality,  03F05,  03F07
@article{1168352668,
     author = {Br\"unnler, Kai},
     title = {Locality for Classical Logic},
     journal = {Notre Dame J. Formal Logic},
     volume = {47},
     number = {1},
     year = {2006},
     pages = { 557-580},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1168352668}
}
Brünnler, Kai. Locality for Classical Logic. Notre Dame J. Formal Logic, Tome 47 (2006) no. 1, pp.  557-580. http://gdmltest.u-ga.fr/item/1168352668/