Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Armstrong's Axioms

**by****William W. Armstrong,****Yatsuka Nakamura, and****Piotr Rudnicki**- Received October 25, 2002
- MML identifier: ARMSTRNG

- [ Mizar article, MML identifier index ]

environ vocabulary ARMSTRNG, BOOLE, RELAT_1, RELAT_2, FINSET_1, FUNCT_1, FUNCT_4, CARD_3, PBOOLE, ZF_REFLE, MCART_1, ORDERS_1, SETFAM_1, INT_1, EQREL_1, WAYBEL_4, SUBSET_1, CANTOR_1, CARD_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, MARGREL1, MATRLIN, BINARITH, BINARI_3, ZF_LANG, MIDSP_3, POWER, EUCLID, ARYTM_1, FINSEQ_4, CONLAT_1, FINSUB_1, PARTFUN1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, FINSUB_1, RELAT_1, RELAT_2, RELSET_1, SETFAM_1, PARTFUN1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, FUNCT_4, FUNCT_1, ORDERS_1, TOLER_1, MCART_1, CARD_3, PBOOLE, STRUCT_0, WAYBEL_4, CANTOR_1, YELLOW_8, CARD_1, FINSEQ_1, PRE_CIRC, MARGREL1, FUNCT_2, FINSEQ_2, MATRLIN, BINARITH, BINARI_3, MIDSP_3, FINSEQ_4, SERIES_1, EUCLID; constructors INT_1, WAYBEL_4, CANTOR_1, YELLOW_8, PRE_CIRC, MATRLIN, BINARITH, BINARI_3, MIDSP_3, REAL_1, SERIES_1, EUCLID, FINSEQOP, PRALG_1; clusters FINSET_1, SUBSET_1, ALTCAT_1, PBOOLE, FINSEQ_1, FINSEQ_2, GOBRD13, FUNCT_1, ORDERS_1, CANTOR_1, RELSET_1, EQREL_1, WAYBEL_7, INT_1, MARGREL1, BINARITH, XBOOLE_0, MATRLIN, PRALG_1, FRAENKEL, XREAL_0, MEMBERED, NUMBERS, ORDINAL2; requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM; begin theorem :: ARMSTRNG:1 for B being set st B is cap-closed for X being set, S being finite Subset-Family of X st X in B & S c= B holds Intersect S in B; definition cluster reflexive antisymmetric transitive non empty Relation; end; theorem :: ARMSTRNG:2 for R being antisymmetric transitive non empty Relation, X being finite Subset of field R st X <> {} ex x being Element of X st x is_maximal_wrt X, R; definition let X be set, R be Relation; func R Maximal_in X -> Subset of X means :: ARMSTRNG:def 1 for x being set holds x in it iff x is_maximal_wrt X, R; end; definition let x, X be set; pred x is_/\-irreducible_in X means :: ARMSTRNG:def 2 x in X & for z, y being set st z in X & y in X & x = z /\ y holds x = z or x = y; antonym x is_/\-reducible_in X; end; definition let X be non empty set; func /\-IRR X -> Subset of X means :: ARMSTRNG:def 3 for x being set holds x in it iff x is_/\-irreducible_in X; end; scheme FinIntersect {X() -> non empty finite set, P[set]} : for x being set st x in X() holds P[x] provided for x being set st x is_/\-irreducible_in X() holds P[x] and for x, y being set st x in X() & y in X() & P[x] & P[y] holds P[x /\ y]; theorem :: ARMSTRNG:3 for X being non empty finite set, x being Element of X ex A being non empty Subset of X st x = meet A & for s being set st s in A holds s is_/\-irreducible_in X; definition let X be set, B be Subset-Family of X; attr B is (B1) means :: ARMSTRNG:def 4 X in B; end; definition let B be set; redefine attr B is cap-closed; synonym B is (B2); end; definition let X be set; cluster (B1) (B2) Subset-Family of X; end; theorem :: ARMSTRNG:4 for X being set, B being non empty Subset-Family of X st B is cap-closed for x being Element of B st x is_/\-irreducible_in B & x <> X for S being finite Subset-Family of X st S c= B & x = Intersect S holds x in S; definition let X, D be non empty set, n be Nat; cluster -> FinSequence-yielding Function of X, n-tuples_on D; end; definition let f be FinSequence-yielding Function, x be set; cluster f.x -> FinSequence-like; end; definition :: cannot redefine from VALUAT for I need to use functions from :: BINARI* and they are on Tuple of let n be Nat, p, q be Tuple of n, BOOLEAN; func p '&' q -> Tuple of n, BOOLEAN means :: ARMSTRNG:def 5 for i being set st i in Seg n holds it.i = (p/.i) '&' (q/.i); commutativity; end; theorem :: ARMSTRNG:5 for n being Nat, p being Tuple of n, BOOLEAN holds (n-BinarySequence 0) '&' p = n-BinarySequence 0; theorem :: ARMSTRNG:6 :: band2: for n being Nat, p being Tuple of n, BOOLEAN holds 'not' (n-BinarySequence 0) '&' p = p; theorem :: ARMSTRNG:7 :: BINARI_3:29 generalized for i being Nat holds (i+1)-BinarySequence 2 to_power i= 0*i^<*1*>; theorem :: ARMSTRNG:8 for n, i being Nat st i < n holds (n-BinarySequence 2 to_power i).(i+1) = 1 & for j being Nat st j in Seg n & j<>i+1 holds (n-BinarySequence 2 to_power i).j = 0; begin :: 2. The relational model of data definition struct DB-Rel (# Attributes -> finite non empty set, Domains -> non-empty ManySortedSet of the Attributes, Relationship -> Subset of product the Domains #); end; begin :: 3. Dependency structures definition let X be set; mode Subset-Relation of X is Relation of bool X; mode Dependency-set of X is Relation of bool X; canceled; end; definition let X be set; cluster non empty finite Dependency-set of X; end; definition let X be set; func Dependencies(X) -> Dependency-set of X equals :: ARMSTRNG:def 7 [: bool X, bool X :]; end; definition let X be set; cluster Dependencies X -> non empty; mode Dependency of X is Element of Dependencies X; end; definition let X be set, F be non empty Dependency-set of X; redefine mode Element of F -> Dependency of X; end; theorem :: ARMSTRNG:9 for X, x being set holds x in Dependencies X iff ex a, b being Subset of X st x = [a,b]; theorem :: ARMSTRNG:10 for X, x being set, F being Dependency-set of X holds x in F implies ex a, b being Subset of X st x = [a,b]; theorem :: ARMSTRNG:11 for X being set, F being Dependency-set of X, S being Subset of F holds S is Dependency-set of X; definition let R be DB-Rel, A, B be Subset of the Attributes of R; pred A >|> B, R means :: ARMSTRNG:def 8 for f, g being Element of the Relationship of R st f|A = g|A holds f|B = g|B; synonym A, B holds_in R; end; definition let R be DB-Rel; func Dependency-str R -> Dependency-set of the Attributes of R equals :: ARMSTRNG:def 9 { [A, B] where A, B is Subset of the Attributes of R: A >|> B, R }; end; theorem :: ARMSTRNG:12 for R being DB-Rel, A, B being Subset of the Attributes of R holds [A, B] in Dependency-str R iff A >|> B, R; begin :: 4. Full families of dependencies definition let X be set, P, Q be Dependency of X; pred P >= Q means :: ARMSTRNG:def 10 P`1 c= Q`1 & Q`2 c= P`2; reflexivity; synonym Q <= P; synonym P is_at_least_as_informative_as Q; end; theorem :: ARMSTRNG:13 :: antisymmetry for X being set, P, Q being Dependency of X st P <= Q & Q <= P holds P = Q; theorem :: ARMSTRNG:14 :: transitivity for X being set, P, Q, S being Dependency of X st P <= Q & Q <= S holds P <= S; definition let X be set, A, B be Subset of X; redefine func [A, B] -> Dependency of X; end; theorem :: ARMSTRNG:15 for X being set, A, B, A', B' being Subset of X holds [A,B] >= [A',B'] iff A c= A' & B' c= B; definition let X be set; func Dependencies-Order X -> Relation of Dependencies X equals :: ARMSTRNG:def 11 { [P, Q] where P, Q is Dependency of X : P <= Q }; end; theorem :: ARMSTRNG:16 for X, x being set holds x in Dependencies-Order X iff ex P, Q being Dependency of X st x = [P, Q] & P <= Q; theorem :: ARMSTRNG:17 for X being set holds dom Dependencies-Order X = [: bool X, bool X :]; theorem :: ARMSTRNG:18 for X being set holds rng Dependencies-Order X = [: bool X, bool X :]; theorem :: ARMSTRNG:19 for X being set holds field Dependencies-Order X = [: bool X, bool X :]; definition let X be set; cluster Dependencies-Order X -> non empty; cluster Dependencies-Order X -> total reflexive antisymmetric transitive; end; definition let X be set, F be Dependency-set of X; attr F is (F1) means :: ARMSTRNG:def 12 for A being Subset of X holds [A, A] in F; synonym F is (DC2); redefine attr F is transitive; synonym F is (F2); synonym F is (DC1); end; theorem :: ARMSTRNG:20 for X being set, F being Dependency-set of X holds F is (F2) iff for A, B, C being Subset of X st [A, B] in F & [B, C] in F holds [A, C] in F ; definition let X be set, F be Dependency-set of X; attr F is (F3) means :: ARMSTRNG:def 13 for A, B, A', B' being Subset of X st [A, B] in F & [A, B] >= [A', B'] holds [A', B'] in F; attr F is (F4) means :: ARMSTRNG:def 14 for A, B, A', B' being Subset of X st [A, B] in F & [A', B'] in F holds [A\/A', B\/B'] in F; end; theorem :: ARMSTRNG:21 for X being set holds Dependencies X is (F1) (F2) (F3) (F4); definition let X be set; cluster (F1) (F2) (F3) (F4) non empty Dependency-set of X; end; definition let X be set, F be Dependency-set of X; attr F is full_family means :: ARMSTRNG:def 15 F is (F1) (F2) (F3) (F4); end; definition let X be set; cluster full_family Dependency-set of X; end; definition let X be set; mode Full-family of X is full_family Dependency-set of X; end; theorem :: ARMSTRNG:22 for X being finite set, F being Dependency-set of X holds F is finite; definition let X be finite set; cluster finite Full-family of X; cluster -> finite Dependency-set of X; end; definition let X be set; cluster full_family -> (F1) (F2) (F3) (F4) Dependency-set of X; cluster (F1) (F2) (F3) (F4) -> full_family Dependency-set of X; end; definition let X be set, F be Dependency-set of X; attr F is (DC3) means :: ARMSTRNG:def 16 for A, B being Subset of X st B c= A holds [A, B] in F; end; definition let X be set; cluster (F1) (F3) -> (DC3) Dependency-set of X; cluster (DC3) (F2) -> (F1) (F3) Dependency-set of X; end; definition let X be set; cluster (DC3) (F2) (F4) non empty Dependency-set of X; end; theorem :: ARMSTRNG:23 :: F13_2_1_3: for X being set, F being Dependency-set of X st F is (DC3) (F2) holds F is (F1) (F3); theorem :: ARMSTRNG:24 :: F1_3_13: for X being set, F being Dependency-set of X st F is (F1) (F3) holds F is (DC3) ; definition let X be set; cluster (F1) -> non empty Dependency-set of X; end; theorem :: ARMSTRNG:25 :: WWA1: for R being DB-Rel holds Dependency-str R is full_family; theorem :: ARMSTRNG:26 :: Ex1: for X being set, K being Subset of X holds { [A, B] where A, B is Subset of X : K c= A or B c= A } is Full-family of X; begin :: 5. Maximal elements of full families definition let X be set, F be Dependency-set of X; func Maximal_wrt F -> Dependency-set of X equals :: ARMSTRNG:def 17 Dependencies-Order X Maximal_in F; end; theorem :: ARMSTRNG:27 for X being set, F being Dependency-set of X holds Maximal_wrt F c= F; definition let X be set, F be Dependency-set of X, x, y be set; pred x ^|^ y, F means :: ARMSTRNG:def 18 [x, y] in Maximal_wrt F; end; theorem :: ARMSTRNG:28 for X being finite set, P being Dependency of X, F being Dependency-set of X st P in F ex A, B being Subset of X st [A, B] in Maximal_wrt F & [A, B] >= P; theorem :: ARMSTRNG:29 for X being set, F being Dependency-set of X, A, B being Subset of X holds A ^|^ B, F iff [A, B] in F & not ex A', B' being Subset of X st [A', B'] in F & (A <> A' or B <> B') & [A, B] <= [A', B']; definition let X be set, M be Dependency-set of X; attr M is (M1) means :: ARMSTRNG:def 19 for A being Subset of X ex A', B' being Subset of X st [A', B'] >= [A, A] & [A', B'] in M; attr M is (M2) means :: ARMSTRNG:def 20 for A, B, A', B' being Subset of X st [A, B] in M & [A', B'] in M & [A, B] >= [A', B'] holds A = A' & B = B'; attr M is (M3) means :: ARMSTRNG:def 21 for A, B, A', B' being Subset of X st [A, B] in M & [A', B'] in M & A' c= B holds B' c= B; end; theorem :: ARMSTRNG:30 :: WWA2: for X being finite non empty set, F being Full-family of X holds Maximal_wrt F is (M1) (M2) (M3); theorem :: ARMSTRNG:31 :: WWA2a check this proof, WWA is sketchy for X being finite set, M, F being Dependency-set of X st M is (M1) (M2) (M3) & F = {[A, B] where A, B is Subset of X : ex A', B' being Subset of X st [A', B'] >= [A, B] & [A', B'] in M} holds M = Maximal_wrt F & F is full_family & for G being Full-family of X st M = Maximal_wrt G holds G = F; definition let X be non empty finite set, F be Full-family of X; cluster Maximal_wrt F -> non empty; end; theorem :: ARMSTRNG:32 :: Ex2: for X being finite set, F being Dependency-set of X, K being Subset of X st F = { [A, B] where A, B is Subset of X : K c= A or B c= A } holds {[K, X]}\/{[A, A] where A is Subset of X : not K c= A} = Maximal_wrt F; begin :: 6. Saturated subsets of Attributes definition let X be set, F be Dependency-set of X; func saturated-subsets F -> Subset-Family of X equals :: ARMSTRNG:def 22 { B where B is Subset of X: ex A being Subset of X st A ^|^ B, F }; synonym closed_attribute_subset F; end; definition let X be set, F be finite Dependency-set of X; cluster saturated-subsets F -> finite; end; theorem :: ARMSTRNG:33 for X, x being set, F being Dependency-set of X holds x in saturated-subsets F iff ex B, A being Subset of X st x = B & A ^|^ B, F; theorem :: ARMSTRNG:34 :: WWA3: for X being finite non empty set, F being Full-family of X holds saturated-subsets F is (B1) (B2); definition let X be set, B be set; func X deps_encl_by B -> Dependency-set of X equals :: ARMSTRNG:def 23 { [a, b] where a, b is Subset of X : for c being set st c in B & a c= c holds b c= c}; end; theorem :: ARMSTRNG:35 :: WWA3_0: for X being set, B being Subset-Family of X, F being Dependency-set of X holds X deps_encl_by B is full_family; theorem :: ARMSTRNG:36 :: WWA3_00: for X being finite non empty set, B being Subset-Family of X holds B c= saturated-subsets (X deps_encl_by B); theorem :: ARMSTRNG:37 :: WWA3a: for X being finite non empty set, B being Subset-Family of X st B is (B1) (B2) holds B = saturated-subsets (X deps_encl_by B) & for G being Full-family of X st B = saturated-subsets G holds G = X deps_encl_by B; definition let X be set, F be Dependency-set of X; func enclosure_of F -> Subset-Family of X equals :: ARMSTRNG:def 24 { b where b is Subset of X : for A, B being Subset of X st [A, B] in F & A c= b holds B c= b }; end; theorem :: ARMSTRNG:38 :: WWA3c: for X being finite non empty set, F being Dependency-set of X holds enclosure_of F is (B1) (B2); theorem :: ARMSTRNG:39 :: WWA3b :: Added for proving WWA7 where it is referenced but never :: stated. This characterizes the smallest full family :: containing a given dependency set for X being finite non empty set, F being Dependency-set of X holds F c= X deps_encl_by enclosure_of F & for G being Dependency-set of X st F c= G & G is full_family holds X deps_encl_by enclosure_of F c= G; definition let X be finite non empty set, F be Dependency-set of X; func Dependency-closure F -> Full-family of X means :: ARMSTRNG:def 25 F c= it & for G being Dependency-set of X st F c= G & G is full_family holds it c= G; end; theorem :: ARMSTRNG:40 :: WWA3d: for X being finite non empty set, F being Dependency-set of X holds Dependency-closure F = X deps_encl_by enclosure_of F; theorem :: ARMSTRNG:41 :: Ex3: for X being set, K being Subset of X, B being Subset-Family of X st B = {X}\/{A where A is Subset of X : not K c= A} holds B is (B1) (B2); theorem :: ARMSTRNG:42 :: Ex3a: :: use WWA3* to prove what is the saturated subset for the example for X being finite non empty set, F being Dependency-set of X, K being Subset of X st F = { [A, B] where A, B is Subset of X : K c= A or B c= A } holds {X}\/{B where B is Subset of X : not K c= B} = saturated-subsets F; theorem :: ARMSTRNG:43 :: Ex3b: for X being finite set, F being Dependency-set of X, K being Subset of X st F = { [A, B] where A, B is Subset of X : K c= A or B c= A } holds {X}\/{B where B is Subset of X : not K c= B} = saturated-subsets F; definition let X, G be set, B be Subset-Family of X; pred G is_generator-set_of B means :: ARMSTRNG:def 26 G c= B & B = { Intersect S where S is Subset-Family of X: S c= G }; end; theorem :: ARMSTRNG:44 :: WWA4b: for X be finite non empty set, G being Subset-Family of X holds G is_generator-set_of saturated-subsets (X deps_encl_by G); theorem :: ARMSTRNG:45 :: WWA4a: for X being finite non empty set, F being Full-family of X ex G being Subset-Family of X st G is_generator-set_of saturated-subsets F & F = X deps_encl_by G; :: WWA did not show what generators B are, :: they are the irreducible elements \ X theorem :: ARMSTRNG:46 for X being set, B being non empty finite Subset-Family of X st B is (B1) (B2) holds /\-IRR B is_generator-set_of B; theorem :: ARMSTRNG:47 for X, G being set, B being non empty finite Subset-Family of X st B is (B1) (B2) & G is_generator-set_of B holds /\-IRR B c= G\/{X}; begin :: 7. Justification of the axioms theorem :: ARMSTRNG:48 :: WWA5: for X being non empty finite set, F being Full-family of X ex R being DB-Rel st the Attributes of R = X & (for a being Element of X holds (the Domains of R).a = INT) & F = Dependency-str R; begin definition let X be set, F be Dependency-set of X; func candidate-keys F -> Subset-Family of X equals :: ARMSTRNG:def 27 { A where A is Subset of X : [A, X] in Maximal_wrt F }; end; theorem :: ARMSTRNG:49 :: Ex8: for X being finite set, F being Dependency-set of X, K being Subset of X st F = { [A, B] where A, B is Subset of X : K c= A or B c= A } holds candidate-keys F = {K}; definition let X be set; redefine attr X is empty; antonym X is (C1); end; definition let X be set; attr X is without_proper_subsets means :: ARMSTRNG:def 28 for x, y being set st x in X & y in X & x c= y holds x = y; synonym X is (C2); end; theorem :: ARMSTRNG:50 :: WWA6: for R being DB-Rel holds candidate-keys Dependency-str R is (C1) (C2); theorem :: ARMSTRNG:51 :: WWA6a: for X being finite set, C being Subset-Family of X st C is (C1) (C2) ex F being Full-family of X st C = candidate-keys F; theorem :: ARMSTRNG:52 :: WWA6a A more reasonable version for X being finite set, C being Subset-Family of X, B being set st C is (C1) (C2) & B = {b where b is Subset of X : for K being Subset of X st K in C holds not K c= b} holds C = candidate-keys (X deps_encl_by B); theorem :: ARMSTRNG:53 :: WWA6a proof II for X being non empty finite set, C being Subset-Family of X st C is (C1) (C2) ex R being DB-Rel st the Attributes of R = X & C = candidate-keys Dependency-str R; begin :: 9. Applications definition let X be set, F be Dependency-set of X; attr F is (DC4) means :: ARMSTRNG:def 29 for A, B, C being Subset of X st [A, B] in F & [A, C] in F holds [A, B\/C] in F; attr F is (DC5) means :: ARMSTRNG:def 30 for A, B, C, D being Subset of X st [A, B] in F & [B\/C, D] in F holds [A\/C, D] in F; attr F is (DC6) means :: ARMSTRNG:def 31 for A, B, C being Subset of X st [A, B] in F holds [A\/C, B] in F; end; theorem :: ARMSTRNG:54 :: APP0: for X being set, F being Dependency-set of X holds F is (F1) (F2) (F3) (F4) iff F is (F2) (DC3) (F4); theorem :: ARMSTRNG:55 :: APP1: for X being set, F being Dependency-set of X holds F is (F1) (F2) (F3) (F4) iff F is (DC1) (DC3) (DC4); theorem :: ARMSTRNG:56 :: APP2: for X being set, F being Dependency-set of X holds F is (F1) (F2) (F3) (F4) iff F is (DC2) (DC5) (DC6); definition let X be set, F be Dependency-set of X; func charact_set F equals :: ARMSTRNG:def 32 { A where A is Subset of X : ex a, b being Subset of X st [a, b] in F & a c= A & not b c= A }; end; theorem :: ARMSTRNG:57 for X, A being set, F being Dependency-set of X st A in charact_set F holds A is Subset of X & ex a, b being Subset of X st [a, b] in F & a c= A & not b c= A; theorem :: ARMSTRNG:58 for X being set, A being Subset of X, F being Dependency-set of X st ex a, b being Subset of X st [a, b] in F & a c= A & not b c= A holds A in charact_set F; theorem :: ARMSTRNG:59 :: WWA7: for X being finite non empty set, F being Dependency-set of X holds (for A, B being Subset of X holds [A, B] in Dependency-closure F iff for a being Subset of X st A c= a & not B c= a holds a in charact_set F) & saturated-subsets Dependency-closure F = (bool X) \ charact_set F; theorem :: ARMSTRNG:60 :: WWACorA: :: Bill: Is this the right translation for X being finite non empty set, F, G being Dependency-set of X st charact_set F = charact_set G holds Dependency-closure F = Dependency-closure G; theorem :: ARMSTRNG:61 for X being non empty finite set, F being Dependency-set of X holds charact_set F = charact_set (Dependency-closure F); definition let A be set, K be set, F be Dependency-set of A; pred K is_p_i_w_ncv_of F means :: ARMSTRNG:def 33 (for a being Subset of A st K c= a & a <> A holds a in charact_set F) & for k being set st k c< K ex a being Subset of A st k c= a & a <> A & not a in charact_set F; end; theorem :: ARMSTRNG:62 :: WWACorB: for X being finite non empty set, F being Dependency-set of X, K being Subset of X holds K in candidate-keys Dependency-closure F iff K is_p_i_w_ncv_of F;

Back to top