If A implies B and B implies C, then A implies C. So the implication A -> C is a consequence of the implications A -> B and B -> C. Let's define this phenomenon formally. So, let L be a set of implications. We say that A -> B follows, semantically follows, or logically follows, or just follows from L if, whenever we have a model of L, it must also be a model of A -> B. So, Z should be a model of A -> B for all subsets Z that are models of L, of all implications from L. And we write it down like this: L, again, we use the same sign as here; so this means that the implication A -> B follows from L. How do we check if the implication A -> B follows from L without considering all possible subsets of M? Let's define a closure operator that will help us do this. So we define for X, which is a subset of M, L(X) as follows. So L is a set of implications on M, X is a subset of M, and L(X) is going to be the intersection of all models of L that include X. So we look at all Ys such that X is a subset of Y and Y is a subset of M, and Y respects all implications from L. Let me give you an example. So, suppose that M is the set of all natural numbers. So, M is infinite in this case. And let's say that the set of implications is also infinite. It includes all implications of the form {i} -> {i + 1}, where i is any natural number. So what's L of a single- element set containing 0? To answer this question, we need to look at all models of this implication set that contain 0. Every such model must be a set of numbers that satisfies all these implications. And it must have 0. Because it has 0, and we have an implication that 0 implies 1, it must also include 1. And because L contains implication 1 -> 2, this set must also contain 2. And then it must contain 3 because of the implication 2 -> 3 and so on. So the only model of this set of implications is N itself, the set of all natural numbers. So here we have only one set Y, the set of all natural numbers, and so the intersection is N itself. So here L({0}) is the set of all natural numbers. Well, for finite M, we can give a slightly different definition, which is equivalent to this, but in a way is easier to check, is easier to work with. So we'll do it in two steps. First, we'll define X with the upper index L as follows. It will be a set that includes X and it also includes some additional attributes. So whenever L contains an implication A -> B such that A is a subset of X, we include B into this set. So we include B if there is an implication A -> B in L such that A is a subset of X. And then we can define L(X) as follows. We take X, we apply this operator once, and then we apply it again, and again, and again until we reach some fixed point, that is, until we get a set L(X) such that, if we apply this operator to it, we'll get the same set L(X) again. So we take X, we apply this operator L, and then we apply it again, and we apply it as long as something changes, as long as we get new attributes here. And once we have reached a fixed point, we're done. So I leave it as an exercise to prove that these two definitions of L(X) are in fact equivalent for a finite M. And another exercise is to prove that L(X) is indeed a closure operator. And I will now prove a statement that shows how we can use L(X) to check if A -> B is a consequence of L, if it semantically follows from L. So the proposition that I'm going to prove is as follows. X -> Y follows from L if and only if Y is a subset of L(X). So let's prove it in one direction first: if X -> Y is a consequence of L, then Y is a subset of L(X). Assume the opposite. Suppose that Y is not a subset of L(X). Well then, using this definition, we can see that there is a model of L that contains X but doesn't contain Y. So there is a model Z such that Z is a model of L, it includes X, and it doesn't include Y. But then Z violates the implication X -> Y because it contains X but it doesn't contain Y. So it's not a model of X -> Y. So we found a model of set L that violates the implication X -> Y. It means that X implies Y doesn't follow from L. So if Y is not a subset of L(X), then X -> Y doesn't follow from L. In the other direction, suppose that Y is in fact a subset of L(X). Then, for all Z such that X is a subset of Z and Z is a model of L, we have that Y is also a subset of Z. So why so? Y is a subset of L(X), but L(X) is the intersection of all models of L that contain X. So whenever we take a model Z of L that contains X, Y must be in it, Y must its subset. So Y is a subset of Z. But this means that L, that X -> Y follows from L simply by the definition. So we proved this proposition. And now if we want to check whether X -> Y follows from L, we can compute the closure of X under the implications from L and check whether Y is a subset of this closure. [MUSIC]