3.6 量化

现代逻辑的关键特征之一就是变量满足的概念可以用来解释量化的公式。让我们用(24)作为一个例子。

>>> m.evaluate('exists x.(girl(x) & walk(x))', g)
True

在这里evaluate()``True，因为dom中有某些 u 通过绑定x到 u 的赋值满足（(25) ）。事实上，o是这样一个 u：

>>> m.evaluate('girl(x) & walk(x)', g.add('x', 'o'))
True

NLTK 中提供了一个有用的工具是satisfiers()方法。它返回满足开放公式的所有个体的集合。该方法的参数是一个已分析的公式、一个变量和一个赋值。下面是几个例子：

>>> fmla1 = read_expr('girl(x) | boy(x)')
>>> m.satisfiers(fmla1, 'x', g)
{'b', 'o'}
>>> fmla2 = read_expr('girl(x) -> walk(x)')
>>> m.satisfiers(fmla2, 'x', g)
{'c', 'b', 'o'}
>>> fmla3 = read_expr('walk(x) -> girl(x)')
>>> m.satisfiers(fmla3, 'x', g)
{'b', 'o'}

想一想为什么fmla2和fmla3是那样的值，这是非常有用。->的真值条件的意思是fmla2等价于-girl(x) | walk(x)，要么不是女孩要么没有步行的个体满足条件。因为b(Bertie)和c(Cyril)都不是女孩，根据模型m，它们都满足整个公式。当然o也满足公式，因为o两项都满足。现在，因为话题的域的每一个成员都满足fmla2，相应的全称量化公式也为真。

>>> m.evaluate('all x.(girl(x) -> walk(x))', g)
True

换句话说，一个全称量化公式∀x.φ关于g为真，只有对每一个 u，φ关于g[u/x]为真。

注意

轮到你来：先用笔和纸，然后用m.evaluate()，尝试弄清楚all x.(girl(x) & walk(x))和exists x.(boy(x) -> walk(x))的真值。确保你能理解为什么它们得到这些值。