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

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