语义 A-翻译与超一致性蕴含经典切消
计算机科学中的逻辑
2014-01-07 v1 逻辑
摘要
我们证明，如果由重写系统定义的理论 R 是超一致的，则模 R 的经典相继式演算享有切消性质，这是一个悬而未决的问题。对于此类理论，已知在模 R 的自然演绎中证明强规范化，且在模 R 的直觉主义相继式演算中切消成立。我们首先定义了 Friedman 的 A-翻译的句法版本和语义版本，表明它保持了伪 Heyting 代数的结构，即我们的语义框架。然后，我们将理论在 A-翻译代数中的解释与其在原代数中的 A-翻译联系起来。这使得我们能够证明超一致性准则和切消定理的稳定性。
引用
@article{arxiv.1401.0998,
title = {Semantic A-translation and Super-consistency entail Classical Cut Elimination},
author = {Lisa Allali and Olivier Hermant},
journal= {arXiv preprint arXiv:1401.0998},
year = {2014}
}