Tarski 的 E_2 欧几里得几何学一阶公理系统 E_2 以其完整性和可判定性而著称。 然而,毕达哥拉斯定理 - 无论是在其现代代数形式 a^2+b^2=c^2 还是在欧几里德的元素中 - 都不能直接用E_2表示,因为距离和面积都不是E_2语言中的原始概念。 在本文中,我们引入了一种双排序语言的替代公理系统 E_d ,它以双位距离函数 d 作为唯一的几何原语。 我们还介绍了它的保守扩展E_da,其中还包含一个三位角函数a。 该系统 E_d 有两个显著特征:它简单(具有单一的几何原始),并且是定量的。 数值距离可以用这种语言直接表达。 相似性公理在 E_d 中起着核心作用,用一块石头有效地杀死两只鸟:它为比例和相似性理论提供了严谨的基础,它暗示了欧几里德的平行姿势(EPP)。 相似性公理可以看作是EPP的定量表述。 毕达哥拉斯定理和相似性理论的其他定量结果可以直接用E_d和E_da的语言表达,激励了Quantitative Euclidean Geometry的名称。 传统的分析几何学可以在E_d的合成几何学下统一。 也就是说,解析几何学不被视为E_d的模型,而是其语句可以用E_d的语言表示为一阶形式句子。 系统 E_d 被证明是一致、完整和可决定的。 最后,我们将理论扩展到高维度的双曲几何和欧几里得几何。