In mathematical logic, generalization (also universal generalization, GEN) is an inference rule of predicate calculus. It states that if <math> \vdash P(x) </math> has been derived, then <math> \vdash \forall x \, P(x) </math> can be derived.

PropertyValue
dbpprop:abstract
  • In mathematical logic, generalization (also universal generalization, GEN) is an inference rule of predicate calculus. It states that if <math> \vdash P(x) </math> has been derived, then <math> \vdash \forall x \, P(x) </math> can be derived.
  • 普遍化是谓词演算的一个推理规则，它声称： 如果 <math> \vdash P(x) </math>，則 <math> \vdash \forall x P(x) </math>。 "普遍化"可以缩写为GEN，而推理规则可以被总结为相继式 <math> P(x) \vdash \forall x P(x) </math>， 但是这引起了一个重要的限制：不能应用演绎定理（DT）于它而推导出 <math> \vdash P(x) \rightarrow \forall x P(x)</math>（注意：这个公式是错的）。 这个公式是错的，因为 x 在前提中是一个无约束的实例，在结论中是一个约束的出现，所以如果这个公式是正确的，则它的 x 的自由实例可以被任何常量（域的元素）所替代： <math> \vdash P(t) \rightarrow \forall x P(x) </math> 但这是不正确的。比如，如果 P(x) 意味着 "x 是素数" 而域是自然数集合，则 <math> \vdash P(7) \rightarrow \forall x P(x) </math> 明显不是真的，因为从它和 <math> \vdash P(7) </math>, "7 是素数"，可以通过肯定前件推出 <math> \vdash \forall x P(x) </math>, "所有自然数都是素数"，这是个矛盾，所以反证法得出这个公式是错的。 这个限制适用于证明：如果 GEN 在一个证明中应用于一个公式，从而约束了它的自由变量 x，则 DT 不能应用于这个证明中把这个公式移动到十字转门的右侧。 注意 P(x) 符号化带有自由变量 x 的开放陈述，它的真实视 x 而定，但是 <math> \vdash P(x) </math> 符号化（对于 x 的所有值）有效的一个陈述，即使它的变量 x 是自由的。GEN 应用于这种有效陈述，约束自由变量并生成 <math> \vdash \forall x P(x) </math>。 所以公式 <math> \vdash \forall x P(x) </math> 只是陈述已经被 <math> \vdash P(x) </math> 蕴涵的事情的更明确的方式。 在谓词演算中还有一个公理，它声称 <math> \vdash \forall x P(x) \rightarrow P(x) </math> 它通过演绎定理的逆定理可变换成 <math> \forall x P(x) \vdash P(x) </math>, 这意味着从 <math> \vdash \forall x P(x) </math> 可以推导 <math> \vdash P(x) </math>。把 GEN 和这个公理放在一起，你可以推出 <math> \vdash P(x) \ \equiv \ \vdash \forall x P(x) </math> 它的意义不同于 <math> P(x) \leftrightarrow \forall x P(x)</math>（注意：这个公式是错的）。 它是错误的原因是 P(x) 可以是任何偶然的（contingent）、无效的、开放公式。为了从根本上防止这种错误的公式，在谓词逻辑中这个限制被增加到 DT 上。 十字转门符号 <math> \vdash </math> 不是合式公式的一部分：严格的说它既不属于命题演算也不属于谓词演算，而可以被认为是一个"元符号"。所以，最终 <math> \vdash \forall x P(x) </math> 实际上意义不多于 <math> \vdash P(x) </math>，因为 <math> \vdash </math> 符号实际上不是公式 P(x) 的一部分；比喻来说，它只是用来"抓住"这个公式的一个"把手"。
dbpprop:hasPhotoCollection
rdfs:comment
  • In mathematical logic, generalization (also universal generalization, GEN) is an inference rule of predicate calculus. It states that if <math> \vdash P(x) </math> has been derived, then <math> \vdash \forall x \, P(x) </math> can be derived.
rdfs:label
  • Generalization (logic)
  • 普遍化
owl:sameAs
skos:subject
foaf:page
is dbpprop:disambiguates of
is dbpprop:redirect of