Right Weakening and Right Contraction in LK
Sachio Hirokawa
Laboratory of Computer Science,
Kyushu University,
Ropponmatsu 4-2-1, Fukuoka 810, JAPAN.
hirokawa@rc.kyushu-u.ac.jp
Abstract
Gentzen's sequent calculus has two kinds of inference rules -- the
logical rules and the structural rules. There are three kinds of
structural rules -- the exchange rule, the weakening rule and the
contraction rule on both sides of a sequent. Logics that have some of
the left structural rules and the none of the right structural rules
determine substructural logics of intuitionistic logic LJ. If we
consider classical logic LK and its structural rules, there are
$2^4 = 16$ possible combinations of structural rules assuming the exchange
rules on both sides. This paper, however, shows that the right
weakening rule and the right contraction rule can not be separated.
Moreover it is shown that if a logic contains both, it contains the
right weakening rule and the right contraction rule. Thus the
weakening rule and the contraction rule have different features on the
left and on the right of a sequent. It follows that the set of
provable formulas in any such substructural logic of LK is identical
to that of either LK, LJ, BCK-logic, relevant logic R or linear logic.
Conference Home Page