Subsection 7.6.3 The Closed World Assumption
There’s a specific kind of reasoning in the absence of facts that often makes sense when we’re working with the contents of a database.
Suppose that we want a rule that says that we’ll drop from our approved supplier list any company from whom we haven’t bought anything in the last 24 months. We might write (for simplicity, assume that the date of a transaction is stated in months):
[1] x ((y (Order(y) (Supplier(x, y) (Month(y) > Now – 24))) ApprovedSupplier(x))
Read this as, “For any x, if there doesn’t exist an order y that was supplied by x more recently than 24 months ago, then x isn’t an approved supplier.
Fine. But how shall we prove that there doesn’t exist an order?
Let’s generalize a bit. Suppose that, in some arbitrary application, we have:
[2] ¬∃x (P(x)) → Q
In other words, if there’s no x that satisfies some property P, then we can assert some claim Q. If we want to reason with [2], how shall we go about showing that there is no such x? If we can actually prove that, great. Absent such a proof, we could look around for a while to see if we can see an example x. But failing to find one is not a proof that none exists. For example, we could look around for quite a while and fail to find an albino peacock. That is not, however, a proof that none exists. In fact, they do. So we can’t, in general admit “I tried to find one but I couldn’t,” as a proof technique.
In a database application, on the other hand, we often want to do exactly that. Returning to our outdated supplier list problem: If we systematically check the database but fail to find a recent order from some supplier, we can conclude that there hasn’t been such an order. (Or at least we can if we assume that our order entry process works as it should.) We can thus conclude that the supplier should be dropped.
In the special case in which we believe that we are operating in a closed world in which all relevant facts are explicitly asserted to be true, we can take the absence of an assertion as equivalent to the claim that it is false. When we do this, we’ll say that we’re exploiting the closed world assumption.
Implementing this requires that we add a technique that can’t be described in the predicate logic framework that we’ve been using.
Exercises Exercises
1.
Assume that you have access to the registrar’s database at University U. You also have the following rule:
∀x ((Student(x) ∧ (¬∃c (Course(c) ∧ Taken(x, c) ∧ DeptOf(c, English)))) → ¬CanGraduate(x))
In other words, no one can graduate without taking an English course.
Suppose that we want to try to prove that some student x cannot graduate. Which of the following is true:
The closed world assumption is valid here. Failure to find an English course taken by x should enable us to conclude that x cannot graduate.
The closed world assumption is not valid here. Failure to find an English course taken by x tells us nothing for sure.
2.
Assume that you can look at your friend Chris’s Facebook account and see her list of Facebook friends. You also take the following as a premise:
∀x (¬Knows(Chris, x) → ¬WorthKnowing(x))
In other words, anyone Chris doesn’t know isn’t worth knowing.
Suppose that we want to try to prove that some person x isn’t worth knowing. Which of the following is true:
The closed world assumption is valid here. Failure to find x on Chris’s list of Facebook friends should enable us to conclude that Chris doesn’t know x.
The closed world assumption is not valid here. Failure to find x on Chris’s list of Facebook friends tells us nothing for sure.