公理模式
此条目可参照英语维基百科相应条目来扩充。 (2022年12月29日) |
在数理逻辑里，公理模式（英语：axiom schema）广义化了公理这个概念。
公理模式是个在公理系统的语言中的一个合式公式，其中有一个以上的模式变数出现。这些模式变数属于元语言的一种，代表系统内的任一项或任一公式。这些变数通常需要有部分是自由的，亦即有些不出现在公式或项中的变数。
若模式变数能替换的公式或项的数目是可数无限的，此公理模式则代表了可数无限个公理。这些公理通常可以被递回地定义。若一个理论不需要使用到公理模式来公理化，则称之为“可有限公理化的”。可有限公理化的理论在元数学中被认为是较为重要的，即使这些理论在推导工作上较少有实际的用途。
公理模式两个极知名的例子为：
理查德·蒙塔古首先证明出公理模式是不可消除的，因此皮亚诺算术及ZFC集合论都是不可有限公理化的。
所有ZFC集合论里的定理也会是NBG集合论的定理，但后者很令人惊讶地，是有限公理化的。新基础集合论也可有限公理化，但重要性则较小。