Variations of Axioms K and S in Substructural Logics
摘要
In this paper, we discuss variations of K and S from the syntactical view of substructural logics without assuming both exchange and associativity. K and S are usually adopted as axioms on implication in Hilbert-style calculus for classical logic and intuitionistic logic. Particularly, K and S are related to weakening and contraction-like rules in sequent calculus LK and LJ. In substructural logics without the exchange rule, several variations of K and S can be considered because two types of implication exist. We present non-commutative and non-associative substructural logics with variations of K and S using Hilbert-style calculus and consider consecution calculus, which is a type of Gentzen-style calculus, algebraic semantics, the derivability of structural rules, such as contraction, exchange, and associativity, and the hierarchy.