The aim of this work is to perform a proof-theoretical investigation of some propositional logics underlying either finite-valued Godel logic or finite-valued Lukasiewicz logic. We define cut-free hyper- sequent calculi for logics obtained by adding either the n-contraction law or the n-weak law of excluded middle to affine intuitionistic linear logic with the linearity axiom (A→B) V (B→A). We also develop cut-free calculi for the classical counterparts of these logics. Moreover we define a hypersequent calculus for L3∩L4 in which the cut-elimination theorem holds. This calculus allows to define an alternative axiomatization of L4 making no use of the Lukasiewicz axiom.
Ciabattoni, A. (1999). Bounded contraction in systems with linearity. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1617, pp. 113–128). Springer Verlag. https://doi.org/10.1007/3-540-48754-9_13