Saved in:
Bibliographic Details
Main Authors: Coniglio, Marcelo E., Figallo, Martín, Rodrigues, Abilio
Format: Preprint
Published: 2024
Subjects:
Online Access:https://arxiv.org/abs/2405.20932
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866916267681644544
author Coniglio, Marcelo E.
Figallo, Martín
Rodrigues, Abilio
author_facet Coniglio, Marcelo E.
Figallo, Martín
Rodrigues, Abilio
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2405_20932
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Normalization and cut-elimination theorems for some logics of evidence and truth
Coniglio, Marcelo E.
Figallo, Martín
Rodrigues, Abilio
Logic
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.
title Normalization and cut-elimination theorems for some logics of evidence and truth
topic Logic
url https://arxiv.org/abs/2405.20932