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. The axioms are sound in generating only functional dependencies in the closure of a set of functional dependencies (denoted as F^{+}) when applied to that set (denoted as F). They are also complete in that repeated application of these rules will generate all functional dependencies in the closure F^+. More formally, let denote a relational scheme over the set of attributes U with a set of functional dependencies F. We say that a functional dependency f is logically implied by F, and denote it with F \models f if and only if for every instance r of R that satisfies the functional dependencies in F, r also satisfies f. We denote by F^{+} the set of all functional dependencies that are logically implied by F. Furthermore, with respect to a set of inference rules A, we say that a functional dependency f is derivable from the functional dependencies in F by the set of inference rules A, and we denote it by if and only if f is obtainable by means of repeatedly applying the inference rules in A to functional dependencies in F. We denote by F^{*}_{A} the set of all functional dependencies that are derivable from F by inference rules in A. Then, a set of inference rules A is sound if and only if the following holds: that is to say, we cannot derive by means of A functional dependencies that are not logically implied by F. The set of inference rules A is said to be complete if the following holds: more simply put, we are able to derive by A all the functional dependencies that are logically implied by F.

Axioms (primary rules)

Let R(U) be a relation scheme over the set of attributes U. Henceforth we will denote by letters X, Y, Z any subset of U and, for short, the union of two sets of attributes X and Y by XY instead of the usual X \cup Y; this notation is rather standard in database theory when dealing with sets of attributes.

Axiom of reflexivity

If X is a set of attributes and Y is a subset of X, then X holds Y. Hereby, X holds Y [X \to Y] means that X functionally determines Y.

Axiom of augmentation

If X holds Y and Z is a set of attributes, then X Z holds Y Z. It means that attribute in dependencies does not change the basic dependencies.

Axiom of transitivity

If X holds Y and Y holds Z, then X holds Z.

Additional rules (Secondary Rules)

These rules can be derived from the above axioms.

Decomposition

If X \to Y Z then X \to Y and X \to Z.

Proof

Composition

If X \to Y and A \to B then X A \to Y B.

Proof

Union

If X \to Y and X \to Z then X \to YZ.

Proof

Pseudo transitivity

If X \to Y and Y Z \to W then X Z\to W.

Proof

Self determination

I \to I for any I. This follows directly from the axiom of reflexivity.

Extensivity

The following property is a special case of augmentation when Z=X. 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 F, an Armstrong relation is a relation which satisfies all the functional dependencies in the closure F^+ 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.