HEYTING3: The Incompleteness of the Lattice of Substitutions

:: The Incompleteness of the Lattice of Substitutions
:: by Adam Grabowski
::
:: Received July 17, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users

scheme :: HEYTING3:sch 1
SSubsetUniq{ F₁() -> 1-sorted , P₁[ object ] } :

for A1, A2 being Subset of F₁() st ( for x being object holds
( x in A1 iff P₁[x] ) ) & ( for x being object holds
( x in A2 iff P₁[x] ) ) holds
A1 = A2

proof end;

Lm1: for A, x being set holds [:A,{x}:] is Function

proof end;

registration

let A, x be set ;

cluster [:A,{x}:] -> Function-like ;

coherence by Lm1;

end;

Lm2: 0 = 2 * 0
;

Lm3: 1 = 0 + 1
;

theorem Th1: :: HEYTING3:1

for X being non empty finite Subset of NAT ex n being Element of NAT st X c= (Seg n) \/ {0}

proof end;

theorem :: HEYTING3:2

for X being finite Subset of NAT holds
not for k being odd Element of NAT holds k in X

proof end;

theorem Th3: :: HEYTING3:3

for k being Element of NAT
for X being non empty finite Subset of [:NAT,{k}:] ex n being non zero Element of NAT st X c= [:((Seg n) \/ {0}),{k}:]

proof end;

theorem Th4: :: HEYTING3:4

for m being Element of NAT
for X being non empty finite Subset of [:NAT,{m}:] holds
not for k being non zero Element of NAT holds [((2 * k) + 1),m] in X

proof end;

theorem :: HEYTING3:5

for m being Element of NAT
for X being finite Subset of [:NAT,{m}:] ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X

proof end;

theorem :: HEYTING3:6

for L being upper-bounded Lattice holds Top L = Top (LattPOSet L)

proof end;

theorem :: HEYTING3:7

for L being lower-bounded Lattice holds Bottom L = Bottom (LattPOSet L)

proof end;

theorem :: HEYTING3:8

for V being set
for C being finite set
for A, B being Element of Fin (PFuncs (V,C)) st A = {} & B <> {} holds
B =>> A = {}

proof end;

theorem Th9: :: HEYTING3:9

for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
SubstitutionSet (V,C) c= SubstitutionSet (V9,C9)

proof end;

theorem Th10: :: HEYTING3:10

for V, V9, C, C9 being set
for A being Element of Fin (PFuncs (V,C))
for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds
mi A = mi B

proof end;

theorem :: HEYTING3:11

for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
the L_join of (SubstLatt (V,C)) = the L_join of (SubstLatt (V9,C9)) || the carrier of (SubstLatt (V,C))

proof end;

definition

let V, C be set ;

func SubstPoset (V,C) -> RelStr equals :: HEYTING3:def 1
LattPOSet (SubstLatt (V,C));

end;

:: deftheorem defines SubstPoset HEYTING3:def 1 :

registration

let V, C be set ;

cluster SubstPoset (V,C) -> with_suprema with_infima ;

end;

registration

let V, C be set ;

cluster SubstPoset (V,C) -> reflexive transitive antisymmetric ;

end;

theorem Th12: :: HEYTING3:12

for V, C being set
for a, b being Element of (SubstPoset (V,C)) holds
( a <= b iff for x being set st x in a holds
ex y being set st
( y in b & y c= x ) )

proof end;

theorem :: HEYTING3:13

for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9)

proof end;

definition

let n, k be Nat;

func PFArt (n,k) -> Element of PFuncs (NAT,{k}) means :Def2: :: HEYTING3:def 2
for x being object holds
( x in it iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) );

proof end;

proof end;

end;

:: deftheorem Def2 defines PFArt HEYTING3:def 2 :

registration

let n, k be Element of NAT ;

cluster PFArt (n,k) -> finite ;

proof end;

end;

definition

let n, k be Nat;

func PFCrt (n,k) -> Element of PFuncs (NAT,{k}) means :Def3: :: HEYTING3:def 3
for x being object holds
( x in it iff ex m being odd Element of NAT st
( m <= (2 * n) + 1 & [m,k] = x ) );

proof end;

proof end;

end;

:: deftheorem Def3 defines PFCrt HEYTING3:def 3 :

registration

let n, k be Element of NAT ;

cluster PFCrt (n,k) -> finite ;

proof end;

end;

theorem :: HEYTING3:14

for n, k being Element of NAT holds [((2 * n) + 1),k] in PFCrt (n,k) by Def3;

theorem Th15: :: HEYTING3:15

for n, k being Element of NAT holds PFCrt (n,k) misses {[((2 * n) + 3),k]}

proof end;

Lm4: for n being Element of NAT holds (2 * n) + 1 <= (2 * (n + 1)) + 1

proof end;

theorem Th16: :: HEYTING3:16

for n, k being Element of NAT holds PFCrt ((n + 1),k) = (PFCrt (n,k)) \/ {[((2 * n) + 3),k]}

proof end;

Lm5: for n, n9 being Element of NAT holds not PFCrt ((n + 1),n9) c= PFCrt (n,n9)

proof end;

theorem Th17: :: HEYTING3:17

for n, k being Element of NAT holds PFCrt (n,k) c< PFCrt ((n + 1),k)

proof end;

registration

let n, k be Element of NAT ;

cluster PFArt (n,k) -> non empty ;

proof end;

end;

theorem Th18: :: HEYTING3:18

for n, m, k being Element of NAT holds not PFArt (n,m) c= PFCrt (k,m)

proof end;

Lm6: for n, k being Element of NAT holds PFCrt (n,k) c= PFCrt ((n + 1),k)

proof end;

theorem :: HEYTING3:19

for n, m, k being Element of NAT st n <= k holds
PFCrt (n,m) c= PFCrt (k,m)

