# 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. 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 $\langle R(U),F\rangle$ 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 $F\vdash _{A}f$ 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:
$F_{A}^{*}\subseteq F^{+}$
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:
$F^{+}\subseteq F_{A}^{*}$
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$.
    If $Y\subseteq X$ then $X\to Y$.

### Axiom of augmentation

If $X$ holds $Y$ and $Z$ is a set of attributes, then $XZ$ holds $YZ$. It means that attribute in dependencies does not change the basic dependencies.
    If $X\to Y$, then $XZ\to YZ$ for any $Z$.

### Axiom of transitivity

If $X$ holds $Y$ and $Y$ holds $Z$, then $X$ holds $Z$.
    If $X\to Y$ and $Y\to Z$, then $X\to Z$.

## Additional rules (Secondary Rules)

These rules can be derived from the above axioms.

### Decomposition

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

#### Proof

| 1. $X\to YZ$ | (Given) |
| 2. $YZ\to Y$ | (Reflexivity) |
| 3. $X\to Y$ | (Transitivity of 1 & 2) |

### Composition

If $X\to Y$ and $A\to B$ then $XA\to YB$.

#### Proof

| 1. $X\to Y$ | (Given) |
| 2. $A\to B$ | (Given) |
| 3. $XA\to YA$ | (Augmentation of 1 & A) |
| 4. $YA\to YB$ | (Augmentation of 2 & Y) |
| 5. $XA\to YB$ | (Transitivity of 3 and 4) |

### Union

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

#### Proof

| 1. $X\to Y$ | (Given) |
| 2. $X\to Z$ | (Given) |
| 3. $X\to XZ$ | (Augmentation of 2 & X) |
| 4. $XZ\to YZ$ | (Augmentation of 1 & Z) |
| 5. $X\to YZ$ | (Transitivity of 3 and 4) |

### Pseudo transitivity

If $X\to Y$ and $YZ\to W$ then $XZ\to W$.

#### Proof

| 1. $X\to Y$ | (Given) |
| 2. $YZ\to W$ | (Given) |
| 3. $XZ\to YZ$ | (Augmentation of 1 & Z) |
| 4. $XZ\to W$ | (Transitivity of 3 and 2) |

### 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$.
    If $X\to Y$, then $X\to XY$.
Extensivity can replace augmentation as axiom in the sense that augmentation can be proved from extensivity together with the other axioms.

#### Proof

| 1. $XZ\to X$ | (Reflexivity) |
| 2. $X\to Y$ | (Given) |
| 3. $XZ\to Y$ | (Transitivity of 1 & 2) |
| 4. $XZ\to XYZ$ | (Extensivity of 3) |
| 5. $XYZ\to YZ$ | (Reflexivity) |
| 6. $XZ\to YZ$ | (Transitivity of 4 & 5) |

## 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.