10.2 First-Order Reasoning about Knowledge

The syntax for first-order epistemic logic is the obvious combination of the constructs of first-order logic—quantification, conjunction, and negation—and the modal operators K₁, …, K_n. The semantics uses relational epistemic structures. In a (propositional) epistemic structure, each world is associated with a truth assignment to the primitive propositions via the interpretation π. In a relational epistemic structure, the π function associates with each world a relational structure. Formally, a relational epistemic structure for n agents over a vocabulary 풯 is a tuple (W, 풦₁, …, 풦_n, π), where W is a set of worlds, π associates with each world in W a 풯-structure (i.e., π(w) is a 풯-structure for each world w ∈ W), and 풦_i is a binary relation on W.

The semantics of first-order modal logic is, for the most part, the result of combining the semantics for first-order logic and the semantics for modal logic in a straightforward way. For example, a formula such as K_iAmerican(President) is true at a world w if, in all worlds that agent i considers possible, the president is American. Note that this formula can be true even if agent i does not know who the president is. That is, there might be some world that agent i considers possible where the president is Bill, and another where the president is George. As long as the president is American in all these worlds, agent i knows that the president is American.

What about a formula such as ∃xK_iAmerican(x)? It seems clear that this formula should be true if there is some individual in the domain at world w, say Bill, such that agent i knows that Bill is American. But now there is a problem. Although Bill may be a member of the domain of the relational structure π(w), it is possible that Bill is not a member of the domain of π(w′) for some world w′ that agent i considers possible at world w. There have been a number of solutions proposed to this problem that allow different domains at each world, but none of them are completely satisfactory (see the notes for references). For the purposes of this book, I avoid the problem by simply considering only common-domain epistemic structures, that is, relational epistemic structures where the domain is the same at every world. To emphasize this point, I write the epistemic structure as (W, D, 풦₁, …,풦_n, π), where D is the common domain used at each world, that is, D = dom(π(w)) for all w ∈ W.

Under the restriction to common-domain structures, defining truth of formulas becomes quite straightforward. Fix a common-domain epistemic structure M = (W, D, 풦₁, …, 풦_n, π). A valuation V on M is a function that assigns to each variable a member of D. This means that V(x) is independent of the world, although the interpretation of, say, a constant c may depend on the world. The definition of what it means for a formula φ to be true at a world w of M, given valuation V, now proceeds by the usual induction on structure. The clauses are exactly the same as those for first-order logic and propositional epistemic logic. For example,

(M, w, V) ⊨ P(t₁, …, t_k), where P is a k-ary relation symbol and t₁, …, t_k are terms, iff (V^π(w)(t₁), …, V^π(w)(t_k)) ∈ P^π(w).

In the case of formulas K_iφ, the definition is just as in the propositional case:

First-order epistemic logic is more expressive than propositional epistemic logic. One important example of its extra expressive power is that it can distinguish between "knowing that" and "knowing who," by using the fact that variables denote the same individual in the domain at different worlds. For example, the formula K_Alice∃x(Tall(x)) says that Alice knows that someone is tall. This formula may be true in a given world where Alice does not know whether Bill or George is tall; she may consider one world possible where Bill is tall and consider another world possible where George is tall. Therefore, although Alice knows that there is a tall person, she may not know exactly who the tall person is. On the other hand, the formula ∃xK_Alice(Tall(x)) expresses the proposition that Alice knows someone who is tall. Because a valuation is independent of the world, it is easy to see that this formula says that there is one particular person who is tall in every world that Alice considers possible.

What about axiomatizations? Suppose for simplicity that all the 풦_i relations are equivalence relations. In that case, the axioms K1–5 of S5_n are valid in common-domain epistemic structures. It might seem that a complete axiomatization can be obtained by considering the first-order analogue of Prop (i.e., allowing all substitution instances of axioms of first-order logic). Unfortunately, in the resulting system, F2 is not sound.

Consider the following instance of F2:

Now consider a relational epistemic structure M = (W, D, 풦₁, π), where

W consists of two worlds, w₁ and w₂;
D consists of two elements, d₁ and d₂;
풦₁(w₁) = 풦₁(w₂) = W;
π is such that President^π(wⁱ) ={d_i} and Tall^π(wⁱ) ={d_i} for i = 1, 2.

Note that d₁ is not tall in w₂ and d₂ is not tall in w₁; thus, (M, w₁) ⊨ ∀x K₁(Tall(x)). On the other hand, the president is d₁ and is tall in w₁ and the president is d₂ and is tall in w₂; thus, (M, w₁) ⊨ K₁(Tall(President)). It follows that (10.1) is not valid in structure M.

What is going on is that the valuation is independent of the world; hence, under a given valuation, a variable x is a rigid designator, that is, it denotes the same domain element in every world. On the other hand, a constant symbol such as President is not a rigid designator, since it can denote different domain elements in different worlds. It is easy to see that F2 is valid if t is a variable. More generally, F2 is valid if the term t is a rigid designator (Exercise 10.9). This suggests that F2 can be salvaged by extending the definition of substitutable as follows. If φ is a first-order formula (one with no occurrences of modal operators), then the definition of t being substitutable in φ is just that given in Section 10.2; if φ has some occurrences of modal operators, then t is substitutable in φ if t is a variable y such that there are no subformulas of the form ∃yψ in φ. With this extended definition, the hoped-for soundness and completeness result holds.

Theorem 10.2.1

With this definition of substitutable, S5_n and AX^fo together provide a sound and complete axiomatization of first-order epistemic logic with respect to relational epistemic structures where the 풦_i relation is an equivalence relation.