The proof can be split into two parts:
This treatment assumes an untyped formalism of relational theory. Relations are modelled as a set of tuples (without any separate notion of a header, nor with any notion of types of attributes) and therefore the empty relation is the empty set ∅, and DEE={∅} is the relation containing a single empty tuple.
In this proof we are typically only concerned with non-empty relations, and therefore the set of attributes of the relation is uniquely defined.
Def: For any relation r≠∅, let *r denote the set of attributes of relation r.
Note: *∅ represents the attributes of the empty relation and is undefined.
Note: To avoid excessive bracketing we assume the unary prefix operator * has higher precedence than infix operators.
Def: The projection of relation r on any set of attributes α is denoted by r[α].
To avoid excessive bracketing we assume the unary postfix operator [] has higher precedence than infix operators.
Note: If r≠∅ then *(r[α]) = *r ∩ α.
Note: Let r be any relation and α,β be any sets of attributes, then r[β][α] = r[α∩β].
Def: Let r and s be relations. We write r⊥s if it is not the case that r and
s are non-empty relations with common attributes. i.e.
r⊥s = ¬( r≠∅ ∧ s≠∅ ∧ (*r∩*s)≠∅ )
Note: If r⊥s then the join r⋈s represents a Cartesian product, which we denote more specifically by r⨯s.
Note: if r⊥s then r⨯s = s⨯r if r⊥s and s⊥t then (r⨯s)⨯t = r⨯(s⨯t)
Note: Let r and s be non-empty relations with r⊥s. Then *(r⨯s) = *r ∪ *s X1
Note: Let r and s be relations with r⊥s. Then (r⨯s = ∅) ⇔ (r=∅ ∨ s=∅) X2
Note: Let r and s be non-empty relations with r⊥s. Then (r⨯s)[*r] = r X3
Note: Let r and s be non-empty relations with r⊥s and α be any set of attributes. Then: *r ∩ α = ∅ ⇒ (r⨯s)[α] = s[α] (*r ∩ α ≠ ∅) ∧ (*s ∩ α ≠ ∅) ⇒ (r⨯s)[α] = r[α] ⨯ s[α] X4
Claim: If r,s,t are relations with r≠∅, r⊥s and r⊥t, then (r⨯s = r⨯t) ⇒ s=t X5 Proof: Suppose not. i.e. r≠∅, r⨯s = r⨯t and s≠t if s=∅ then r⨯t = ∅ (because r⨯t = r⨯s = r⨯∅ = ∅) t=∅ (by X2 and r≠∅) contradicts s≠t else s≠∅ if t=∅ then r⨯s = ∅ (because r⨯s = r⨯t = r⨯∅ = ∅) s=∅ (by X2 and r≠∅) contradicts s≠∅ else t≠∅ *r ∪ *s = *(r⨯s) (by X1) = *(r⨯t) = *r ∪ *t (by X1) (*r ∪ *s) \ *r = (*r ∪ *t) \ *r (subtract *r from both sides) (*r\*r) ∪ (*s\*r) = (*r\*r) ∪ (*t\*r) (set difference is right distributive over union) *s\*r = *t\*r (*r\*r = ∅) *s = *t (*r ∩ *s = ∅ and *r ∩ *t = ∅) s = (r⨯s)[*s] (because r≠∅ and s≠∅ and by X3) = (r⨯t)[*t] (substitute r⨯s = r⨯t and *s=*t) = t (because r≠∅ and t≠∅ and by X3) contradicts s≠t
Def: Let 1 denote the relation {∅} (i.e. DEE). I1
Note: ∀r, r⨯1 = 1⨯r = r. I2
Note: if r≠∅ then (*r=∅ ⇔ r=1) I3
Def: Let R be a finite set of relations with no attributes in common between any pair of non-empty relations within R. i.e. ∀r,s∈R, r⊥s. ∏(R) denotes the Cartesian product of all relations in R, with special cases ∏(∅) = 1 and ∀r, ∏({r}) = r. M1
Note: ∏(R) is well defined because the Cartesian product is commutative and associative.
Note: ∀R,S, ∏(R∪S) = ∏(R) ⨯ ∏(S) M2
Note: ∏(R)=∅ ⇔ ∅∈R M3
Def: For any relation r≠∅, let deg(r) = |*r|. deg(∅) is undefined. DEG1
Note: Let r and s be non-empty relations with r⊥s. Then deg(r⨯s) = deg(r) + deg(s) DEG2
Def: Relation r is prime if both the following hold: P1
Note: ∅ is not prime P2
Def: Let r be a relation and R be a set of relations. P3 R is a prime factorisation of r if both:
Note: Relation ∅ has no prime factorisation. P4
Note: 1 has a prime factorisation ∅ since ∏(∅)=1 P5
Note: Every prime relation r has a prime factorisation {r} since ∏({r})=r. P6
Note: Less than (<) on the natural numbers N = {0,1,2,... } is a well-order relation. < is a strict total order with the property that every non-empty subset of N has a least element in this ordering.
Claim: ∀ relation r≠∅, ∃ prime factorisation R of r. E1
Proof:
Suppose not. Then there exist one or more non-empty relations with no prime factorisation.
The natural numbers are well ordered. Therefore there must exist a smallest degree for relations with no prime factorisation. Let it be n. Let r be a relation with deg(r)=n and r has no prime factorisation, and every relation of degree less than n has a prime factorisation.
Suppose n=0. Then deg(r)=0 so r=1. But 1 has a prime factorisation ∅ since ∏(∅)=1. This contradicts our supposition that r has no prime factorisation, so n>0.
Suppose r is prime. Then r has a prime factorisation {r} since ∏({r})=r. This contradicts our supposition that r has no prime factorisation, so r cannot be prime.
So we can assume both r is not prime and r≠1. Therefore ∃s,t such that r=s⨯t and {s,t}≠{1,r}. From r=s⨯t we know n = deg(r) = deg(s)+deg(t).
Suppose s=1. Then r = s⨯t = 1⨯t = t. This contradicts {s,t}≠{1,r}, therefore s≠1.
Suppose t=1. Then r = s⨯t = s⨯1 = s. This contradicts {s,t}≠{1,r}, therefore t≠1.
Since s≠1, deg(s)>0. From n = deg(s)+deg(t) we deduce deg(t)<n.
Since t≠1, deg(t)>0. From n = deg(s)+deg(t) we deduce deg(s)<n.
By supposition every relation of degree less than n has a prime factorisation. Therefore ∃prime factorisation S of s, and ∃prime factorisation T of t.
Therefore s=∏(S) and t=∏(T).
Now ∏(S∪T) = ∏(S)⨯∏(T) = s⨯t = r. Also ∀u∈S∪T, u is prime (since all members of both S and T are prime). Therefore S∪T is a prime factorisation of r. This contradicts our supposition that r has no prime factorisation.
Def: Let r and s be relations. We write r|s meaning r divides s if ∃t, r⨯t = s D1
Note: ∀r r|∅. (and in particular ∅|∅) D2
Note: Let r≠∅ and s≠∅. Then r|s ⇒ r=s[*r] D3
Note: ∀r r|r. D4
Note: ∀r 1|r. D5
Note: ∅|r ⇒ r=∅ D6
Lemma: Let p and r be non-empty relations. Then: (*p ⊂ *r) ∧ (∃ t≠∅, (p|t) ∧ (r|t)) ⇒ p|r U1 (note that the strict subset operator is used in the condition *p ⊂ *r) Proof: Suppose p≠∅, r≠∅, *p⊂*r, t≠∅, p|t, r|t. We want to prove p|r. if *p=∅ then p=1 (by I3) 1|r (by D5) p|r (substitute p=1) else *p≠∅ p≠1 (otherwise *p=∅) r≠1 (otherwise *r=∅ contradicting *p⊂*r) ∃s r⨯s = t (from r|t and D1) ∃q p⨯q = t (from p|t and D1) s≠∅ (otherwise t = r⨯s = r⨯∅ = ∅, contradicting t≠∅) q≠∅ (otherwise t = p⨯q = p⨯∅ = ∅, contradicting t≠∅) *s⊂*q (because *p⊂*r (*t\*r) ⊂ (*t\*p) (take complement w.r.t. *t on each side) *s = *t\*r (because *t = *r∪*s and *r∩*s = ∅) *q = *t\*p (because *t = *p∪*q and *p∩*q = ∅) *s⊂*q (substitutions in (*t\*r) ⊂ (*t\*p)) ) if *s ∩ *q = ∅ then *s=∅ (*s⊂*q and *s∩*q = ∅) s=1 (s≠∅, and *s=∅ so can apply I3) r = p⨯q (r = r⨯1 = r⨯s = p⨯q) p|r (by D1) else *s∩*q ≠ ∅ *r∩*q ≠ ∅ (because *q = *t\*p (because *t = *p∪*q and *p∩*q = ∅) = (*r∪*s) \ *p = (*r\*p)∪(*s\*p) (set difference is right distributive over union) *r\*p ⊆ *q (property of set union: A⊆(A∪B)) *r\*p ⊆ *r (property of set difference: (A\B)⊆A) *r\*p ≠ ∅ (*p ⊂ *r) *r ∩ *q ≠ ∅ (From above 3 facts about *r\*p) ) q = (p⨯q)[*q] (by X3 since p≠∅ and q≠∅) = (r⨯s)[*q] (substitute p⨯q = t = r⨯s) = r[*q]⨯s[*q] (by X4 since *r∩*q≠∅ and *s∩*q≠∅) = r[*q]⨯s (*s⊂*q so s[*q]=s) r⨯s = p⨯q = p⨯(r[*q]⨯s) (substitution for q) = (p⨯r[*q])⨯s (by associativity of ⨯) p ⨯ r[*q] = r (s≠∅ so apply X5) p|r (by D1)
Lemma: ∀prime relation p, ∀r,s with r⊥s, p|(r⨯s) ⇒ (p|r)∨(p|s) U2 Proof: Suppose p is prime, r⊥s, and p|(r⨯s). We shall show (p|r)∨(p|s) if r=∅ then p|∅ (by D2) p|r (substitute r=∅) else if s=∅ then p|∅ (by D2) p|s (substitute s=∅) else if r=1 then r⨯s = 1⨯s = s p|s (substitute r⨯s=s in p|(r⨯s)) else if s=1 then r⨯s = r⨯1 = r p|r (substitute r⨯s=r in p|(r⨯s)) else r≠∅, s≠∅, r≠1, s≠1 r⨯s ≠ ∅ (by X2) ∃q, r⨯s = p⨯q (p|(r⨯s) and D1) p≠∅, q≠∅ (otherwise r⨯s = p⨯q = ∅, contradicting r⨯s ≠ ∅) if *p ⊂ *r then ∃ t≠∅, (p|t) ∧ (r|t) (let t = r⨯s = p⨯q) p|r (by U1) else if *p⊂*s then ∃ t≠∅, (p|t) ∧ (s|t) (let t = r⨯s = p⨯q) p|s (by U1) else if *p=*r then r = (r⨯s)[*r] (by X3) = (p⨯q)[*p] (substitute *p = *r and p⨯q = r⨯s) = p (by X3) r|r (by D4) p|r (substitute r=p) else if *p = *s then s = (r⨯s)[*s] (by X3) = (p⨯q)[*p] (substitute *p=*s and p⨯q = r⨯s) = p (by X3) s|s (by D4) p|s (substitute s=p) else *p⊄*r, *p≠*r i.e. ¬(*p⊆*r) *p⊄*s, *p≠*s i.e. ¬(*p⊆*s) *r∩*p ≠ ∅ (because ¬(*p⊆*s)) *s∩*p ≠ ∅ (because ¬(*p⊆*r)) p = (p⨯q)[*p] (by X3) = (r⨯s)[*p] (substitute r⨯s = p⨯q) = r[*p] ⨯ s[*p] (*r∩*p ≠ ∅ and *s∩*p ≠ ∅ so apply X4) contradicts p is prime (p has been factorised into r[*p]⨯s[*p])
Claim: ∀relation r≠∅, prime factorisation of r is unique U3 Proof: Suppose not. Then there are non-empty relations with distinct prime factorisations. Let n be the smallest degree of any such relation. Let t≠∅ be a relation of degree n with prime factorisations P and Q with P≠Q. t = ∏(P) = ∏(Q) P≠∅ (otherwise t=∏(P)=1 which has unique factorisation ∅) ∃p∈P (because P≠∅) Q≠∅ (otherwise t=∏(Q)=1 which has unique factorisation ∅) ∃q∈Q (because Q≠∅) Let q' = ∏(Q\{q}) t = ∏(Q) = q⨯∏(Q\{q}) = q⨯q' n = deg(t) = deg(q)+deg(q') (by DEG2) deg(q')<n (because deg(q) > 0 since q∈Q is prime) q' has unique prime factorisation (deg(q') < n and definition of n) p | (q⨯q') (because p∈P so p|∏(P) and ∏(P) = q⨯q') (p|q)∨(p|q') (p is prime so lemma U2 is applicable) Claim: p∈Q Proof: if p|q then p=q p∈Q else p|q' (because (p|q)∨(p|q')) ∃u p⨯u = q' (by D1) u≠∅ (otherwise q'=∅ so t=∅) ∃U U is prime factorisation of u (by E1 and u≠∅) q' = p⨯u = p⨯∏(U) = ∏(U∪{p}) U∪{p} = Q\{q} (q' has unique prime factorisation) p∈Q Let t' = ∏(P\{p}) = ∏(Q\{p}). t = p⨯t' (by M2) n = deg(t) = deg(p)+deg(t') (by DEG2) deg(t')<n (p is prime so deg(p)>0) t' has unique factorisation (deg(t')<n and definition of n) P\{p} = Q\{p} (because t' has unique factorisation) P=Q (otherwise P\{p} ≠ Q\{p}) Contradiction to P≠Q