Quantification

One of the crucial insights of modern logic is that the notion of variable satisfaction can be used to provide an interpretation for quantified formulas. Let's use (24) as an example.

When is it true? Let's think about all the individuals in our domain, i.e., in dom. We want to check whether any of these individuals has the property of being a girl and walking. In other words, we want to know if there is some u in dom such that g[u/x] satisfies the open formula (25).

Consider the following:

>>> m.evaluate('exists x.(girl(x) & walk(x))', g) True evaluate() returns True here because there is some u in dom such that (25) is satisfied by an assignment which binds x to u. In fact, o is such a u:

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

One useful tool offered by NLTK is the satisfiers() method. This returns a set of all the individuals that satisfy an open formula. The method parameters are a parsed formula, a variable, and an assignment. Here are a few examples:

>>> fmlal = lp.parse('girl(x) | boy(x)') >>> m.satisfiers(fmla1, 'x', g) set(['b', 'o'])

>>> fmla2 = lp.parse('girl(x) -> walk(x)') >>> m.satisfiers(fmla2, 'x', g) set(['c', 'b', 'o'])

>>> fmla3 = lp.parse('walk(x) -> girl(x)') >>> m.satisfiers(fmla3, 'x', g) set(['b', 'o'])

It's useful to think about why fmla2 and fmla3 receive the values they do. The truth conditions for -> mean that fmla2 is equivalent to -girl(x) | walk(x), which is satisfied by something that either isn't a girl or walks. Since neither b (Bertie) nor c (Cyril) are girls, according to model m, they both satisfy the whole formula. And of course o satisfies the formula because o satisfies both disjuncts. Now, since every member of the domain of discourse satisfies fmla2, the corresponding universally quantified formula is also true.

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

In other words, a universally quantified formula Vx.9 is true with respect to g just in case for every u, 9 is true with respect to g[u/x].

Your Turn: Try to figure out, first with pencil and paper, and then using m.evaluate(), what the truth values are for all x.(girl(x) & A' walk(x)) and exists x.(boy(x) -> walk(x)). Make sure you understand why they receive these values.