弱化规则

在逻辑学和类型论中, 弱化规则是某种在语境中增加事物的规则.

1在逻辑学中

在逻辑学中, 对于命题 $A$, 它的弱化规则指如下规则:$$\frac{\Gamma ⊢C}{\Gamma ,A⊢C}$$

这也就是说, 可以给已经证明的相继式增加 $A$ 条件.

弱化规则是结构性规则的一种, 不假设弱化规则的逻辑叫相关逻辑.

2在类型论中

在类型论中, 弱化规则一般都是成立的, 它对应形式丛 ${\pi }_A:(\Gamma ,A)\to \Gamma$ 的拉回操作 ${\pi }_A^{\ast }$, 该操作又叫弱化函子. 类型论中的弱化函子的左右伴随分别是$\Sigma$ 类型和$\Pi$ 类型, 参见依值和和依值积.

术语翻译

弱化规则 • 英文 weakening rule