查看“︁层化”︁的源代码

{{roughtranslation|time=2014-02-19T06:02:46+00:00}}
在数学中层化有多种用法。
==在数理逻辑中的层化==
在[[数理逻辑]]中，'''层化'''是保证一个逻辑理论存在唯一形式释义的任何一致的数到[[谓词]]符号的指派。特别是，对于[[Horn子句]]理论，我们称一个理论是层化的，当且仅当有一个层化指派 S 满足下列条件:

:(A) 如果谓词 P 是肯定的推导自谓词 Q，则 P 的层化数必定大于等于 Q 的层化数，简写为 <math>S(P) \geq S(Q)</math>。

:(B) 如果谓词 P 推导自否定的谓词 Q，则 P 的层化数必定大于 Q 的层化数，简写为 <math>S(P) > S(Q) \ </math>。

层化只保证 Horn 子句理论的唯一释义。它被[[蒯因]] (1937年)用来解决[[罗素悖论]]，它破坏了[[弗雷格]]的中心著作《[[Grundgesetze der Arithmetik]]》 (1902年)。

==在新基础中的层化==

在带有等式和成员关系的一阶逻辑的语言中，一个公式 <math>\phi</math> 对[[新基础]]和有关集合论被称为是'''层化'''的，当且仅当有一个函数 <math>\sigma</math> 以如下方式映射在 <math>\phi</math> 中出现的每个变量(考虑为一个语法单位)到一个自然数(如果所有整数都使用则运做相当良好)，<math>\phi</math> 中出现的任何原子公式 <math>x \in y</math> 满足 <math>\sigma(x)+1 = \sigma(y) \ </math> 而在 <math>\phi</math> 中出现的任何原子公式 <math>x = y</math> 满足 <math>\sigma(x) = \sigma(y) \ </math>。

显然要求只在原子公式是约束于要考虑的集合抽象 <math>\{x \mid \phi\}</math> 中的时候满足这些条件就足够了。满足这个弱条件的集合抽象被称成'''弱层化'''。

<!-- 译者对本段很疑惑 -->
[[新基础]]的层化推广到了带有更多谓词和带有项构造的语言。每个基本谓词都需要规定所需要的 <math>\sigma</math> 在(弱)层化公式中的(约束)参数上的值之间的置换(displacement)。在带有项构造的语言中，项自身需要被指派在 <math>\sigma</math> 下的值，带有它在(弱)层化公式中的每个(约束)参数上的值的固定置换。定义的项构造(可能只是含蓄的)使用描述理论来巧妙的处理:  项 <math>(\iota x.\phi) \ </math> (x 使得 <math>\phi</math>) 必须被指派在 <math>\sigma</math> 下同变量 x 同样的值。

一个公式是层化的，当且仅当有可能指派类型给在公式中出现的所有变量，以在[[新基础]]文章中描述的 TST 版本的类型论中有意义的方式。

[[Category:數理邏輯|C]]
{{logic-stub}}