仿射几何的不可判定一阶理论

Tarski 发起了一种基于逻辑的形式几何方法，研究具有三元介于关系 ($\beta$) 和四元等距关系 ($\equiv$) 的一阶结构。Tarski 确立了包括 $(R^2,\beta,\equiv)$ 的一阶 (FO) 理论是可判定的在内的若干结果。Aiello 和 van Benthem (2002) 猜想带有单谓词的 $(R^2,\beta)$ 扩张的 FO 理论是可判定的。我们通过证明对于所有 $n>1$，$(R^2,\beta)$ 的单扩张的 FO 理论是 $\Pi^1_1$-难的，从而甚至不是算术的，来反驳这一猜想。我们还定义了一类自然且全面的几何结构类 $C$，即 $(T,\beta)$，其中 $T$ 是 $R^2$ 的子集，并证明对于 $C$ 中的每个结构 $(T,\beta)$，其单扩张类的 FO 理论是不可判定的。随后，我们考虑了带有受限单谓词（例如有限谓词）的结构 $(T,\beta)$ 的扩张类，并建立了一系列相关的不可判定性结果。除了可判定性问题外，我们还简要研究了通用 MSO 和弱通用 MSO 在 $(R^n,\beta)$ 扩张上的表达能力。虽然这些逻辑在一般情况下是不可比的，但在 $(R^n,\beta)$ 的扩张上，弱通用 MSO 的公式可以翻译为等价的通用 MSO 公式。这是发表在第 21 届 EACSL 计算机科学逻辑年会 (CSL 2012) 论文集上的一篇论文的扩展版本。