begin
theorem
canceled;
theorem Th2:
Lm1:
for A, B, C being set st A = B \/ C & A c= B holds
A = B
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem
theorem Th8:
theorem Th9:
:: deftheorem Def1 defines Involved HEYTING2:def 1 :
theorem Th10:
Lm2:
for V being set
for C being finite set
for A being non empty Element of Fin (PFuncs V,C) holds Involved A is finite
theorem Th11:
theorem Th12:
theorem
:: deftheorem defines - HEYTING2:def 2 :
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem
theorem Th19:
definition
let V be
set ;
let C be
finite set ;
let A,
B be
Element of
Fin (PFuncs V,C);
func A =>> B -> Element of
Fin (PFuncs V,C) equals
(PFuncs V,C) /\ { (union { ((f . i) \ i) where i is Element of PFuncs V,C : i in A } ) where f is Element of PFuncs A,B : dom f = A } ;
coherence
(PFuncs V,C) /\ { (union { ((f . i) \ i) where i is Element of PFuncs V,C : i in A } ) where f is Element of PFuncs A,B : dom f = A } is Element of Fin (PFuncs V,C)
end;
:: deftheorem defines =>> HEYTING2:def 3 :
theorem Th20:
Lm3:
for a, V being set
for C being finite set
for A being Element of Fin (PFuncs V,C)
for K being Element of SubstitutionSet V,C st a in A ^ (A =>> K) holds
ex b being set st
( b in K & b c= a )
theorem
Lm4:
for V being set
for C being finite set
for K being Element of SubstitutionSet V,C
for X being set st X c= K holds
X in SubstitutionSet V,C
theorem Th22:
begin
definition
let V be
set ;
let C be
finite set ;
func pseudo_compl V,
C -> UnOp of the
carrier of
(SubstLatt V,C) means :
Def4:
for
u being
Element of
(SubstLatt V,C) for
u9 being
Element of
SubstitutionSet V,
C st
u9 = u holds
it . u = mi (- u9);
existence
ex b1 being UnOp of the carrier of (SubstLatt V,C) st
for u being Element of (SubstLatt V,C)
for u9 being Element of SubstitutionSet V,C st u9 = u holds
b1 . u = mi (- u9)
correctness
uniqueness
for b1, b2 being UnOp of the carrier of (SubstLatt V,C) st ( for u being Element of (SubstLatt V,C)
for u9 being Element of SubstitutionSet V,C st u9 = u holds
b1 . u = mi (- u9) ) & ( for u being Element of (SubstLatt V,C)
for u9 being Element of SubstitutionSet V,C st u9 = u holds
b2 . u = mi (- u9) ) holds
b1 = b2;
func StrongImpl V,
C -> BinOp of the
carrier of
(SubstLatt V,C) means :
Def5:
for
u,
v being
Element of
(SubstLatt V,C) for
u9,
v9 being
Element of
SubstitutionSet V,
C st
u9 = u &
v9 = v holds
it . u,
v = mi (u9 =>> v9);
existence
ex b1 being BinOp of the carrier of (SubstLatt V,C) st
for u, v being Element of (SubstLatt V,C)
for u9, v9 being Element of SubstitutionSet V,C st u9 = u & v9 = v holds
b1 . u,v = mi (u9 =>> v9)
correctness
uniqueness
for b1, b2 being BinOp of the carrier of (SubstLatt V,C) st ( for u, v being Element of (SubstLatt V,C)
for u9, v9 being Element of SubstitutionSet V,C st u9 = u & v9 = v holds
b1 . u,v = mi (u9 =>> v9) ) & ( for u, v being Element of (SubstLatt V,C)
for u9, v9 being Element of SubstitutionSet V,C st u9 = u & v9 = v holds
b2 . u,v = mi (u9 =>> v9) ) holds
b1 = b2;
let u be
Element of
(SubstLatt V,C);
func SUB u -> Element of
Fin the
carrier of
(SubstLatt V,C) equals
bool u;
coherence
bool u is Element of Fin the carrier of (SubstLatt V,C)
correctness
;
func diff u -> UnOp of the
carrier of
(SubstLatt V,C) means :
Def7:
for
v being
Element of
(SubstLatt V,C) holds
it . v = u \ v;
existence
ex b1 being UnOp of the carrier of (SubstLatt V,C) st
for v being Element of (SubstLatt V,C) holds b1 . v = u \ v
correctness
uniqueness
for b1, b2 being UnOp of the carrier of (SubstLatt V,C) st ( for v being Element of (SubstLatt V,C) holds b1 . v = u \ v ) & ( for v being Element of (SubstLatt V,C) holds b2 . v = u \ v ) holds
b1 = b2;
end;
:: deftheorem Def4 defines pseudo_compl HEYTING2:def 4 :
:: deftheorem Def5 defines StrongImpl HEYTING2:def 5 :
:: deftheorem defines SUB HEYTING2:def 6 :
:: deftheorem Def7 defines diff HEYTING2:def 7 :
Lm5:
for V being set
for C being finite set
for v, u being Element of (SubstLatt V,C) st v in SUB u holds
v "\/" ((diff u) . v) = u
Lm6:
for V being set
for C being finite set
for u being Element of (SubstLatt V,C)
for a being Element of PFuncs V,C
for K being Element of Fin (PFuncs V,C) st K = {a} holds
ex v being Element of SubstitutionSet V,C st
( v in SUB u & v ^ K = {} & ( for b being Element of PFuncs V,C st b in (diff u) . v holds
b tolerates a ) )
definition
let V be
set ;
let C be
finite set ;
func Atom V,
C -> Function of
(PFuncs V,C),the
carrier of
(SubstLatt V,C) means :
Def8:
for
a being
Element of
PFuncs V,
C holds
it . a = mi {.a.};
existence
ex b1 being Function of (PFuncs V,C),the carrier of (SubstLatt V,C) st
for a being Element of PFuncs V,C holds b1 . a = mi {.a.}
correctness
uniqueness
for b1, b2 being Function of (PFuncs V,C),the carrier of (SubstLatt V,C) st ( for a being Element of PFuncs V,C holds b1 . a = mi {.a.} ) & ( for a being Element of PFuncs V,C holds b2 . a = mi {.a.} ) holds
b1 = b2;
end;
:: deftheorem Def8 defines Atom HEYTING2:def 8 :
Lm7:
for V being set
for C being finite set
for a being Element of PFuncs V,C st a is finite holds
(Atom V,C) . a = {a}
theorem Th23:
theorem Th24:
Lm8:
for V being set
for C being finite set
for u, v being Element of (SubstLatt V,C) st ( for a being set st a in u holds
ex b being set st
( b in v & b c= a ) ) holds
u [= v
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
Lm9:
for V being set
for C being finite set
for u, v being Element of (SubstLatt V,C) st u [= v holds
for x being set st x in u holds
ex b being set st
( b in v & b c= x )
theorem Th29:
theorem Th30:
deffunc H1( set , set ) -> Element of bool [:[:the carrier of (SubstLatt $1,$2),the carrier of (SubstLatt $1,$2):],the carrier of (SubstLatt $1,$2):] = the L_meet of (SubstLatt $1,$2);
theorem Th31:
theorem Th32:
Lm10:
now
let V be
set ;
for C being finite set
for u, v being Element of (SubstLatt V,C) holds
( u "/\" H2(u,v) [= v & ( for w being Element of (SubstLatt V,C) st u "/\" v [= w holds
v [= H2(u,w) ) )let C be
finite set ;
for u, v being Element of (SubstLatt V,C) holds
( u "/\" H2(u,v) [= v & ( for w being Element of (SubstLatt V,C) st u "/\" v [= w holds
v [= H2(u,w) ) )let u,
v be
Element of
(SubstLatt V,C);
( u "/\" H2(u,v) [= v & ( for w being Element of (SubstLatt V,C) st u "/\" v [= w holds
v [= H2(u,w) ) )deffunc H2(
Element of
(SubstLatt V,C),
Element of
(SubstLatt V,C))
-> Element of the
carrier of
(SubstLatt V,C) =
FinJoin (SUB $1),
(H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff $1),$2));
set Psi =
H1(
V,
C)
.: (pseudo_compl V,C),
((StrongImpl V,C) [:] (diff u),v);
reconsider v9 =
v as
Element of
SubstitutionSet V,
C by SUBSTLAT:def 4;
A1:
now
let w be
Element of
(SubstLatt V,C);
( w in SUB u implies (H1(V,C) [;] u,(H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),v))) . w [= v )set u2 =
(diff u) . w;
set pc =
(pseudo_compl V,C) . w;
set si =
(StrongImpl V,C) . ((diff u) . w),
v;
A2:
w "/\" (((pseudo_compl V,C) . w) "/\" ((StrongImpl V,C) . ((diff u) . w),v)) =
(w "/\" ((pseudo_compl V,C) . w)) "/\" ((StrongImpl V,C) . ((diff u) . w),v)
by LATTICES:def 7
.=
(Bottom (SubstLatt V,C)) "/\" ((StrongImpl V,C) . ((diff u) . w),v)
by Th31
.=
Bottom (SubstLatt V,C)
by LATTICES:40
;
assume
w in SUB u
;
(H1(V,C) [;] u,(H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),v))) . w [= vthen A3:
w "\/" ((diff u) . w) = u
by Lm5;
(H1(V,C) [;] u,(H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),v))) . w =
H1(
V,
C)
. u,
((H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),v)) . w)
by FUNCOP_1:66
.=
u "/\" ((H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),v)) . w)
by LATTICES:def 2
.=
u "/\" (H1(V,C) . ((pseudo_compl V,C) . w),(((StrongImpl V,C) [:] (diff u),v) . w))
by FUNCOP_1:48
.=
u "/\" (((pseudo_compl V,C) . w) "/\" (((StrongImpl V,C) [:] (diff u),v) . w))
by LATTICES:def 2
.=
u "/\" (((pseudo_compl V,C) . w) "/\" ((StrongImpl V,C) . ((diff u) . w),v))
by FUNCOP_1:60
.=
(w "/\" (((pseudo_compl V,C) . w) "/\" ((StrongImpl V,C) . ((diff u) . w),v))) "\/" (((diff u) . w) "/\" (((pseudo_compl V,C) . w) "/\" ((StrongImpl V,C) . ((diff u) . w),v)))
by A3, LATTICES:def 11
.=
((diff u) . w) "/\" (((StrongImpl V,C) . ((diff u) . w),v) "/\" ((pseudo_compl V,C) . w))
by A2, LATTICES:39
.=
(((diff u) . w) "/\" ((StrongImpl V,C) . ((diff u) . w),v)) "/\" ((pseudo_compl V,C) . w)
by LATTICES:def 7
;
then A4:
(H1(V,C) [;] u,(H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),v))) . w [= ((diff u) . w) "/\" ((StrongImpl V,C) . ((diff u) . w),v)
by LATTICES:23;
((diff u) . w) "/\" ((StrongImpl V,C) . ((diff u) . w),v) [= v
by Th32;
hence
(H1(V,C) [;] u,(H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),v))) . w [= v
by A4, LATTICES:25;
verum
end;
u "/\" H2(
u,
v)
= FinJoin (SUB u),
(H1(V,C) [;] u,(H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),v)))
by LATTICE2:83;
hence
u "/\" H2(
u,
v)
[= v
by A1, LATTICE2:70;
for w being Element of (SubstLatt V,C) st u "/\" v [= w holds
v [= H2(u,w)let w be
Element of
(SubstLatt V,C);
( u "/\" v [= w implies v [= H2(u,w) )assume A5:
u "/\" v [= w
;
v [= H2(u,w)A6:
v = FinJoin v9,
(Atom V,C)
by Th24;
then A7:
u "/\" v = FinJoin v9,
(H1(V,C) [;] u,(Atom V,C))
by LATTICE2:83;
now
set pf =
pseudo_compl V,
C;
set sf =
(StrongImpl V,C) [:] (diff u),
w;
let a be
Element of
PFuncs V,
C;
( a in v9 implies (Atom V,C) . a [= H2(u,w) )reconsider SA =
{.a.} as
Element of
Fin (PFuncs V,C) ;
consider v being
Element of
SubstitutionSet V,
C such that A8:
v in SUB u
and A9:
v ^ SA = {}
and A10:
for
b being
Element of
PFuncs V,
C st
b in (diff u) . v holds
b tolerates a
by Lm6;
assume A11:
a in v9
;
(Atom V,C) . a [= H2(u,w)then A12:
a is
finite
by Th2;
reconsider v9 =
v as
Element of
(SubstLatt V,C) by SUBSTLAT:def 4;
set dv =
(diff u) . v9;
(H1(V,C) [;] u,(Atom V,C)) . a [= w
by A7, A5, A11, LATTICE2:46;
then
H1(
V,
C)
. u,
((Atom V,C) . a) [= w
by FUNCOP_1:66;
then A13:
u "/\" ((Atom V,C) . a) [= w
by LATTICES:def 2;
a is
finite
by A11, Th2;
then reconsider SS =
{a} as
Element of
SubstitutionSet V,
C by Th6;
v ^ SS = {}
by A9;
then A14:
(Atom V,C) . a [= (pseudo_compl V,C) . v9
by Th27;
((diff u) . v9) "/\" ((Atom V,C) . a) [= u "/\" ((Atom V,C) . a)
by Th25, LATTICES:27;
then
((diff u) . v9) "/\" ((Atom V,C) . a) [= w
by A13, LATTICES:25;
then
(Atom V,C) . a [= (StrongImpl V,C) . ((diff u) . v9),
w
by A10, A12, Th30;
then A15:
(Atom V,C) . a [= ((StrongImpl V,C) [:] (diff u),w) . v9
by FUNCOP_1:60;
((pseudo_compl V,C) . v9) "/\" (((StrongImpl V,C) [:] (diff u),w) . v9) =
H1(
V,
C)
. ((pseudo_compl V,C) . v9),
(((StrongImpl V,C) [:] (diff u),w) . v9)
by LATTICES:def 2
.=
(H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),w)) . v9
by FUNCOP_1:48
;
then
(Atom V,C) . a [= (H1(V,C) .: (pseudo_compl V,C),((StrongImpl V,C) [:] (diff u),w)) . v9
by A14, A15, FILTER_0:7;
hence
(Atom V,C) . a [= H2(
u,
w)
by A8, LATTICE2:44;
verum
end;
hence
v [= H2(
u,
w)
by A6, LATTICE2:70;
verum
end;
Lm11:
for V being set
for C being finite set holds SubstLatt V,C is implicative
theorem