Charles Explorer logo
🇨🇿

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

Publikace na Filozofická fakulta |
2017

Tento text není v aktuálním jazyce dostupný. Zobrazuje se verze "en".Abstrakt

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.