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;