Scholarlink

We present a sequent calculus GNFL for negative free logic with definite descriptions in the classical and intuitionistic versions, with empty and nonempty domains. It is shown constructively that GNFL satisfies the cut elimination theorem and its cut-free version satisfies the subformula property.

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

Cut Elimination for Negative Free Logics with Definite Descriptions

  • 会议论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年

查看全文
  • Andrzej Indrzejczak

摘要

We present a sequent calculus GNFL for negative free logic with definite descriptions in the classical and intuitionistic versions, with empty and nonempty domains. It is shown constructively that GNFL satisfies the cut elimination theorem and its cut-free version satisfies the subformula property.