Classical Categories and Deep Inference Export

@misc{citeulike:3728513, abstract = {Deep inference is a proof-theoretic notion in which proof rules apply arbitrarily deeply inside a formula. We show that the essence of deep inference is the bifunctoriality of the connectives. We demonstrate that, when given an inequational theory that models cut-reduction, a deep inference calculus for classical logic (SKSg) is a categorical model of the classical sequent calculus LK in the sense of F\"{u}hrmann and Pym. We observe that this gives a notion of cut-reduction for derivations in SKSg, for which the usual notion of cut in SKSg is a special case. Viewing SKSg as a model of the sequent calculus uncovers new insights into the Craig interpolation lemma and intuitionistic provability.}, author = {Mckinley, Richard}, booktitle = {Proceedings of Structures and Deduction '05}, citeulike-article-id = {3728513}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.3889}, citeulike-linkout-1 = {http://www.cs.bath.ac.uk/~csprim/csl05.pdf}, comment = {via http://alessio.guglielmi.name/res/cos/}, keywords = {category-theory, classical-logic, deep-inference}, location = {Lisbon}, month = {March}, posted-at = {2008-11-30 05:25:09}, priority = {0}, title = {Classical Categories and Deep Inference}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.3889}, year = {2005} }

TY - ELEC ID - citeulike:3728513 L3 - citeulike-article-id:3728513 N2 - Deep inference is a proof-theoretic notion in which proof rules apply arbitrarily deeply inside a formula. We show that the essence of deep inference is the bifunctoriality of the connectives. We demonstrate that, when given an inequational theory that models cut-reduction, a deep inference calculus for classical logic (SKSg) is a categorical model of the classical sequent calculus LK in the sense of Führmann and Pym. We observe that this gives a notion of cut-reduction for derivations in SKSg, for which the usual notion of cut in SKSg is a special case. Viewing SKSg as a model of the sequent calculus uncovers new insights into the Craig interpolation lemma and intuitionistic provability. CY - Lisbon TI - Classical Categories and Deep Inference T2 - Proceedings of Structures and Deduction '05 KW - category-theory KW - classical-logic KW - deep-inference N1 - via http://alessio.guglielmi.name/res/cos/ AU - Mckinley, Richard PY - 2005/03// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.3889 ER -