Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### The Incompleteness of the Lattice of Substitutions

**by****Adam Grabowski**- Received July 17, 2000
- MML identifier: HEYTING3

- [ Mizar article, MML identifier index ]

environ vocabulary ORDERS_1, FUNCT_1, MATRIX_2, FINSET_1, SQUARE_1, FINSEQ_1, BOOLE, FUNCT_5, MCART_1, LATTICES, LATTICE3, RELAT_2, FINSUB_1, PARTFUN1, HEYTING1, TARSKI, RELAT_1, SUBSTLAT, NORMFORM, BINOP_1, FILTER_1, CAT_1, YELLOW_0, WELLORD1, HEYTING2, BHSP_3, HEYTING3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, ORDERS_1, NAT_1, FINSEQ_1, BINOP_1, FINSET_1, FINSUB_1, PARTFUN1, LATTICES, DOMAIN_1, STRUCT_0, SUBSTLAT, MCART_1, FUNCT_5, WELLORD1, YELLOW_0, ABIAN, PRE_CIRC, LATTICE3, HEYTING2; constructors NAT_1, SETWISEO, DOMAIN_1, ABIAN, INT_1, TOLER_1, PRE_CIRC, WAYBEL_1, HEYTING1, HEYTING2, YELLOW_4; clusters RELSET_1, LATTICES, FINSET_1, SUBSET_1, FINSUB_1, SUBSTLAT, PARTFUN1, STRUCT_0, LATTICE3, ABIAN, NAT_1, YELLOW_1, YELLOW_3, BINARITH, FINSEQ_1, YELLOW_0, XREAL_0, MEMBERED, PRE_CIRC, ORDINAL2; requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM; begin :: Preliminaries scheme SSubsetUniq { R() -> RelStr, P[set] } : for A1, A2 being Subset of R() st (for x being set holds x in A1 iff P[x]) & (for x being set holds x in A2 iff P[x]) holds A1 = A2; definition let A, x be set; cluster [:A, {x}:] -> Function-like; end; theorem :: HEYTING3:1 for n being odd Nat holds 1 <= n; theorem :: HEYTING3:2 for X being finite non empty Subset of NAT holds max X in X; theorem :: HEYTING3:3 for X being finite non empty Subset of NAT holds ex n being Nat st X c= Seg n \/ {0}; theorem :: HEYTING3:4 for X being finite Subset of NAT holds ex k being odd Nat st not k in X; theorem :: HEYTING3:5 for k being Nat, X being finite non empty Subset of [:NAT,{k}:] holds ex n being non empty Nat st X c= [:Seg n \/ {0},{k}:]; theorem :: HEYTING3:6 for m being Nat, X being finite non empty Subset of [:NAT,{m}:] holds ex k being non empty Nat st not [2*k+1,m] in X; theorem :: HEYTING3:7 for m being Nat, X being finite Subset of [:NAT,{m}:] ex k being Nat st for l being Nat st l >= k holds not [l,m] in X; theorem :: HEYTING3:8 for L being upper-bounded Lattice holds Top L = Top LattPOSet L; theorem :: HEYTING3:9 for L being lower-bounded Lattice holds Bottom L = Bottom LattPOSet L; begin :: Poset of Substitutions canceled; theorem :: HEYTING3:11 for V being set, C being finite set, A, B being Element of Fin PFuncs (V, C) st A = {} & B <> {} holds B =>> A = {}; theorem :: HEYTING3:12 for V, V', C, C' being set st V c= V' & C c= C' holds SubstitutionSet (V, C) c= SubstitutionSet (V', C'); theorem :: HEYTING3:13 for V, V', C, C' being set, A being Element of Fin PFuncs (V, C), B being Element of Fin PFuncs (V', C') st V c= V' & C c= C' & A = B holds mi A = mi B; theorem :: HEYTING3:14 for V, V', C, C' being set st V c= V' & C c= C' holds the L_join of SubstLatt (V, C) = (the L_join of SubstLatt (V', C')) | [:the carrier of SubstLatt (V, C), the carrier of SubstLatt (V, C):]; definition let V, C be set; func SubstPoset (V, C) -> RelStr equals :: HEYTING3:def 1 LattPOSet SubstLatt (V, C); end; definition let V, C be set; cluster SubstPoset (V, C) -> with_suprema with_infima; end; definition let V, C be set; cluster SubstPoset (V, C) -> reflexive antisymmetric transitive; end; theorem :: HEYTING3:15 for V, C being set, a, b being Element of SubstPoset (V, C) holds a <= b iff for x being set st x in a ex y being set st y in b & y c= x; theorem :: HEYTING3:16 for V, V', C, C' being set st V c= V' & C c= C' holds SubstPoset (V, C) is full SubRelStr of SubstPoset (V', C'); definition let n, k be Nat; func PFArt (n, k) -> Element of PFuncs (NAT, {k}) means :: HEYTING3:def 2 for x being set holds x in it iff ( ex m being odd Nat st m <= 2*n & [m,k] = x ) or [2*n,k] = x; end; definition let n, k be Nat; cluster PFArt (n, k) -> finite; end; definition let n, k be Nat; func PFCrt (n, k) -> Element of PFuncs (NAT, {k}) means :: HEYTING3:def 3 for x being set holds x in it iff ( ex m being odd Nat st m <= 2*n + 1 & [m,k] = x ); end; definition let n,k be Nat; cluster PFCrt (n,k) -> finite; end; theorem :: HEYTING3:17 for n, k being Nat holds [2*n+1,k] in PFCrt (n,k); theorem :: HEYTING3:18 for n, k being Nat holds PFCrt (n,k) misses {[2*n+3,k]}; theorem :: HEYTING3:19 for n, k being Nat holds PFCrt (n+1,k) = PFCrt (n,k) \/ {[2*n+3,k]}; theorem :: HEYTING3:20 for n, k being Nat holds PFCrt (n,k) c< PFCrt (n+1,k); definition let n, k be Nat; cluster PFArt (n, k) -> non empty; end; theorem :: HEYTING3:21 for n, m, k being Nat holds not PFArt (n, m) c= PFCrt (k, m); theorem :: HEYTING3:22 for n, m, k being Nat st n <= k holds PFCrt (n,m) c= PFCrt (k,m); theorem :: HEYTING3:23 for n being Nat holds PFArt (1,n) = { [1,n], [2,n] }; definition let n, k be Nat; func PFBrt (n,k) -> Element of Fin PFuncs (NAT, {k}) means :: HEYTING3:def 4 for x being set holds x in it iff ( ex m being non empty Nat st m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k); end; theorem :: HEYTING3:24 for n, k being Nat, x being set st x in PFBrt (n+1,k) holds ex y being set st y in PFBrt (n,k) & y c= x; theorem :: HEYTING3:25 for n, k being Nat holds not PFCrt (n,k) in PFBrt (n+1,k); theorem :: HEYTING3:26 for n, m, k being Nat st PFArt (n,m) c= PFArt (k,m) holds n = k; theorem :: HEYTING3:27 for n, m, k being Nat holds PFCrt (n,m) c= PFArt (k,m) iff n < k; begin :: Uncompleteness theorem :: HEYTING3:28 for n, k being Nat holds PFBrt (n,k) is Element of SubstPoset (NAT, {k}); definition let k be Nat; func PFDrt k -> Subset of SubstPoset (NAT, {k}) means :: HEYTING3:def 5 for x being set holds x in it iff ex n being non empty Nat st x = PFBrt (n,k); end; theorem :: HEYTING3:29 for k being Nat holds PFBrt (1,k) = { PFArt (1,k), PFCrt (1,k) }; theorem :: HEYTING3:30 for k being Nat holds PFBrt (1,k) <> {{}}; definition let k be Nat; cluster PFBrt (1,k) -> non empty; end; theorem :: HEYTING3:31 for n, k being Nat holds { PFArt (n,k) } is Element of SubstPoset (NAT, {k}); theorem :: HEYTING3:32 for k being Nat, V, X being set, a being Element of SubstPoset (V, {k}) st X in a holds X is finite Subset of [:V, {k}:]; theorem :: HEYTING3:33 for m being Nat, a being Element of SubstPoset (NAT, {m}) st PFDrt m is_>=_than a holds for X being non empty set st X in a holds not ( for n being Nat st [n,m] in X holds n is odd ); theorem :: HEYTING3:34 for k being Nat, a, b being Element of SubstPoset (NAT, {k}), X being Subset of SubstPoset (NAT, {k}) st a is_<=_than X & b is_<=_than X holds a "\/" b is_<=_than X; definition let k be Nat; cluster non empty Element of SubstPoset (NAT, {k}); end; theorem :: HEYTING3:35 for n being Nat, a being Element of SubstPoset (NAT, {n}) st {} in a holds a = {{}}; theorem :: HEYTING3:36 for k being Nat, a being non empty Element of SubstPoset (NAT, {k}) st a <> {{}} ex f being finite Function st f in a & f <> {}; theorem :: HEYTING3:37 for k being Nat, a being non empty Element of SubstPoset (NAT, {k}), a' being Element of Fin PFuncs (NAT, {k}) st a <> {{}} & a = a' holds Involved a' is finite non empty Subset of NAT; theorem :: HEYTING3:38 for k being Nat, a being Element of SubstPoset (NAT, {k}), a' being Element of Fin PFuncs (NAT, {k}), B being finite non empty Subset of NAT st B = Involved a' & a' = a holds for X being set st X in a for l being Nat st l > max B + 1 holds not [l,k] in X; theorem :: HEYTING3:39 for k being Nat holds Top SubstPoset (NAT, {k}) = {{}}; theorem :: HEYTING3:40 for k being Nat holds Bottom SubstPoset (NAT, {k}) = {}; theorem :: HEYTING3:41 for k being Nat, a, b being Element of SubstPoset (NAT, {k}) st a <= b & a = {{}} holds b = {{}}; theorem :: HEYTING3:42 for k being Nat, a, b being Element of SubstPoset (NAT, {k}) st a <= b & b = {} holds a = {}; theorem :: HEYTING3:43 for m being Nat, a being Element of SubstPoset (NAT, {m}) st PFDrt m is_>=_than a holds a <> {{}}; definition let m be Nat; cluster SubstPoset (NAT, {m}) -> non complete; end; definition let m be Nat; cluster SubstLatt (NAT, {m}) -> non complete; end;

Back to top