Chapter 10: First-Order Modal Logic

Overview

"Contrariwise," continued Tweedledee, "if it was so, it might be, and if it were so, it would be; but as it isn't, it ain't. That's logic!"

—Charles Lutwidge Dodgson (Lewis Carroll)

Propositional logic is useful for modeling rather simple forms of reasoning, but it lacks the expressive power to capture a number of forms of reasoning. In particular, propositional logic cannot talk about individuals, the properties they have, and relations between them, nor can it quantify over individuals, so as to say that all individuals have a certain property or that some individual can. These are all things that can be done in first-order logic.

To understand these issue, suppose that Alice is American but Bob is not. In a propositional logic, there could certainly be a primitive proposition p that is intended to express the fact that Alice is American, and another primitive proposition q to express that Bob is American. The statement that Alice is American but Bob is not would then be expressed as p ∧ q. But this way of expressing the statement somehow misses out on the fact that there is one property—being American—and two individuals, Alice and Bob, each of whom may or may not possess the property. In first-order logic, the fact that Alice is American and Bob is not can be expressed using a formula such as American(Alice) ∧ American(Bob). This formula brings out the relationship between Alice and Bob more clearly.

First-order logic can also express relations and functional connections between individuals. For example, the fact that Alice is taller than Bob can be expressed using a formula such as Taller(Alice, Bob); the fact that Joe is the father of Sara can be expressed by a formula such as Joe = Father(Sara). Finally, first-order logic can express the fact that all individuals have a certain property or that there is some individual who has a certain property by using a universal quantifier ∀, read "for all," or an existential quantifier ∃, read "there exists," respectively. For example, the formula ∃x ∀yTaller(x, y) says that there is someone who is taller than everyone; the formula ∀x ∀y ∀z((Taller(x, y) ∧ Taller(y, z)) ⇒ Taller(x, z)) says that the taller-than relation is transitive: if x is taller than y and y is taller than z, then x is taller than z.

First-order modal logic combines first-order logic with modal operators. As with everything else we have looked at so far, new subtleties arise in the combination of first-order logic and modal logic that do not appear in propositional modal logic or first-order logic alone. I first review first-order logic and then consider a number of first-order modal logics.