直觉主义存在实例化与 Epsilon 符号

Grigori Mints

直觉主义存在实例化与 Epsilon 符号

逻辑 2012-08-16 v1 计算机科学中的逻辑

作者: Grigori Mints

摘要

本文提出了一种带有存在实例化规则的直觉主义谓词逻辑自然演绎系统，该系统使用了 Hilbert 的 $\e$ -符号。该系统相对于直觉主义谓词逻辑是保守的。我们为合适的 Kripke 语义提供了完备性证明，概述了规范化证明的方法，综述了相关工作并陈述了一些开放问题。我们的系统扩展了 A. Dragalin 和 Sh. Maehara 提出的带有 $\e$ -符号的直觉主义系统。

关键词

直觉主义谓词逻辑存在实例化 Epsilon 符号自然演绎 Kripke 语义保守性规范化

引用

@article{arxiv.1208.0861,
  title  = {Intuitionistic Existential Instantiation and Epsilon Symbol},
  author = {Grigori Mints},
  journal= {arXiv preprint arXiv:1208.0861},
  year   = {2012}
}

直觉主义存在实例化与 Epsilon 符号

摘要

关键词

引用

相关论文