one BinRelAttr_Reflexive = return [essence| forAll &xP : &dom . &rel(&x,&x) |]
one BinRelAttr_Irreflexive = return [essence| forAll &xP : &dom . !(&rel(&x,&x)) |]
one BinRelAttr_Coreflexive = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) -> &x=&y |]
one BinRelAttr_Symmetric = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) -> &rel(&y,&x) |]
one BinRelAttr_AntiSymmetric = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) /\ &rel(&y,&x) -> &x=&y |]
one BinRelAttr_ASymmetric = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) -> !&rel(&y,&x) |]
one BinRelAttr_Transitive = return [essence| forAll &xP, &yP, &zP : &dom . &rel(&x,&y) /\ &rel(&y,&z) -> &rel(&x,&z) |]
one BinRelAttr_Total = return [essence| forAll &xP, &yP : &dom . &rel(&x, &y) \/ &rel(&y, &x) |]
one BinRelAttr_Connex = return [essence| forAll &xP, &yP : &dom . &rel(&x,&y) \/ &rel(&y,&x) \/ (&x = &y) |]
one BinRelAttr_Euclidean = return [essence| forAll &xP, &yP, &zP : &dom . &rel(&x,&y) /\ &rel(&x,&z) -> &rel(&y,&z) |]
one BinRelAttr_LeftTotal = return [essence| forAll &xP : &dom . exists &yP : &dom . &rel(&x,&y) |]
one BinRelAttr_RightTotal = return [essence| forAll &yP : &dom . exists &xP : &dom . &rel(&x,&y) |]
one BinRelAttr_Serial = one BinRelAttr_LeftTotal
one BinRelAttr_Equivalence = one BinRelAttr_Reflexive ++ one BinRelAttr_Symmetric ++ one BinRelAttr_Transitive
one BinRelAttr_LinearOrder = one BinRelAttr_Total ++ one BinRelAttr_AntiSymmetric ++ one BinRelAttr_Transitive
one BinRelAttr_WeakOrder = one BinRelAttr_Total ++ one BinRelAttr_Transitive
one BinRelAttr_PreOrder = one BinRelAttr_Reflexive ++ one BinRelAttr_Transitive
one BinRelAttr_PartialOrder = one BinRelAttr_Reflexive ++ one BinRelAttr_AntiSymmetric ++ one BinRelAttr_Transitive
one BinRelAttr_StrictPartialOrder = one BinRelAttr_Irreflexive ++ one BinRelAttr_ASymmetric ++ one BinRelAttr_Transitive
-- reflexive, the diagonal is full
-- irreflexive, the diagonal is empty
-- coreflexive, only the diagonal is full
-- symmetric, if R(x,y) then R(y,x)
-- anti-symmetric, both R(x,y) and R(y,x) are never full at the same time (we say nothing about the the diagonal)
-- a-symmetric, anti-symmetric + irreflexive
-- transitive xy + yz -> xz
-- total: either R(x,y) or R(y,x). implies reflexive
-- connex: total, but doesn't imply reflexive (we say nothing about the diagonal)
-- left-total: every x is related to some y -- R(x,y)
-- right-total: every y is related to some x -- R(x,y)
-- Euclidean: xy + xz -> yz
-- some properties
-- total implies reflexive. connex doesn't.
-- aSymmetric implies irreflexive and antiSymmetric
Some notes from code comments:
-- reflexive, the diagonal is full -- irreflexive, the diagonal is empty -- coreflexive, only the diagonal is full -- symmetric, if R(x,y) then R(y,x) -- anti-symmetric, both R(x,y) and R(y,x) are never full at the same time (we say nothing about the the diagonal) -- a-symmetric, anti-symmetric + irreflexive -- transitive xy + yz -> xz -- total: either R(x,y) or R(y,x). implies reflexive -- connex: total, but doesn't imply reflexive (we say nothing about the diagonal) -- left-total: every x is related to some y -- R(x,y) -- right-total: every y is related to some x -- R(x,y) -- Euclidean: xy + xz -> yz
-- some properties -- total implies reflexive. connex doesn't. -- aSymmetric implies irreflexive and antiSymmetric
-- derived definitions -- serial: left-total -- equivalance: reflexive + symmetric + transitive -- linearOrder: antiSymmetric + total + transitive -- weakOrder; total + transitive -- preOrder: reflexive + transitive -- partialOrder: reflexive + antiSymmetric + transitive -- strictPartialOrder: irreflexive + transitive (implied aSymmetric)