公理化方法

公理化方法先指定研究对象和若干不在该理论内部继续证明的起点，再用清楚的推理规则推出定理。定义给术语定界，公理规定起点，定理是从起点推出来的结论；三者在文本中承担不同工作。公理是否适合描述现实空间，还要由所选模型或经验判断，不能由证明形式单独决定。

用一个小模型看公理能说到哪里

设研究对象有“点”和“线”，只要求：

1. 任意两个不同的点恰好同处一条线；
2. 每条线恰好含两个点。

取点 $A,B,C$，线为 $AB,AC,BC$（这里 $AB$ 表示只含 $A,B$ 的线）。任意不同两点都有唯一对应线，每条线也恰好两点，所以这是一个满足两条要求的模型。

再取四个点 $A,B,C,D$，为每一对不同的点各设一条只含这两点的线，共 $(\genfrac{}{}{0ex}{}{4}{2})=6$ 条。这个模型也满足同样两条要求。两套模型里分别有 3 点和 4 点，故“恰好有三个点”不可能由这两条公理推出：若真能推出，它必须在每个满足公理的模型中都成立，四点模型却使它为假。图中每一条短线代表一个两点集合，不是说日常平面直线只有两个位置。

相同的两条公理允许点数不同的模型，不能单靠它们证明点数恰好为三。

上面建立的是相对于通常集合运算的具体模型，因此也给出这两条简单公理可共同满足的理由；它不表示不借助任何背景理论就证明了自己的绝对无矛盾性。用模型指出某结论不能由公理推出，与在公理内证明一个结论，是两种互补的检查。

希尔伯特的几何工作

希尔伯特在 Grundlagen der Geometrie（1899，常译《几何基础》）中把几何的基础关系分组列出：点、线、面之间的关联，点之间的顺序，平行，线段与角的合同，以及连续性。不同年代的版本对具体条目与编号有调整；阅读时应看每组公理实际说了什么，而不把条数当作核心。它的目的之一，是让证明中曾被图形直观默许的条件可以被明确查找。

例如画一张三角形能帮助猜测内角关系，却不能替代“任意符合前提的三角形都成立”的推导；在欧氏几何的定理链里，使用平行公设的结论会依赖所选几何背景。皮亚诺公理对自然数的后继与归纳作类似的基础刻画；公理化不是只在几何才有。

定理与模型的两次检查

一项数学主张要先问可推导吗：前提是哪些公理、定义、先前定理？推理步骤是否有效？再问适用于眼前对象吗：现实图形或模型是否满足这些前提？如果换了背景结构，即使同一串推理仍然有效，所证明的条件命题也未必在新对象上给出想要的结论。沿数学推理与证明学习这些区分，再读具体几何定理会更容易定位辅助线与隐藏前提。

参考资料

• David Hilbert，《The Foundations of Geometry》英译本，原始著作。
• MIT《Mathematics for Computer Science》，公理化方法与证明。