I’ve touched on the point several times already that some FDs imply others; now it’s time to get more specific. First of all, however, I need to introduce some notation—notation that (a) reduces the number of keystrokes required in formal proofs and the like and (b) can also help, sometimes, to see the forest as well as the trees, as it were.
As you might recall, the statement of Heath’s Theorem in Chapter 5 included the following sentence: Let XY denote the union of X and Y, and similarly for XZ. The notation I want to introduce is basically just an extension of this simple idea (it’s a trifle illogical, but it’s very convenient). To be specific, the notation uses expressions of the form XY to mean:
The union of {X} and {Y}, if X and Y denote individual attributes (i.e., are individual attribute names)
The union of X and Y, if X and Y denote sets of attributes (i.e., are sets of attribute names)
It also allows {X} to be abbreviated to just X (e.g., in an FD) if X denotes an individual attribute. Note: For convenience, I’ll refer to this notation from this point forward as Heath notation.
We’ve seen that, formally speaking, an FD is just an expression of the form X → Y, where X and Y are sets (actually sets of attribute names, but from a formal point of view it really doesn’t matter what the sets consist of). Now, suppose we’re given some set (F, say) of FDs. Then we can apply certain formal rules of inference to derive further FDs from the ones in F—FDs that are implied by the ones in F, meaning that if the ones in F hold in some relvar R, then the derived ones do so too. The rules in question were first stated by Armstrong in 1974 and for that reason are usually referred to as Armstrong’s inference rules or (more commonly) Armstrong’s axioms. They can be stated in a variety of equivalent ways, of which the following is perhaps the simplest:
If Y is a subset of X, then X → Y (“reflexivity”).
If X → Y, then XZ → YZ (“augmentation”).
If X → Y and Y → Z, then X → Z (“transitivity”).
Observe that these rules are intuitively reasonable, given the intended interpretation of an FD. That is, since we know what FDs “mean,” we can easily see that, e.g., if the FDs X → Y and Y → Z both hold in relvar R, then the FD X → Z must do so too. Note: The suppliers relvar S illustrates this particular rule—the FDs {SNO} → {CITY} and {CITY} → {STATUS} both hold in that relvar, and therefore the FD {SNO} → {STATUS} does so, too.
So the rules are reasonable. But what’s more important is that they’re both sound and complete. Soundness and completeness are concepts frequently encountered in connection with formal systems in general. In the formal system under consideration here, this is what they mean:
Completeness: If an FD f is implied by the ones in the given set F, then it can be derived from the ones in F by means of the rules. (To repeat, to say some FD f is implied by the FDs in some set F is to say that if the FDs in F hold, then f holds too.)
Soundness: If an FD f isn’t implied by the ones in the given set F, then it can’t be derived from the ones in F by means of the rules.[66]
The rules thus form what’s called an axiomatization for FDs. As a consequence, they can be used to derive what’s called the closure F+of any given set F of FDs. Here’s a definition:
What’s more, the derivation process can be mechanized; that is, Armstrong’s rules can be incorporated into (e.g.) a design tool that, given a set F of FDs that hold in some relvar R, will be able to compute the closure F+ of that set F, or in other words the complete set of all FDs that hold in that relvar. The significance of this fact should be obvious.
[66] If you have a background in logic, you might like the following characterization: Soundness means all theorems are tautologies; completeness means all tautologies are theorems. Or more intuitively (and with acknowledgments to Hugh Darwen): Soundness means if you can prove it, it’s true; completeness means if it’s true, you can prove it.