Scholarlink

<p>First, G0-style sequent calculi for extended Belnap–Dunn and intuitionistic logics, including Nelson and Gurevich logics, are introduced. A theorem establishing the equivalence between G0- and G3-style sequent calculi for these logics is then presented, and the cut-elimination theorem for these G0-style calculi is obtained as a result. Next, natural deduction systems with general elimination rules are introduced for these logics, and a full normalization theorem for these natural deduction systems is proved. This proof is achieved using bi-directional translations between the proposed G0-style sequent calculi and the natural deduction systems with general elimination rules.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Proof Theory for Extended Belnap–Dunn and Intuitionistic Logics

  • 期刊论文

  • 发表日期：

    2025年9月8日

查看全文
  • Norihiro Kamide,
  • Sara Negri

摘要

First, G0-style sequent calculi for extended Belnap–Dunn and intuitionistic logics, including Nelson and Gurevich logics, are introduced. A theorem establishing the equivalence between G0- and G3-style sequent calculi for these logics is then presented, and the cut-elimination theorem for these G0-style calculi is obtained as a result. Next, natural deduction systems with general elimination rules are introduced for these logics, and a full normalization theorem for these natural deduction systems is proved. This proof is achieved using bi-directional translations between the proposed G0-style sequent calculi and the natural deduction systems with general elimination rules.