On non-eliminability of the cut rule and the roles of associativity and distributivity in non-commutative substructural logics

Details On non-eliminability of the cut rule and the roles of associativity and distributivity in non-commutative substructural logics On non-eliminability of the cut rule and the roles of associativity and distributivity in non-commutative substructural logics

2009-02-02

arxiv.org/abs/0902.0304v1

Mathematics

Logic

Scientific paper

We introduce a sequent calculus FL' for non-commutative substructural logic. It has at most one formula on the right side of sequent, and excludes three structural inference rules, i.e. contraction, weakening and exchange. (FL' is based on our investigations of the Gentzen-style natural deduction for non-commutative substructural logics.) FL' has the same proof strength as the standard sequent calculus FL (Full Lambek), which is the basic sequent calculus for all other substructural logics. For the standard FL, we use Ono's formulation. Although FL' and the standard FL are equivalent, there is a subtle difference in the left rule of implication. In the standard FL, two parameters $\Gamma_1$ and $\Gamma_2$(resp.), each of which is just an finite sequence of arbitrary formulas, appear on the left and right side (resp.) of a formula which is placed on the left side of the sequent on the upper left side of the left rule $\imply$ (which corresponds to $\imply'$ in FL'). On the other hand, there is no such parameter on the left side of the sequent on the upper left side in the left rule for $\imply'$ of FL'. In FL', $\Gamma_1$ is always empty, and only $\Gamma_2$ is allowed to occur in the left rule for $\imply'$. (Similar differences occur in multiplicative and additive conjunctions, and in additive disjunction.) This difference between FL' and FL matters deeply, for we are led to a construction of proof-figures in FL', which show how the associativity of multiplicative conjunction and the distributivity of multiplicative conjunction over additive disjunction are involved in the eliminations of the cut rule in those proof-figures. We specify how associativity and distributivity are related to the non-eliminability of an application of the cut rule in those proof-figures of FL'.

Affiliated with

Also associated with

No associations

Rating

On non-eliminability of the cut rule and the roles of associativity and distributivity in non-commutative substructural logics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with On non-eliminability of the cut rule and the roles of associativity and distributivity in non-commutative substructural logics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On non-eliminability of the cut rule and the roles of associativity and distributivity in non-commutative substructural logics will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-159994