On intuitionistic many-valued logics
Masazumi Hanazawa, Mitio Takano · Journal of the Mathematical Society of Japan · 1986
G. Gentzen introduced the notion of sequent, which consists of the antecedent and of the succedent, each of which in turn is a sequence of finite formulas, and utilizing that notion he formulated the formal system L K for the classical logic. Then by restricting sequents to ones whose succedents are sequences of at most one formula, he obtained from L K the formal system L f for the intuitionistic logic. Later, Takahashi in [3], and Rousseau in [1] independently, extended the notion of sequent to that of matrix, which consists of the 1st row, the 2nd row, • • • , and of the N7 th row, each of which in turn is a sequence of finite formulas, where Al is a natural number greater than 1, and then utilizing that notion they formulated the formal system M L K for each M -valued logic. What is obtained from the system M-LK, when we restrict matrices to ones whose M th rows or more rows are sequences of at most one formula? This paper is one answer to this problem.