公理是在数学或逻辑理论中无需证明便被接受为起点的命题。公理与推理规则共同构成通过演绎推理推导其他命题的基础。在现代数学中，公理不必是不言自明的，也不必普遍为真；其作用是明确特定结论成立所依据的假设。因此，一个命题是否被视为公理，取决于它所处的理论及该理论的表述方式。(ocw.mit.edu)
历史发展
欧几里得的《几何原本》是公理化方法的奠基性范例。第一卷区分了定义、公设和共同概念。公设涉及几何作图与几何关系；共同概念则表达关于相等关系和量的更一般原则。例如，一条共同概念指出，与同一个量相等的量彼此相等。后续命题均由这些起始原则及此前已确立的结果推导而来。(maths.tcd.ie)
平行公设尤为重要，因为从其他几何假设推导它的尝试，最终让位于非欧几何的发展。关于平行关系的不同假设可以支撑不同的几何理论，而不只是被视为某个据称必须遵循的框架中的错误。(maths.tcd.ie)
大卫·希尔伯特提出了一种影响深远的现代公理化几何学体系。他的方法规定了被称为点、直线和平面的对象之间的关系，并明确指出哪些结论依赖于哪些假设组。这有助于将几何学的逻辑结构与对其对象的任何特定直观解释分离开来。(maths.tcd.ie)
公理、定义与定理
公理与定理的区别在于它们在理论表述中的作用：公理被接受为起始假设，而定理则通过数学证明确立。这一区别是相对的，而非命题本身固有的。在一种表述中被作为公理的命题，在另一种表述中可能由不同的起始假设推导出来。公理本身也可以作为证明的前提；称其为“未经证明”，并不意味着它们不属于该理论中可证明的命题。(ocw.mit.edu)
定义通常用于引入术语或规定表达式的含义，公理则对所讨论的对象施加条件。在结构化的研究方法中，公理也可以充当隐式定义：理论不逐一解释“点”或“直线”的含义，而是规定这些对象必须满足的关系。不同的对象集合可能满足同样的条件。(plato.stanford.edu)
“公设”常与“公理”互换使用，不过历史上的论述有时会区分两者，欧几里得就是如此。现代用法并不要求公理在直观上具有特别明显的自明性。(maths.tcd.ie)
形式公理系统
形式系统规定符号语言、公理以及允许进行推导的规则。在一阶逻辑中，公理通常是由逻辑符号以及表示理论中的关系、运算或指定对象的符号组成的语句。形式证明记录了按照指定规则进行的有限推导过程。(math.ucla.edu)
一个公理化体系可以包含有限条或无限条公理。公理模式是规定一族公理的模板，而不只是单个语句。例如，一阶皮亚诺公理体系所刻画的算术使用归纳公理模式，每个符合要求的公式都对应这个模式的一个实例。有效公理化理论的公理可以由算法生成，这一条件对于研究形式证明局限性的结果至关重要。(math.ucla.edu)
数学中的例子
公理既可以描述抽象结构，也可以为更广泛的学科提供基础。皮亚诺算术通过关于零、后继、加法、乘法和归纳的原则来描述自然数。其一阶表述区分了预期的自然数解释与满足同一组公理的其他结构。(math.ucla.edu)
在集合论中，公理化体系规定了支配集合及其隶属关系的原则。策梅洛—弗兰克尔集合论简称 ZF，是一种标准的数学基础体系；加入选择公理后便得到 ZFC。选择公理断言，对任意一族非空集合，都存在一个从每个集合中选取一个元素的函数。在假定 ZF 相容的前提下，选择公理独立于 ZF。(plato.stanford.edu)
在概率论中，标准公理要求概率非负、整个样本空间的概率为一，以及两两互不相交的事件满足可列可加性。这些公理约束了概率的赋值方式，但并未指定每个具体事件的概率。具体的概率模型会提供这些额外细节。(probabilitycourse.com)
相容性、独立性与完备性
关于公理化体系的重要问题，可以从以下三个性质加以区分：
- **相容性：**不可能同时推导出一个语句及其否定。
- **独立性：**某条公理无法由其余公理推导出来。
- **完备性：**对于理论语言中的每个语句，都能推导出该语句或其否定。(ocw.mit.edu)
模型是满足公理的数学结构，这一概念是模型论的研究对象。要证明某条公理的独立性，可以构造一个满足其他公理却不满足该公理的模型。在推理规则可靠的前提下，这样的模型表明，所考察的公理无法由其他公理推出。(maths.tcd.ie)
公理化的局限
哥德尔不完备定理揭示了相容、有效公理化且能够表达足够丰富的算术的理论所受到的限制。第一不完备定理表明，这样的理论中存在既无法证明也无法反驳的语句。第二不完备定理则表明，在满足相关技术条件时，理论无法证明由其标准的内部相容性语句所表达的自身相容性。这些结果并非不加区分地适用于所有公理系统。(plato.stanford.edu)
这种不完备性不同于一阶逻辑学的完备性。逻辑完备性意味着，凡是在给定公理的所有模型中都为真的语句，都能从这些公理形式地推导出来。不完备理论的不同模型可能对某个特定语句的真假给出不同结果；逻辑证明系统可以是完备的，而理论本身却无法判定该语句。(math.ucla.edu)