具有一般引入与消去规则的直觉主义逻辑系统的正规化与子公式性质
逻辑
2021-10-20 v1 计算机科学中的逻辑
摘要
本文研究了 Negri 和 von Plato 提出的一种具有一般引入和消去规则的直觉主义逻辑形式化。阐述了该系统的哲学重要性。给出了适用于该系统的“极大公式”、“段”和“极大段”的定义，并给出了针对极大公式的相应归约步骤以及针对极大段的置换归约步骤。也考虑了所使用主要方法的替代方案。证明了该系统内的推导可化为正规形，且正规形推导具有子公式性质。
引用
@article{arxiv.2110.09921,
title = {Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules},
author = {Nils Kürbis},
journal= {arXiv preprint arXiv:2110.09921},
year = {2021}
}
备注
arXiv admin note: substantial text overlap with arXiv:2108.03939