## Cut elimination, identity elimination, and interpolation in super-Belnap logics. (arXiv:1803.03822v1 [math.LO])

We develop a Gentzen-style proof theory for super-Belnap logics (extensions
of the four-valued Dunn-Belnap logic), expanding on an approach initiated by
Pynko. We show that just like substructural logics may be understood
proof-theoretically as logics which relax the structural rules of classical
logic but keep its logical rules as well as the rules of Identity and Cut,
super-Belnap logics may be seen as logics which relax Identity and Cut but keep
the logical rules as well as the structural rules of classical logic. A
generalization of the cut elimination theorem for classical propositional logic
is then proved and used to establish interpolation for various super-Belnap
logics. In particular, we obtain an alternative syntactic proof of a refinement
of the Craig interpolation theorem for classical propositional logic discovered
recently by Milne.查看全文