全二阶逻辑系统消去切割的构造性证明
逻辑
2016-06-22 v2 计算机科学中的逻辑
摘要
本文给出全二阶逻辑系统消去切割（cut elimination）的构造性证明，该系统吸收了结构规则并使用集合而非序列。通过使用归纳的新参数——切割权重（cutweight），避免了切割秩增长的标准问题。该技术也可应用于一阶逻辑。
引用
@article{arxiv.1606.01763,
title = {A Constructive Proof of Cut Elimination for a System of Full Second Order Logic},
author = {Sandro Skansi},
journal= {arXiv preprint arXiv:1606.01763},
year = {2016}
}
备注
This paper has been withdrawn by the author due to crucial errors noted by reviewers: no cut-elimination proof for second-order logic can be formalized in second-order arithmetic. The author's arguments are formalizable in a subsystem of Kalmar-elementary arithmetic. So the purported proof seems patently wrong