应用 G"odel 辩证法解释获得 Higman 引理的构造性证明
计算机科学中的逻辑
2012-10-12 v1 离散数学
摘要
我们利用 G"odel 的辩证法解释（Dialectica interpretation）分析了 Nash-Williams 关于 Higman 引理优雅但非构造性的“最坏坏序列”证明。所得结果是一个简洁的引理构造性证明（适用于任意可判定的良拟序），其中清晰地保留了 Nash-Williams 的组合思想，并给出了一个用于在词序列中查找嵌入对的显式程序。
引用
@article{arxiv.1210.3117,
title = {Applying G\"odel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma},
author = {Thomas Powell},
journal= {arXiv preprint arXiv:1210.3117},
year = {2012}
}
备注
In Proceedings CL&C 2012, arXiv:1210.2890