Armstrong's axioms are a set of axioms (or, more precisely, inference rules) used to infer all the functional dependencies on a relational database. They were developed by William W. Armstrong in his 1974 paper.[1] The axioms are sound in generating only functional dependencies in the closure of a set of functional dependencies (denoted as ) when applied to that set (denoted as ). They are also complete in that repeated application of these rules will generate all functional dependencies in the closure .
More formally, let denote a relational scheme over the set of attributes with a set of functional dependencies . We say that a functional dependency is logically implied by , and denote it with if and only if for every instance of that satisfies the functional dependencies in , also satisfies . We denote by the set of all functional dependencies that are logically implied by .
Furthermore, with respect to a set of inference rules , we say that a functional dependency is derivable from the functional dependencies in by the set of inference rules , and we denote it by if and only if is obtainable by means of repeatedly applying the inference rules in to functional dependencies in . We denote by the set of all functional dependencies that are derivable from by inference rules in .
Then, a set of inference rules is sound if and only if the following holds:
that is to say, we cannot derive by means of functional dependencies that are not logically implied by .
The set of inference rules is said to be complete if the following holds:
more simply put, we are able to derive by all the functional dependencies that are logically implied by .
Axioms (primary rules)
Let be a relation scheme over the set of attributes . Henceforth we will denote by letters , , any subset of and, for short, the union of two sets of attributes and by instead of the usual ; this notation is rather standard in database theory when dealing with sets of attributes.
Axiom of reflexivity
If is a set of attributes and is a subset of , then holds . Hereby, holds [] means that functionally determines .
If then .
Axiom of augmentation
If holds and is a set of attributes, then holds . It means that attribute in dependencies does not change the basic dependencies.
If , then for any .
Axiom of transitivity
If holds and holds , then holds .
If and , then .
Additional rules (Secondary Rules)
These rules can be derived from the above axioms.
Decomposition
If then and .
Proof
1.
(Given)
2.
(Reflexivity)
3.
(Transitivity of 1 & 2)
Composition
If and then .
Proof
1.
(Given)
2.
(Given)
3.
(Augmentation of 1 & A)
4.
(Augmentation of 2 & Y)
5.
(Transitivity of 3 and 4)
Union
If and then .
Proof
1.
(Given)
2.
(Given)
3.
(Augmentation of 2 & X)
4.
(Augmentation of 1 & Z)
5.
(Transitivity of 3 and 4)
Pseudo transitivity
If and then .
Proof
1.
(Given)
2.
(Given)
3.
(Augmentation of 1 & Z)
4.
(Transitivity of 3 and 2)
Self determination
for any . This follows directly from the axiom of reflexivity.
Extensivity
The following property is a special case of augmentation when .
If , then .
Extensivity can replace augmentation as axiom in the sense that augmentation can be proved from extensivity together with the other axioms.
Proof
1.
(Reflexivity)
2.
(Given)
3.
(Transitivity of 1 & 2)
4.
(Extensivity of 3)
5.
(Reflexivity)
6.
(Transitivity of 4 & 5)
Armstrong relation
Given a set of functional dependencies , an Armstrong relation is a relation which satisfies all the functional dependencies in the closure and only those dependencies. Unfortunately, the minimum-size Armstrong relation for a given set of dependencies can have a size which is an exponential function of the number of attributes in the dependencies considered.[2]