, , LK and Cutfree Proofs TeX Export

@article{citeulike:1421835, abstract = {Abstract\ \ Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional inductions. We also give a new purely inductive proof of the cut theorem for the original single cut rule in Gentzen's sequent calculus \$\$ LK \$\$ without any use of mix.}, author = {Bimb\'{o}, Katalin}, citeulike-article-id = {1421835}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/s10992-007-9048-0}, doi = {10.1007/s10992-007-9048-0}, journal = {Journal of Philosophical Logic}, keywords = {test}, posted-at = {2007-06-29 09:48:47}, priority = {1}, title = {, , LK and Cutfree Proofs}, url = {http://dx.doi.org/10.1007/s10992-007-9048-0} }

TY - JOUR ID - citeulike:1421835 L3 - citeulike-article-id:1421835 N2 - Abstract  Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional inductions. We also give a new purely inductive proof of the cut theorem for the original single cut rule in Gentzen’s sequent calculus $$ LK $$ without any use of mix. JF - Journal of Philosophical Logic TI - , , LK and Cutfree Proofs KW - test AU - Bimbó, Katalin UR - http://dx.doi.org/10.1007/s10992-007-9048-0 ER -