含塔斯基规则的经典逻辑系统的规范化与子公式性质，及一处修正
计算机科学中的逻辑
2023-04-25 v2 逻辑
摘要
本文考虑一种使用一般引入规则和一般消去规则的形式化经典逻辑。它提出了适用于该系统的“极大公式”“段”和“极大段”的定义，并给出它们的归约过程。随后证明系统中的演绎可转换为范式，即既不包含极大公式也不包含极大段的演绎，且范式演绎满足子公式性质。塔斯基规则被视作蕴含的一般引入规则。否定的一般引入规则具有类似形式。以蕴含或否定为主算子的极大公式需要比直觉主义逻辑规范化中更为复杂的归约过程。文末添加的修正纠正了一个错误：定理2是错误的，由其导出的一个推论以及因同一错误得出的另一个推论也是错误的。幸运的是，这不影响本文的主要结果。
引用
@article{arxiv.2108.03939,
title = {Normalisation and Subformula Property for a System of Classical Logic with Tarski's Rule, and a Correction},
author = {Nils Kürbis},
journal= {arXiv preprint arXiv:2108.03939},
year = {2023}
}