Abstract

The paper introduces Hilbert– and Gentzen-style calculi which correspond to systems ${\mathsf{C}_{n}}$ from Gupta and Belnap [3]. Systems ${\mathsf{C}_{n}}$ were shown to be sound and complete with respect to the semantics of finite revision. Here, it is shown that Gentzen-style systems ${\mathsf{GC}_{n}}$ admit a syntactic proof of cut elimination. As a consequence, it follows that they are consistent.