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

TL;DR

This paper develops proof systems for the logics of evidence and truth, proving normalization and cut-elimination theorems, which lead to decidability results for these extended non-classical logics.

Contribution

It introduces natural deduction and sequent calculi for LETJ and LETF, extending Nelson's logic N and FDE with a classicality operator, and proves key proof-theoretic properties.

Findings

Normalization and cut-elimination theorems established for both logics

Decidability of LETJ and LETF proved as a consequence

Proof systems facilitate further analysis of evidence and truth logics

Abstract

In this paper, we investigate proof-theoretic aspects of the logics of evidence and truth LETJ and LETF. These logics extend, respectively, Nelson's logic N and the logic of first-degree entailment FDE, also known as Belnap-Dunn four-valued logic, with a classicality operator that recovers classical logic for formulas in its scope. We will present natural deduction and sequent systems for LETJ and LETF, together with proofs of normalization and cut-elimination theorems, respectively. As a corollary, we obtain decidability for both logics.