能否设计几何引擎？论仿射欧几里得几何的可判定性
符号计算
2018-06-04 v3
摘要
我们综述了欧几里得几何各种公理化中推论关系的可判定性现状。我们提请注意 Martin Ziegler 于 1980 年得出的一则被广泛忽视的结果，该结果证明了 Tarski 关于域的有限公理化理论不可判定的猜想。我们详述如何利用 Ziegler 定理证明希尔伯特平面和欧几里得平面的一阶理论的推论关系不可判定。作为新结果我们补充：(A) 吴文俊正交与度量几何（吴文俊，1984）以及折纸几何公理化（J. Justin 1986, H. Huzita 1991）的一阶推论关系不可判定。已知希尔伯特平面的泛理论和吴氏正交几何的泛理论是可判定的。我们在此使用初等模型论工具证明：(B) 任何与实数解析几何一致的帕普斯平面几何理论 的泛一阶推论是可判定的。
引用
@article{arxiv.1712.07474,
title = {Can one design a geometry engine? On the (un)decidability of affine Euclidean geometries},
author = {J. A. Makowsky},
journal= {arXiv preprint arXiv:1712.07474},
year = {2018}
}
备注
28 pages, revised version, May 25, 2018