谓词抽象

在逻辑学中，谓词抽象是指从一个句子中创建一个谓词的结果。如果Q是任何公式，那么从该句子中形成的谓词抽象是(λy.Q)，其中λ是一个抽象算子，在(λy.Q)中，y的每一次出现都被λ约束。由此产生的谓词(λx.Q(x))是一个能够以术语t为参数的单数谓词，如(λx.Q(x))(t)，它表示由’t’表示的对象具有这样的属性，即Q。抽象定律指出（λx.Q(x)）(t)≡Q(t/x)，其中Q(t/x)是用t替换Q中所有自由出现的x的结果。这个定律至少在两种情况下被证明是失败的：(i)当t是无参量的，(ii)当Q包含模态操作符。

在模态逻辑中，dere/dedicto的区别被表述为在(1)中，模态运算符适用于公式A(t)，术语t在模态运算符的范围内。在(2)中，t不在模态运算符的范围内。