通过希尔伯特ε算子对量词的外显定义是合流且终止的
计算机科学中的逻辑
2017-04-21 v1 逻辑
摘要
我们研究了通过希尔伯特ε算子（或ε-绑定符）消除一阶公式中的量词，遵循伯奈斯通过ε项对外显定义存在量词和全称量词符号的方法。这种消除在1939年希尔伯特-伯奈斯关于第一ε定理的证明中首次外显出现。我们认为该证明在关于这种消除方面存在一个空白，与外显定义总是终止的错误假设有关。令人惊讶的是，据我们所知，此前从未有人证明过这种消除过程的合流性或终止性。甚至关于非合流性和终止问题开放性的种种说法也在流传。我们通过一个直接的、简洁的、易于验证的证明，基于关于如何从弱正规化获得终止性的新定理，证明了这种消除过程的合流性和终止性。
引用
@article{arxiv.1611.06389,
title = {The Explicit Definition of Quantifiers via Hilbert's epsilon is Confluent and Terminating},
author = {Claus-Peter Wirth},
journal= {arXiv preprint arXiv:1611.06389},
year = {2017}
}
备注
ii+20pp