Herbrand定理的矢列演算证明
逻辑
2010-07-21 v1
摘要
Herbrand定理通常被表述为Gentzen经典矢列演算中加强的Hauptsatz的一个推论。然而，中矢列仅直接给出前束范式中公式的Herbrand定理。在《证明论手册》中，Buss声称给出了该定理完整陈述的一个证明，使用矢列演算方法证明了Herbrand证明演算的完备性，但正如我们所展示的，该证明存在一个缺陷。在本注释中，我们给出了Herbrand定理在其完全一般性下的正确证明，作为LK完全切割消去定理的一个推论。主要困难在于证明，如果存在一个收缩规则前提的Herbrand证明，那么也存在其结论的Herbrand证明。我们通过证明深层收缩规则的可容许性来解决这个问题。
引用
@article{arxiv.1007.3414,
title = {A sequent calculus demonstration of Herbrand's theorem},
author = {Richard McKinley},
journal= {arXiv preprint arXiv:1007.3414},
year = {2010}
}