proof end;

Lm7: for n, m, k being Element of NAT st n < k holds
PFCrt (n,m) c= PFArt (k,m)

proof end;

theorem :: HEYTING3:20

for n being Element of NAT holds PFArt (1,n) = {[1,n],[2,n]}

proof end;

definition

let n, k be Nat;

func PFBrt (n,k) -> Element of Fin (PFuncs (NAT,{k})) means :Def4: :: HEYTING3:def 4
for x being object holds
( x in it iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) );

proof end;

proof end;

end;

:: deftheorem Def4 defines PFBrt HEYTING3:def 4 :

theorem :: HEYTING3:21

for n, k being Element of NAT
for x being set st x in PFBrt ((n + 1),k) holds
ex y being set st
( y in PFBrt (n,k) & y c= x )

proof end;

theorem :: HEYTING3:22

for n, k being Element of NAT holds not PFCrt (n,k) in PFBrt ((n + 1),k)

proof end;

Lm8: for n, k being Element of NAT
for x being set st x in PFBrt (n,k) holds
x is finite

proof end;

theorem Th23: :: HEYTING3:23

for n, m, k being Element of NAT st PFArt (n,m) c= PFArt (k,m) holds
n = k

proof end;

theorem Th24: :: HEYTING3:24

for n, m, k being Element of NAT holds
( PFCrt (n,m) c= PFArt (k,m) iff n < k )

proof end;

theorem Th25: :: HEYTING3:25

for n, k being Element of NAT holds PFBrt (n,k) is Element of (SubstPoset (NAT,{k}))

proof end;

definition

let k be Element of NAT ;

func PFDrt k -> Subset of (SubstPoset (NAT,{k})) means :Def5: :: HEYTING3:def 5
for x being object holds
( x in it iff ex n being non zero Element of NAT st x = PFBrt (n,k) );

proof end;

proof end;

end;

:: deftheorem Def5 defines PFDrt HEYTING3:def 5 :

theorem :: HEYTING3:26

for k being Element of NAT holds PFBrt (1,k) = {(PFArt (1,k)),(PFCrt (1,k))}

proof end;

theorem Th27: :: HEYTING3:27

for k being Element of NAT holds PFBrt (1,k) <> {{}}

proof end;

registration

let k be Element of NAT ;

cluster PFBrt (1,k) -> non empty ;

proof end;

end;

theorem Th28: :: HEYTING3:28

for n, k being Element of NAT holds {(PFArt (n,k))} is Element of (SubstPoset (NAT,{k}))

proof end;

theorem Th29: :: HEYTING3:29

for k being Element of NAT
for V, X being set
for a being Element of (SubstPoset (V,{k})) st X in a holds
X is finite Subset of [:V,{k}:]

proof end;

theorem Th30: :: HEYTING3:30

for m being Element of NAT
for 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
ex n being Element of NAT st
( [n,m] in X & not n is odd )

proof end;

theorem Th31: :: HEYTING3:31

for k being Element of NAT
for a, b being Element of (SubstPoset (NAT,{k}))
for X being Subset of (SubstPoset (NAT,{k})) st a is_<=_than X & b is_<=_than X holds
a "\/" b is_<=_than X

proof end;

registration

let k be Element of NAT ;

cluster non empty for Element of the carrier of (SubstPoset (NAT,{k}));

proof end;

end;

Lm9: for a being non empty set st a <> {{}} & {} in a holds
ex b being set st
( b in a & b <> {} )

proof end;

theorem Th32: :: HEYTING3:32

for n being Element of NAT
for a being Element of (SubstPoset (NAT,{n})) st {} in a holds
a = {{}}

proof end;

theorem Th33: :: HEYTING3:33

for k being Element of NAT
for a being non empty Element of (SubstPoset (NAT,{k})) st a <> {{}} holds
ex f being finite Function st
( f in a & f <> {} )

proof end;

theorem Th34: :: HEYTING3:34

for k being Element of NAT
for a being non empty Element of (SubstPoset (NAT,{k}))
for a9 being Element of Fin (PFuncs (NAT,{k})) st a <> {{}} & a = a9 holds
Involved a9 is non empty finite Subset of NAT

proof end;

theorem Th35: :: HEYTING3:35

for k being Element of NAT
for a being Element of (SubstPoset (NAT,{k}))
for a9 being Element of Fin (PFuncs (NAT,{k}))
for B being non empty finite Subset of NAT st B = Involved a9 & a9 = a holds
for X being set st X in a holds
for l being Element of NAT st l > (max B) + 1 holds
not [l,k] in X

proof end;

theorem Th36: :: HEYTING3:36

for k being Element of NAT holds Top (SubstPoset (NAT,{k})) = {{}}

proof end;

theorem Th37: :: HEYTING3:37

for k being Element of NAT holds Bottom (SubstPoset (NAT,{k})) = {}

proof end;

theorem Th38: :: HEYTING3:38

for k being Element of NAT
for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & a = {{}} holds
b = {{}}

proof end;

theorem Th39: :: HEYTING3:39

for k being Element of NAT
for a, b being Element of (SubstPoset (NAT,{k})) st a <= b & b = {} holds
a = {}

proof end;

theorem Th40: :: HEYTING3:40

for m being Element of NAT
for a being Element of (SubstPoset (NAT,{m})) st PFDrt m is_>=_than a holds
a <> {{}}

proof end;

Lm10: for m being Element of NAT holds not SubstPoset (NAT,{m}) is complete

proof end;

registration

let m be Element of NAT ;

cluster SubstPoset (NAT,{m}) -> non complete ;

coherence by Lm10;

end;

registration

let m be Element of NAT ;

cluster SubstLatt (NAT,{m}) -> non complete ;

proof end;

end;