Parametric mixed sequent calculus

TL;DR

This paper introduces a propositional sequent calculus combining classical and intuitionistic logic, proves cut-elimination, and explores its relation to linear logic, advancing the understanding of logical systems integration.

Contribution

It presents a novel mixed sequent calculus unifying classical and intuitionistic logics with proven cut-elimination and links to linear logic.

Findings

Cut-elimination theorem established

System contains disjoint copies of classical and intuitionistic logics

Relation to linear logic demonstrated

Abstract

In this paper, we present a propositional sequent calculus containing disjoint copies of classical and intuitionistic logics. We prove a cut-elimination theorem and we establish a relation between this system and linear logic.