Armstrong's axioms


Armstrong's axioms are a set of axioms used to infer all the functional dependencies on a relational database. They were developed by William W. Armstrong in his 1974 paper. The axioms are sound in generating only functional dependencies in the closure of a set of functional dependencies when applied to that set. 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.

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.

Axiom of transitivity

If holds and holds, then holds.

Additional rules (Secondary Rules)

These rules can be derived from the above axioms.

Decomposition

If then and.

Proof

Composition

If and then.

Proof

Union (Notation)

If and then.

Pseudo transitivity

If and then.

Proof

Self determination

for any. This follows directly from the axiom of reflexivity.

Extensivity

The following property is a special case of augmentation when.
Extensivity can replace augmentation as axiom in the sense that augmentation can be proved from extensivity together with the other axioms.

Proof

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.