Normalization and cut-elimination theorems for some logics of evidence and truth

Abstract In this paper, we investigate proof-theoretic aspects of the logics of evidence and truth $LET_{J}$ and $LET_{F}$. These logics extend, respectively, Nelson’s logic N4 and the logic of first-degree entailment, also known as Belnap–Dunn four-valued logic, with a classicality operator ${{\circ }}$ that recovers classical logic for formulas in its scope. We will present natural deduction and sequent systems for $LET_{J}$ and $LET_{F}$, together with proofs of normalization and cut-elimination theorems, respectively. As a corollary, we obtain decision procedures, which guarantees bottom-up proof search for both logics.