Armstrong's axioms

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 ${\displaystyle F^{+}}$) when applied to that set (denoted as ${\displaystyle F}$). They are also complete in that repeated application of these rules will generate all functional dependencies in the closure ${\displaystyle F^{+}}$.

More formally, let ${\displaystyle \langle R(U),F\rangle }$ denote a relational scheme over the set of attributes ${\displaystyle U}$ with a set of functional dependencies ${\displaystyle F}$. We say that a functional dependency ${\displaystyle f}$ is logically implied by ${\displaystyle F}$, and denote it with ${\displaystyle F\models f}$ if and only if for every instance ${\displaystyle r}$ of ${\displaystyle R}$ that satisfies the functional dependencies in ${\displaystyle F}$, ${\displaystyle r}$ also satisfies ${\displaystyle f}$. We denote by ${\displaystyle F^{+}}$ the set of all functional dependencies that are logically implied by ${\displaystyle F}$.

Furthermore, with respect to a set of inference rules ${\displaystyle A}$, we say that a functional dependency ${\displaystyle f}$ is derivable from the functional dependencies in ${\displaystyle F}$ by the set of inference rules ${\displaystyle A}$, and we denote it by ${\displaystyle F\vdash _{A}f}$ if and only if ${\displaystyle f}$ is obtainable by means of repeatedly applying the inference rules in ${\displaystyle A}$ to functional dependencies in ${\displaystyle F}$. We denote by ${\displaystyle F_{A}^{*}}$ the set of all functional dependencies that are derivable from ${\displaystyle F}$ by inference rules in ${\displaystyle A}$.

Then, a set of inference rules ${\displaystyle A}$ is sound if and only if the following holds:

${\displaystyle F_{A}^{*}\subseteq F^{+}}$

that is to say, we cannot derive by means of ${\displaystyle A}$ functional dependencies that are not logically implied by ${\displaystyle F}$. The set of inference rules ${\displaystyle A}$ is said to be complete if the following holds:

${\displaystyle F^{+}\subseteq F_{A}^{*}}$

more simply put, we are able to derive by ${\displaystyle A}$ all the functional dependencies that are logically implied by ${\displaystyle F}$.