Правило тривиальности доказано.
2. Проведем пошаговое доказательство правила аддитивности:
1) имеем: X → Y (это посылка 1);
2) имеем: X → Z (это посылка 2);
3) имеем: Y ∪ Z → Y ∪ Z (из правила рефлексивности вывода Армстронга);
4) имеем: X ∪ Z → Y ∪ Z (получаем при помощи применения правила псевдотранзитивности вывода Армстронга, а потом как следствие первого и третьего шагов доказательства);
5) имеем: X ∪ X → Y ∪ Z (получаем, применяя правило псевдотранзитивности вывода Армстронга, а после следует из второго и четвертого шагов);
6) имеем X → Y ∪ Z (следует из пятого шага).
Правило аддитивности доказано.
3. И, наконец, проведем построение доказательства правила проективности:
1) имеем: X → Y ∪ Z, X → Y ∪ Z (это посылка);
2) имеем: Y → Y, Z → Z (выводится при помощи правила рефлексивности вывода Армстронга);
3) имеем: Y ∪ z → y, Y ∪ z → Z (получается из правила пополнения вывода Армстронга и следствием из второго шага доказательства);
4) имеем: X → Y, X → Z (получается, применением правила псевдотранзитивности вывода Армстронга, а затем как следствие из первого и третьего шагов доказательства).
Правило проективности доказано.
Все производные правила вывода доказаны.
4. Полнота системы правил Армстронга
Пусть F(S) — заданное множество функциональных зависимостей, заданных над схемой отношения S.
Обозначим через inv <F(S)> ограничение, накладываемое этим множеством функциональных зависимостей. Распишем его:
Inv <F(S)> r(S) = ∀X → Y ∈F(S) [inv r(S)].
Итак, это множество ограничений, накладываемое функциональными зависимостями, расшифровывается следующим образом: для любого правила из системы функциональных зависимостей X → Y, принадлежащего множеству функциональных зависимостей F(S), действует ограничение функциональных зависимостей inv r(S), определенных над множеством отношения r(S).
Пусть какое-то отношение r(S) удовлетворяет этому ограничению.
Применяя правила вывода Армстронга к функциональным зависимостям, определенным для множества F(S), можно получить новые функциональные зависимости, как уже было сказано и доказано нами ранее. И, что показательно, ограничениям этих функциональных зависимостей отношение F(S) будет автоматически удовлетворять, что видно из расширенной формы записи правил вывода Армстронга. Напомним общий вид этих расширенных правил вывода:
Правило вывода 1.inv < X → X > r(S);
Правило вывода 2.inv r(S) ⇒inv ∪ Z → Y> r(S);
Правило вывода 3.
