:: QUANTAL1 semantic presentation

scheme :: QUANTAL1:sch 1
DenestFraenkel{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> set , F₄( set ) -> Element of F₂(), P₁[ set ] } :

{ F₃(a) where a is Element of F₂() : a in { F₄(b) where b is Element of F₁() : P₁[b] } } = { F₃(F₄(a)) where a is Element of F₁() : P₁[a] }

proof end;

scheme :: QUANTAL1:sch 2
EmptyFraenkel{ F₁() -> non empty set , F₂( set ) -> set , P₁[ set ] } :

{ F₂(a) where a is Element of F₁() : P₁[a] } = {}

provided

A1: for a being Element of F₁() holds P₁[a]

proof end;

deffunc H₁( non empty LattStr ) -> set = the carrier of $1;

deffunc H₂( LattStr ) -> M5([:the carrier of $1,the carrier of $1:],the carrier of $1) = the L_join of $1;

deffunc H₃( LattStr ) -> M5([:the carrier of $1,the carrier of $1:],the carrier of $1) = the L_meet of $1;

deffunc H₄( HGrStr ) -> M5([:the carrier of $1,the carrier of $1:],the carrier of $1) = the mult of $1;

theorem Th1: :: QUANTAL1:1

for L1, L2 being non empty LattStr st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )

proof end;

theorem Th2: :: QUANTAL1:2

for L1, L2 being non empty LattStr st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) holds
for a being Element of L1
for b being Element of L2
for X being set st a = b holds
( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_great_than X implies b is_great_than X ) & ( b is_great_than X implies a is_great_than X ) )

proof end;

definition

let L be 1-sorted ;
mode UnOp of L is Function of L,L;

end;

definition

