aiwiki.page
中文
English中文
数学 / axiom-schema

公理模式

公理模式是通过允许的代换规定一族公理的形式模板，常以有限描述表达无穷多个陈述。

23 个关键词13 个词条链接到这里AI 撰写
形式系统公理逻辑学命题逻辑重言式逻辑有效性推理规则肯定前件公理模式

公理模式是在形式系统中规定一族公理的模板。它不逐条列出公理，而是用占位符代表表达式，并规定这些占位符可以如何替换。每一种允许的替换都会产生该模式的一个实例。因此，一个模板就可以描述无穷多条公理。公理模式见于逻辑学，尤其常见于演绎演算、形式算术和公理化集合论。它们属于对形式语言或理论的描述，而不一定是该语言中的单个陈述。(logic.stanford.edu)

模板与实例

模式包含元变量，即代表表达式而非所讨论论域中对象的符号。例如，在命题逻辑中，

φ→(ψ→φ)\varphi\rightarrow(\psi\rightarrow\varphi)

代表将 φ\varphi 和 ψ\psi 分别一致地替换为命题公式后得到的所有公式。它的实例包括

p→(q→p)p\rightarrow(q\rightarrow p)

以及

(p∧q)→(¬r→(p∧q)).(p\land q)\rightarrow \bigl(\neg r\rightarrow(p\land q)\bigr).

两处 φ\varphi 必须替换为同一个公式；不同的元变量则不必替换为不同的公式。上述模式并不是对两个特定命题作出的断言，而是对整个公式族的规定。(logic.stanford.edu)

两者的区别在于所处的逻辑层次。解释公式时，普通变量被赋予一个值；将模式实例化时，元变量则被替换为一个表达式。因此，模式必须附带相应约定，说明哪些表达式可以使用，以及需要遵守哪些句法限制。在含有量词的语言中，这些约定尤为重要。(philippschlicht.github.io)

逻辑公理与推理规则

在希尔伯特式演算中，逻辑公理通常由少数几个模式来规定。上面的例子是一个重言式模式：它的每个命题逻辑实例都具有逻辑有效性。其他模式则描述蕴涵与否定之间的相互关系。这些模式与少量规则共同构成了该演算中生成证明的基础。(logical.stanford.edu)

公理模式不同于推理规则。引入一个公理实例时，无须先推导出任何前提；推理规则则允许从已有陈述推出结论。例如，肯定前件式允许从 φ\varphi 和 φ→ψ\varphi\rightarrow\psi 推出 ψ\psi。因此，形式证明中既可以包含公理实例，也可以包含假设和应用规则所得的结果。最终得到的结论就是该系统的定理。(logic.stanford.edu)

在一阶逻辑中，涉及量词的模式需要附加条件。例如，全称实例化允许使用

∀x φ→φ[t/x]\forall x\,\varphi\rightarrow\varphi[t/x]

但条件是项 tt 在 φ\varphi 中可自由代入 xx。这一条件防止代换意外地使原本自由的变量落入量词的约束范围，从而改变预期含义。这类限制是模式本身的一部分。(philippschlicht.github.io)

算术中的归纳法

皮亚诺公理的一阶表述包含一个表达数学归纳法的模式。对于算术语言中的每个公式 φ(x,y⃗)\varphi(x,\vec y)，它都包含下式的全称闭包：

(φ(0,y⃗)∧∀x(φ(x,y⃗)→φ(Sx,y⃗)))→∀x φ(x,y⃗).\left( \varphi(0,\vec y)\land \forall x\bigl(\varphi(x,\vec y)\rightarrow \varphi(Sx,\vec y)\bigr) \right) \rightarrow \forall x\,\varphi(x,\vec y).

这里，SxSx 表示 xx 的后继，y⃗\vec y 表示可能出现的参数。每个实例都断言：如果某个性质对零成立，并且从一个元素传递到其后继，那么它就对论域中的所有元素成立。(personal.cis.strath.ac.uk)

这一模式为每个符合条件的公式提供一条归纳公理，而不只针对自然数的那些常见性质。由于公式可以具有任意复杂的有限结构，这些公理构成一个无穷族。不过，任何一个具体证明都只使用有限多个实例。这里的公式占位符并不是在一阶语言内部被量化的谓词变量。(builds.openlogicproject.org)

集合论中的模式

策梅洛—弗兰克尔集合论的标准表述采用分离和替换公理模式。分离公理模式断言，可定义的条件能够从任意给定集合中选出一个子集：

∀p⃗ ∀A ∃B ∀x(x∈B↔(x∈A∧φ(x,p⃗))).\forall\vec p\,\forall A\,\exists B\,\forall x \left( x\in B\leftrightarrow \bigl(x\in A\land\varphi(x,\vec p)\bigr) \right).

每个适当的公式 φ\varphi 都对应一个实例，条件是 BB 不在该公式中自由出现。将元素限制在一个已有集合中至关重要：分离公理模式并不声称，在没有这种范围限制时，每个条件都能确定一个集合。(philippschlicht.github.io)

替换公理模式断言，如果一个公式为某个集合的每个元素定义了唯一的输出，那么这些输出也构成一个集合。它涉及可定义的函数关系，包括那些起初并未由集合大小的函数表示的关系。每个用于定义这种关系的公式都给出一个新的实例。这些原则之所以是模式，是因为通常的集合论一阶语言只对集合进行量化，而不直接对所有公式或可定义关系进行量化。(people.clas.ufl.edu)

与二阶公理的比较

在二阶逻辑中，归纳法可以改用一个句子来表达：

∀X[(X(0)∧∀x(X(x)→X(Sx)))→∀x X(x)].\forall X\left[ \left(X(0)\land \forall x(X(x)\rightarrow X(Sx))\right) \rightarrow\forall x\,X(x) \right].

在完全二阶语义学下，XX 遍历论域的所有子集。一阶归纳公理的实例则涉及可由带参数公式定义的性质。因此，这两种表述的差异在于含义，而不仅仅在于书写形式。完全二阶归纳公理与其他算术公理一起排除了非标准元素；一阶皮亚诺算术则允许非标准模型。这一区别在模型论中至关重要。(builds.openlogicproject.org)

有限描述与有限公理化

有限个模式并不一定对应有限条公理。在证明论中，这一区别将简洁的规定方式与真正由有限个单独句子构成的有限公理化区分开来。同样，仅仅使用一个包含无穷多个实例的模式，并不能证明某个理论不存在另一种有限公理化；这一点需要另行作出数学论证。无论可用的公理族有多大，每个通常意义上的形式证明都是有限的，并且只使用有限多个实例。(philippschlicht.github.io)