Cut elimination, identity elimination, and interpolation in super-Belnap logics

TL;DR

This paper develops a proof theory for super-Belnap logics, relaxing certain inference rules while maintaining others, and proves cut elimination and interpolation results, including a new proof of a refined Craig interpolation theorem.

Contribution

It introduces a Gentzen-style proof system for super-Belnap logics and extends cut elimination and interpolation theorems to this class of logics.

Findings

Established a generalized cut elimination theorem for super-Belnap logics.

Proved interpolation properties for various super-Belnap logics.

Provided a new syntactic proof of a refined Craig interpolation theorem.

Abstract

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.