Normalization and cut-elimination theorems for some logics of evidence and truth
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要