let L be non empty LattStr ;
let X be Subset of L;
attr X is directed means :: QUANTAL1:def 1
for Y being finite Subset of X ex x being Element of L st
( "\/" Y,L [= x & x in X );

end;

:: deftheorem defines directed QUANTAL1:def 1 :

theorem :: QUANTAL1:3

for L being non empty LattStr
for X being Subset of L st X is directed holds
not X is empty

proof end;

definition

attr c₁ is strict;
struct QuantaleStr -> LattStr , HGrStr ;
aggr QuantaleStr(# carrier, L_join, L_meet, mult #) -> QuantaleStr ;

end;

registration

cluster non empty QuantaleStr ;
existence

proof end;

end;

definition

attr c₁ is strict;
struct QuasiNetStr -> QuantaleStr , multLoopStr ;
aggr QuasiNetStr(# carrier, L_join, L_meet, mult, unity #) -> QuasiNetStr ;

end;

registration

cluster non empty QuasiNetStr ;
existence

proof end;

end;

definition

let IT be non empty HGrStr ;
attr IT is with_left-zero means :: QUANTAL1:def 2
ex a being Element of IT st
for b being Element of IT holds a * b = a;
attr IT is with_right-zero means :: QUANTAL1:def 3
ex b being Element of IT st
for a being Element of IT holds a * b = b;

end;

:: deftheorem defines with_left-zero QUANTAL1:def 2 :

:: deftheorem defines with_right-zero QUANTAL1:def 3 :

definition

let IT be non empty HGrStr ;
attr IT is with_zero means :Def4: :: QUANTAL1:def 4
( IT is with_left-zero & IT is with_right-zero );

end;

:: deftheorem Def4 defines with_zero QUANTAL1:def 4 :

registration

cluster non empty with_zero -> non empty with_left-zero with_right-zero HGrStr ;
coherence by Def4;
cluster non empty with_left-zero with_right-zero -> non empty with_zero HGrStr ;
coherence by Def4;

end;

registration

cluster non empty with_left-zero with_right-zero with_zero HGrStr ;
existence

proof end;

end;

definition

let IT be non empty QuantaleStr ;
attr IT is right-distributive means :Def5: :: QUANTAL1:def 5
for a being Element of IT
for X being set holds a [*] ("\/" X,IT) = "\/" { (a [*] b) where b is Element of IT : b in X } ,IT;
attr IT is left-distributive means :Def6: :: QUANTAL1:def 6
for a being Element of IT
for X being set holds ("\/" X,IT) [*] a = "\/" { (b [*] a) where b is Element of IT : b in X } ,IT;
attr IT is times-additive means :: QUANTAL1:def 7
for a, b, c being Element of IT holds
( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) );
attr IT is times-continuous means :: QUANTAL1:def 8
for X1, X2 being Subset of IT st X1 is directed & X2 is directed holds
("\/" X1) [*] ("\/" X2) = "\/" { (a [*] b) where a, b is Element of IT : ( a in X1 & b in X2 ) } ,IT;

end;

:: deftheorem Def5 defines right-distributive QUANTAL1:def 5 :

:: deftheorem Def6 defines left-distributive QUANTAL1:def 6 :

:: deftheorem defines times-additive QUANTAL1:def 7 :

:: deftheorem defines times-continuous QUANTAL1:def 8 :

theorem Th4: :: QUANTAL1:4

for Q being non empty QuantaleStr st LattStr(# the carrier of Q,the L_join of Q,the L_meet of Q #) = BooleLatt {} holds
( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )

proof end;

registration

let A be non empty set ;
let b1, b2, b3 be BinOp of A;
cluster QuantaleStr(# A,b1,b2,b3 #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty Lattice-like complete unital associative commutative with_left-zero with_right-zero with_zero right-distributive left-distributive QuantaleStr ;
existence

proof end;

end;

scheme :: QUANTAL1:sch 3
LUBFraenkelDistr{ F₁() -> non empty Lattice-like complete QuantaleStr , F₂( set , set ) -> Element of F₁(), F₃() -> set , F₄() -> set } :

"\/" { ("\/" { F₂(a,b) where b is Element of F₁() : b in F₄() } ,F₁()) where a is Element of F₁() : a in F₃() } ,F₁() = "\/" { F₂(a,b) where a, b is Element of F₁() : ( a in F₃() & b in F₄() ) } ,F₁()

proof end;

theorem Th5: :: QUANTAL1:5

for Q being non empty Lattice-like complete right-distributive left-distributive QuantaleStr
for X, Y being set holds ("\/" X,Q) [*] ("\/" Y,Q) = "\/" { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q

proof end;

theorem Th6: :: QUANTAL1:6

for Q being non empty Lattice-like complete right-distributive left-distributive QuantaleStr
for a, b, c being Element of Q holds
( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) )

proof end;

registration

let A be non empty set ;
let b1, b2, b3 be BinOp of A;
let e be Element of A;
cluster QuasiNetStr(# A,b1,b2,b3,e #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty Lattice-like complete QuasiNetStr ;
existence

proof end;

end;

registration

cluster non empty Lattice-like complete right-distributive left-distributive -> non empty Lattice-like complete times-additive times-continuous QuasiNetStr ;
coherence

proof end;

end;

registration

cluster non empty Lattice-like complete unital associative commutative with_left-zero with_right-zero with_zero right-distributive left-distributive times-additive times-continuous QuasiNetStr ;
existence

proof end;

end;

definition

mode Quantale is non empty Lattice-like complete associative right-distributive left-distributive QuantaleStr ;
mode QuasiNet is non empty Lattice-like complete unital associative with_left-zero times-additive times-continuous QuasiNetStr ;

end;

definition

mode BlikleNet is non empty with_zero QuasiNet;

end;

theorem :: QUANTAL1:7

for Q being non empty unital QuasiNetStr st Q is Quantale holds
Q is BlikleNet

proof end;

theorem Th8: :: QUANTAL1:8

for Q being Quantale
for a, b, c being Element of Q st a [= b holds
( a [*] c [= b [*] c & c [*] a [= c [*] b )

proof end;

theorem Th9: :: QUANTAL1:9

for Q being Quantale
for a, b, c, d being Element of Q st a [= b & c [= d holds
a [*] c [= b [*] d

proof end;

definition

let f be Function;
attr f is idempotent means :: QUANTAL1:def 9
f * f = f;

end;

:: deftheorem defines idempotent QUANTAL1:def 9 :

Lm1: for A being non empty set
for f being UnOp of A st f is idempotent holds
for a being Element of A holds f . (f . a) = f . a

proof end;

definition

let L be non empty LattStr ;
let IT be UnOp of L;
attr IT is inflationary means :: QUANTAL1:def 10
for p being Element of L holds p [= IT . p;
attr IT is deflationary means :: QUANTAL1:def 11
for p being Element of L holds IT . p [= p;
attr IT is monotone means :Def12: :: QUANTAL1:def 12
for p, q being Element of L st p [= q holds
IT . p [= IT . q;
attr IT is \/-distributive means :: QUANTAL1:def 13
for X being Subset of L holds IT . ("\/" X) [= "\/" { (IT . a) where a is Element of L : a in X } ,L;

end;

:: deftheorem defines inflationary QUANTAL1:def 10 :

:: deftheorem defines deflationary QUANTAL1:def 11 :

:: deftheorem Def12 defines monotone QUANTAL1:def 12 :

:: deftheorem defines \/-distributive QUANTAL1:def 13 :

registration

let L be Lattice;
cluster inflationary deflationary monotone M4(the carrier of L,the carrier of L);
existence

proof end;

end;

theorem Th10: :: QUANTAL1:10

for L being complete Lattice
for j being UnOp of L st j is monotone holds
( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" { (j . a) where a is Element of L : a in X } ,L )

proof end;

definition

let Q be non empty QuantaleStr ;
let IT be UnOp of Q;
attr IT is times-monotone means :: QUANTAL1:def 14
for a, b being Element of Q holds (IT . a) [*] (IT . b) [= IT . (a [*] b);

end;

:: deftheorem defines times-monotone QUANTAL1:def 14 :

definition

let Q be non empty QuantaleStr ;
let a, b be Element of Q;
func a -r> b -> Element of Q equals :: QUANTAL1:def 15
"\/" { c where c is Element of Q : c [*] a [= b } ,Q;
correctness ;
func a -l> b -> Element of Q equals :: QUANTAL1:def 16
"\/" { c where c is Element of Q : a [*] c [= b } ,Q;
correctness ;

end;

:: deftheorem defines -r> QUANTAL1:def 15 :

:: deftheorem defines -l> QUANTAL1:def 16 :

theorem Th11: :: QUANTAL1:11

for Q being Quantale
for a, b, c being Element of Q holds
( a [*] b [= c iff b [= a -l> c )

proof end;

theorem Th12: :: QUANTAL1:12

for Q being Quantale
for a, b, c being Element of Q holds
( a [*] b [= c iff a [= b -r> c )

proof end;

theorem Th13: :: QUANTAL1:13

for Q being Quantale
for s, a, b being Element of Q st a [= b holds
( b -r> s [= a -r> s & b -l> s [= a -l> s )

proof end;

theorem :: QUANTAL1:14

for Q being Quantale
for s being Element of Q
for j being UnOp of Q st ( for a being Element of Q holds j . a = (a -r> s) -r> s ) holds
j is monotone

proof end;

definition

let Q be non empty QuantaleStr ;
let IT be Element of Q;
attr IT is dualizing means :Def17: :: QUANTAL1:def 17
for a being Element of Q holds
( (a -r> IT) -l> IT = a & (a -l> IT) -r> IT = a );
attr IT is cyclic means :Def18: :: QUANTAL1:def 18
for a being Element of Q holds a -r> IT = a -l> IT;

end;

:: deftheorem Def17 defines dualizing QUANTAL1:def 17 :

:: deftheorem Def18 defines cyclic QUANTAL1:def 18 :

theorem Th15: :: QUANTAL1:15

for Q being Quantale
for c being Element of Q holds
( c is cyclic iff for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c )

proof end;

theorem Th16: :: QUANTAL1:16

for Q being Quantale
for s, a being Element of Q st s is cyclic holds
( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s )

proof end;

theorem :: QUANTAL1:17

for Q being Quantale
for s, a being Element of Q st s is cyclic holds
( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s )

proof end;

theorem :: QUANTAL1:18

for Q being Quantale
for s, a, b being Element of Q st s is cyclic holds
((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s

proof end;

theorem Th19: :: QUANTAL1:19

for Q being Quantale
for D being Element of Q st D is dualizing holds
( Q is unital & the_unity_wrt the mult of Q = D -r> D & the_unity_wrt the mult of Q = D -l> D )

proof end;

theorem :: QUANTAL1:20

for Q being Quantale
for a, b, c being Element of Q st a is dualizing holds
( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a )

proof end;

definition

attr c₁ is strict;
struct Girard-QuantaleStr -> QuasiNetStr ;
aggr Girard-QuantaleStr(# carrier, L_join, L_meet, mult, unity, absurd #) -> Girard-QuantaleStr ;
sel absurd c₁ -> Element of the carrier of c₁;

end;

registration

cluster non empty Girard-QuantaleStr ;
existence

proof end;

end;

definition

let IT be non empty Girard-QuantaleStr ;
attr IT is cyclic means :Def19: :: QUANTAL1:def 19
the absurd of IT is cyclic;
attr IT is dualized means :Def20: :: QUANTAL1:def 20
the absurd of IT is dualizing;

end;

:: deftheorem Def19 defines cyclic QUANTAL1:def 19 :

:: deftheorem Def20 defines dualized QUANTAL1:def 20 :

theorem Th21: :: QUANTAL1:21

for Q being non empty Girard-QuantaleStr st LattStr(# the carrier of Q,the L_join of Q,the L_meet of Q #) = BooleLatt {} holds
( Q is cyclic & Q is dualized )

proof end;

registration

let A be non empty set ;
let b1, b2, b3 be BinOp of A;
let e1, e2 be Element of A;
cluster Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty Lattice-like complete unital associative commutative right-distributive left-distributive times-additive times-continuous strict cyclic dualized Girard-QuantaleStr ;
existence

proof end;

end;

definition

mode Girard-Quantale is non empty Lattice-like complete unital associative right-distributive left-distributive cyclic dualized Girard-QuantaleStr ;

end;

definition

let G be Girard-QuantaleStr ;
func Bottom G -> Element of G equals :: QUANTAL1:def 21
the absurd of G;
correctness ;

end;

:: deftheorem defines Bottom QUANTAL1:def 21 :

definition

let G be non empty Girard-QuantaleStr ;
func Top G -> Element of G equals :: QUANTAL1:def 22
(Bottom G) -r> (Bottom G);
correctness ;
let a be Element of G;
func Bottom a -> Element of G equals :: QUANTAL1:def 23
a -r> (Bottom G);
correctness ;

end;

:: deftheorem defines Top QUANTAL1:def 22 :

:: deftheorem defines Bottom QUANTAL1:def 23 :

definition

let G be non empty Girard-QuantaleStr ;
func Negation G -> UnOp of G means :: QUANTAL1:def 24
for a being Element of G holds it . a = Bottom a;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines Negation QUANTAL1:def 24 :

definition

let G be non empty Girard-QuantaleStr ;
let u be UnOp of G;
func Bottom u -> UnOp of G equals :: QUANTAL1:def 25
(Negation G) * u;
correctness ;

end;

:: deftheorem defines Bottom QUANTAL1:def 25 :

definition

let G be non empty Girard-QuantaleStr ;
let o be BinOp of G;
func Bottom o -> BinOp of G equals :: QUANTAL1:def 26
(Negation G) * o;
correctness ;

end;

:: deftheorem defines Bottom QUANTAL1:def 26 :

theorem Th22: :: QUANTAL1:22

for Q being Girard-Quantale
for a being Element of Q holds Bottom (Bottom a) = a

proof end;

theorem Th23: :: QUANTAL1:23

for Q being Girard-Quantale
for a, b being Element of Q st a [= b holds
Bottom b [= Bottom a by Th13;

theorem Th24: :: QUANTAL1:24

for Q being Girard-Quantale
for X being set holds Bottom ("\/" X,Q) = "/\" { (Bottom a) where a is Element of Q : a in X } ,Q

proof end;

theorem Th25: :: QUANTAL1:25

for Q being Girard-Quantale
for X being set holds Bottom ("/\" X,Q) = "\/" { (Bottom a) where a is Element of Q : a in X } ,Q

proof end;

theorem Th26: :: QUANTAL1:26

for Q being Girard-Quantale
for a, b being Element of Q holds
( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) )

proof end;

definition

let Q be Girard-Quantale;
let a, b be Element of Q;
func a delta b -> Element of Q equals :: QUANTAL1:def 27
Bottom ((Bottom a) [*] (Bottom b));
correctness ;

end;

:: deftheorem defines delta QUANTAL1:def 27 :

theorem :: QUANTAL1:27

for Q being Girard-Quantale
for a being Element of Q
for X being set holds
( a [*] ("\/" X,Q) = "\/" { (a [*] b) where b is Element of Q : b in X } ,Q & a delta ("/\" X,Q) = "/\" { (a delta c) where c is Element of Q : c in X } ,Q )

proof end;

theorem :: QUANTAL1:28

for Q being Girard-Quantale
for a being Element of Q
for X being set holds
( ("\/" X,Q) [*] a = "\/" { (b [*] a) where b is Element of Q : b in X } ,Q & ("/\" X,Q) delta a = "/\" { (c delta a) where c is Element of Q : c in X } ,Q )

proof end;

theorem :: QUANTAL1:29

for Q being Girard-Quantale
for a, b, c being Element of Q holds
( a delta (b "/\" c) = (a delta b) "/\" (a delta c) & (b "/\" c) delta a = (b delta a) "/\" (c delta a) )

proof end;

theorem :: QUANTAL1:30

for Q being Girard-Quantale
for a1, b1, a2, b2 being Element of Q st a1 [= b1 & a2 [= b2 holds
a1 delta a2 [= b1 delta b2

proof end;

theorem :: QUANTAL1:31

for Q being Girard-Quantale
for a, b, c being Element of Q holds (a delta b) delta c = a delta (b delta c)

proof end;

theorem Th32: :: QUANTAL1:32

for Q being Girard-Quantale
for a being Element of Q holds
( a [*] (Top Q) = a & (Top Q) [*] a = a )

proof end;

theorem :: QUANTAL1:33

for Q being Girard-Quantale
for a being Element of Q holds
( a delta (Bottom Q) = a & (Bottom Q) delta a = a )

proof end;

theorem :: QUANTAL1:34

for Q being Quantale
for j being UnOp of Q st j is monotone & j is idempotent & j is \/-distributive holds
ex L being complete Lattice st
( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" X,Q) ) )

proof end;