On the unity of logic (Q685059)

This is a drastic extension of the author's previous work [Math. Struct. Comput. Sci. 1, No. 3, 255-296 (1991; Zbl 0752.03027)]. A single cut-free Gentzen-type system unifying classical, intuitionistic and linear logic is devised. The list of rules takes four pages, but the system is not a mechanical mixture of known systems for sublogics. The unifying element is the translation of stronger systems into linear logic, which underlines the notion of polarity, but is not explicitly present in the system.