:: Kleene Algebra of Partial Predicates :: by Artur Korni{\l}owicz , Ievgen Ivanov and Mykola Nikitchenko :: :: Received March 27, 2018 :: Copyright (c) 2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies PARTPR_1, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1, MARGREL1, XBOOLEAN, TARSKI, MONOID_0, FUNCOP_1, ZFMISC_1, BINOP_1, LATTICES, EQREL_1, XXREAL_2, ROBBINS1, PBOOLE, STRUCT_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MARGREL1, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, STRUCT_0, MONOID_0, LATTICES, ROBBINS1; constructors RFUNCT_3, RELSET_1, MARGREL1, LATTICES, MONOID_0, ROBBINS1; registrations XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, RELSET_1, NAT_1, MONOID_0, LATTICES, ROBBINS1; requirements NUMERALS, BOOLE, SUBSET; begin :: Partial predicates reserve x for object; reserve D for set; definition let D; func Pr(D) -> set equals :: PARTPR_1:def 1 PFuncs(D,BOOLEAN); end; registration let D; cluster Pr(D) -> non empty functional; end; definition let D; mode PartialPredicate of D is PartFunc of D,BOOLEAN; end; reserve p for PartialPredicate of D; theorem :: PARTPR_1:1 x in Pr(D) implies x is PartialPredicate of D; theorem :: PARTPR_1:2 p in Pr(D); theorem :: PARTPR_1:3 p.x = TRUE or p.x = FALSE; definition let D; func PPnegation(D) -> Function of Pr(D),Pr(D) means :: PARTPR_1:def 2 for p being PartialPredicate of D holds dom(it.p) = dom p & for d being object holds (d in dom p & p.d = TRUE implies it.p.d = FALSE) & (d in dom p & p.d = FALSE implies it.p.d = TRUE); end; definition let D,p; func PP_not(p) -> PartialPredicate of D equals :: PARTPR_1:def 3 PPnegation(D).p; involutiveness; end; theorem :: PARTPR_1:4 x in dom p & PP_not(p).x = FALSE implies p.x = TRUE; theorem :: PARTPR_1:5 x in dom p & PP_not(p).x = TRUE implies p.x = FALSE; theorem :: PARTPR_1:6 x in dom PP_not(p) & PP_not(p).x = FALSE implies x in dom p & p.x = TRUE; theorem :: PARTPR_1:7 x in dom PP_not(p) & PP_not(p).x = TRUE implies x in dom p & p.x = FALSE; reserve D for non empty set; reserve p,q,r for PartialPredicate of D; definition let D; func PPdisjunction(D) -> Function of [:Pr(D),Pr(D):],Pr(D) means :: PARTPR_1:def 4 for p,q being PartialPredicate of D holds dom(it.(p,q)) = {d where d is Element of D: d in dom p & p.d = TRUE or d in dom q & q.d = TRUE or d in dom p & p.d = FALSE & d in dom q & q.d = FALSE} & for d being object holds (d in dom p & p.d = TRUE or d in dom q & q.d = TRUE implies it.(p,q).d = TRUE) & (d in dom p & p.d = FALSE & d in dom q & q.d = FALSE implies it.(p,q).d = FALSE); end; definition let D,p,q; func PP_or(p,q) -> PartialPredicate of D equals :: PARTPR_1:def 5 PPdisjunction(D).(p,q); commutativity; idempotence; end; theorem :: PARTPR_1:8 x in dom(PP_or(p,q)) implies x in dom p & p.x = TRUE or x in dom q & q.x = TRUE or x in dom p & p.x = FALSE & x in dom q & q.x = FALSE; theorem :: PARTPR_1:9 x in dom p & x in dom q & PP_or(p,q).x = TRUE implies p.x = TRUE or q.x = TRUE; theorem :: PARTPR_1:10 x in dom PP_or(p,q) & PP_or(p,q).x = TRUE implies x in dom p & p.x = TRUE or x in dom q & q.x = TRUE; theorem :: PARTPR_1:11 x in dom p & PP_or(p,q).x = FALSE implies p.x = FALSE; theorem :: PARTPR_1:12 x in dom q & PP_or(p,q).x = FALSE implies q.x = FALSE; theorem :: PARTPR_1:13 x in dom PP_or(p,q) & PP_or(p,q).x = FALSE implies x in dom p & p.x = FALSE & x in dom q & q.x = FALSE; ::\$N Associativity law theorem :: PARTPR_1:14 PP_or(p,PP_or(q,r)) = PP_or(PP_or(p,q),r); theorem :: PARTPR_1:15 PP_or(PP_or(p,q),PP_or(p,r)) = PP_or(PP_or(p,q),r); definition let D,p,q; func PP_and(p,q) -> PartialPredicate of D equals :: PARTPR_1:def 6 PP_not PP_or(PP_not(p),PP_not(q)); commutativity; idempotence; func PP_imp(p,q) -> PartialPredicate of D equals :: PARTPR_1:def 7 PP_or(PP_not(p),q); end; theorem :: PARTPR_1:16 dom(PP_and(p,q)) = {d where d is Element of D: d in dom p & p.d = FALSE or d in dom q & q.d = FALSE or d in dom p & p.d = TRUE & d in dom q & q.d = TRUE}; theorem :: PARTPR_1:17 x in dom(PP_and(p,q)) implies x in dom p & p.x = FALSE or x in dom q & q.x = FALSE or x in dom p & p.x = TRUE & x in dom q & q.x = TRUE; theorem :: PARTPR_1:18 x in dom p & p.x = TRUE & x in dom q & q.x = TRUE implies PP_and(p,q).x = TRUE; theorem :: PARTPR_1:19 x in dom p & p.x = FALSE implies PP_and(p,q).x = FALSE; theorem :: PARTPR_1:20 x in dom q & q.x = FALSE implies PP_and(p,q).x = FALSE; theorem :: PARTPR_1:21 x in dom p & PP_and(p,q).x = TRUE implies p.x = TRUE; theorem :: PARTPR_1:22 x in dom q & PP_and(p,q).x = TRUE implies q.x = TRUE; theorem :: PARTPR_1:23 x in dom PP_and(p,q) & PP_and(p,q).x = TRUE implies x in dom p & p.x = TRUE & x in dom q & q.x = TRUE; theorem :: PARTPR_1:24 x in dom p & x in dom q & PP_and(p,q).x = FALSE implies p.x = FALSE or q.x = FALSE; theorem :: PARTPR_1:25 x in dom PP_and(p,q) & PP_and(p,q).x = FALSE implies x in dom p & p.x = FALSE or x in dom q & q.x = FALSE; ::\$N Associativity law theorem :: PARTPR_1:26 PP_and(p,PP_and(q,r)) = PP_and(PP_and(p,q),r); theorem :: PARTPR_1:27 PP_and(PP_and(p,q),PP_and(p,r)) = PP_and(PP_and(p,q),r); ::\$N Meet-absorbing law theorem :: PARTPR_1:28 PP_or(PP_and(p,q),q) = q; ::\$N Join-absorbing law theorem :: PARTPR_1:29 PP_and(p,PP_or(p,q)) = p; ::\$N Distributivity law theorem :: PARTPR_1:30 PP_and(p,PP_or(q,r)) = PP_or(PP_and(p,q),PP_and(p,r)); theorem :: PARTPR_1:31 dom(PP_imp(p,q)) = {d where d is Element of D: d in dom p & p.d = FALSE or d in dom q & q.d = TRUE or d in dom p & p.d = TRUE & d in dom q & q.d = FALSE}; theorem :: PARTPR_1:32 x in dom(PP_imp(p,q)) implies x in dom p & p.x = FALSE or x in dom q & q.x = TRUE or x in dom p & p.x = TRUE & x in dom q & q.x = FALSE; theorem :: PARTPR_1:33 x in dom p & p.x = FALSE implies PP_imp(p,q).x = TRUE; theorem :: PARTPR_1:34 x in dom q & q.x = TRUE implies PP_imp(p,q).x = TRUE; theorem :: PARTPR_1:35 x in dom p & p.x = TRUE & x in dom q & q.x = FALSE implies PP_imp(p,q).x = FALSE; theorem :: PARTPR_1:36 x in dom p & x in dom q & PP_imp(p,q).x = TRUE implies p.x = FALSE or q.x = TRUE; theorem :: PARTPR_1:37 x in dom p & PP_imp(p,q).x = FALSE implies p.x = TRUE; theorem :: PARTPR_1:38 x in dom q & PP_imp(p,q).x = FALSE implies q.x = FALSE; theorem :: PARTPR_1:39 x in dom PP_imp(p,q) & PP_imp(p,q).x = FALSE implies x in dom p & p.x = TRUE & x in dom q & q.x = FALSE; theorem :: PARTPR_1:40 x in dom PP_imp(p,q) & PP_imp(p,q).x = TRUE implies x in dom p & p.x = FALSE or x in dom q & q.x = TRUE; theorem :: PARTPR_1:41 PP_and(PP_imp(p,r),PP_imp(q,r)) = PP_imp(PP_or(p,q),r); theorem :: PARTPR_1:42 PP_or(PP_imp(p,r),PP_imp(q,r)) = PP_imp(PP_and(p,q),r); ::\$N True constant predicate definition let D be set; func PP_True(D) -> PartialPredicate of D equals :: PARTPR_1:def 8 D --> TRUE; end; ::\$N False constant predicate definition let D be set; func PP_False(D) -> PartialPredicate of D equals :: PARTPR_1:def 9 D --> FALSE; end; theorem :: PARTPR_1:43 for D being set holds PP_not(PP_False(D)) = PP_True(D); theorem :: PARTPR_1:44 for D being set holds PP_not(PP_True(D)) = PP_False(D); theorem :: PARTPR_1:45 PP_or(p,PP_True(D)) = PP_True(D); theorem :: PARTPR_1:46 PP_or(PP_True(D),p) = PP_True(D); theorem :: PARTPR_1:47 PP_and(p,PP_False(D)) = PP_False(D); theorem :: PARTPR_1:48 PP_and(PP_False(D),p) = PP_False(D); theorem :: PARTPR_1:49 PP_or(p,PP_not(p)) = PP_True(D) | dom p; theorem :: PARTPR_1:50 PP_or(PP_not(p),p) = PP_True(D) | dom p; theorem :: PARTPR_1:51 PP_and(p,PP_not(p)) = PP_False(D) | dom p; theorem :: PARTPR_1:52 PP_and(PP_not(p),p) = PP_False(D) | dom p; theorem :: PARTPR_1:53 PP_imp(PP_False(D),p) = PP_True(D); theorem :: PARTPR_1:54 PP_imp(p,PP_True(D)) = PP_True(D); theorem :: PARTPR_1:55 PP_or(PP_False(D)|dom p,PP_True(D)|dom q) = PP_True(D) | dom q; ::\$N Empty predicate definition let D be set; func PP_BottomPred(D) -> PartialPredicate of D equals :: PARTPR_1:def 10 {}; end; theorem :: PARTPR_1:56 for D being set holds PP_not(PP_BottomPred(D)) = PP_BottomPred(D); theorem :: PARTPR_1:57 PP_or(PP_BottomPred(D),PP_True(D)) = PP_True(D); theorem :: PARTPR_1:58 PP_and(PP_BottomPred(D),PP_False(D)) = PP_False(D); theorem :: PARTPR_1:59 PP_imp(PP_BottomPred(D),PP_True(D)) = PP_True(D); begin :: Algebra of partial connectives with (strong) Kleene logical connectives definition let D; func PartialPredConnectivesMeet(D) -> BinOp of Pr(D) means :: PARTPR_1:def 11 for p,q being PartialPredicate of D holds it.(p,q) = PP_and(p,q); func PartialPredConnectivesJoin(D) -> BinOp of Pr(D) means :: PARTPR_1:def 12 for p,q being PartialPredicate of D holds it.(p,q) = PP_or(p,q); func PartialPredConnectivesCompl(D) -> UnOp of Pr(D) means :: PARTPR_1:def 13 for p being PartialPredicate of D holds it.p = PP_not(p); end; definition let D; func PartialPredConnectivesLatt(D) -> strict OrthoLattStr equals :: PARTPR_1:def 14 OrthoLattStr(# Pr(D) , PartialPredConnectivesJoin(D) , PartialPredConnectivesMeet(D) , PartialPredConnectivesCompl(D) #); end; registration let D be non empty set; let f,g be BinOp of D; let h be UnOp of D; cluster OrthoLattStr(#D,f,g,h#) -> non empty; end; registration let D; cluster PartialPredConnectivesLatt(D) -> non empty constituted-Functions; end; registration cluster non empty constituted-Functions for LattStr; end; registration cluster strict non empty constituted-Functions for OrthoLattStr; end; registration let D; cluster PartialPredConnectivesLatt(D) -> Lattice-like; cluster PartialPredConnectivesLatt(D) -> bounded; cluster PartialPredConnectivesLatt(D) -> de_Morgan join-idempotent with_idempotent_element; end; theorem :: PARTPR_1:60 Top PartialPredConnectivesLatt(D) = PP_True(D); theorem :: PARTPR_1:61 Bottom PartialPredConnectivesLatt(D) = PP_False(D); definition let L be non empty constituted-Functions LattStr, a, b be Element of L; pred a is_a_partial_complement_of b means :: PARTPR_1:def 15 a"\/"b = Top L | dom b & b"\/"a = Top L | dom b & a"/\"b = Bottom L | dom b & b"/\"a = Bottom L | dom b; end; definition let L be non empty constituted-Functions LattStr; attr L is partially_complemented means :: PARTPR_1:def 16 for b being Element of L ex a being Element of L st a is_a_partial_complement_of b; end; definition let IT be constituted-Functions non empty LattStr; attr IT is partially_Boolean means :: PARTPR_1:def 17 IT is bounded partially_complemented distributive; end; registration cluster partially_Boolean -> bounded partially_complemented distributive for constituted-Functions non empty LattStr; cluster bounded partially_complemented distributive -> partially_Boolean for constituted-Functions non empty LattStr; end; theorem :: PARTPR_1:62 for a,b being Element of PartialPredConnectivesLatt(D) st a = p & b = PP_not(p) holds b is_a_partial_complement_of a; registration let D; cluster PartialPredConnectivesLatt(D) -> partially_Boolean; end; ::\$N Distributivity law theorem :: PARTPR_1:63 PP_or(p,PP_and(q,r)) = PP_and(PP_or(p,q),PP_or(p,r)); definition let L be non empty OrthoLattStr; attr L is Kleene means :: PARTPR_1:def 18 for x,y being Element of L holds x"/\"x` [= y"\/"y`; end; registration cluster Boolean well-complemented -> Kleene for meet-absorbing join-absorbing meet-commutative non empty OrthoLattStr; end; registration let D; cluster PartialPredConnectivesLatt(D) -> Kleene; end; registration cluster partially_Boolean join-idempotent Lattice-like for non empty constituted-Functions LattStr; end; registration cluster Kleene de_Morgan join-idempotent with_idempotent_element Lattice-like strict for non empty OrthoLattStr; end; registration cluster partially_Boolean Kleene de_Morgan join-idempotent with_idempotent_element Lattice-like strict for non empty constituted-Functions OrthoLattStr; end;