In the history logics the theory of relationships between two things: `x is the father of y` for example, is a 20th century development. For a long time statements like x is the father of y would be translated into `x is a member of the fathers of y`. This allows some conclusions to be drawn but disguises some important properties. Relations are central to all modern mathematical forms of logic. These relations can appear in two disguises: As predicates with two unknowns, or as sets of pairs of objects. The following can all be treated as the same expression:

• frank fathered dick,
• fathered(frank, dick),
• (frank, dick) in fathered,
• (frank, dick).fathered,
• dick in fathered(frank),
• frank in /fathered(dick),
• etc.

Binary relations are a special case of the n-ary relations: [ logic_44_n-aryrelations.html ] There is also a specialized theory of relations between things of the same type: [ logic_41_HomogenRelations.html ]

MATHS assumes that for any two types T1 and T2 then @(T1><T2) is also a type. @(T1><T2) stands for the set of all pairs. It is convenient to identify each of these sets with a relationship. Hence we talk of the type of all binary relations between T1 and T2, @(T1,T2). The power set symbol (@) has a special meaning when applied to pairs:

1. For T1, T2:Types, @(T1,T2)::=@(T1><T2).
2. For T1, T2:Types, R:@(T1,T2), dom(R)::= T1,
3. cod(R)::= T2.
4. dom::=domain,
5. cod::=codomain.

   Formal Model

   You can (if you want to) formulate this in the documentation notation of MATHS: [ notn_13_Docn_Syntax.html ]
6. FORMALIZATION_AS_SETS::=
   Net{

   1. BINARY_RELATIONS::=
      Net{

      1. dom::Types=generic.
      2. cod::Types=generic.
      3. underlying_set_of_pairs::@(dom><cod)

      
      }=::BINARY_RELATIONS.

      In practice this is not useful but it does make an interesting exercise.

   
   }=::FORMALIZATION_AS_SETS.

   We have a special notation for expressing the relation associated with a predicate:

7. For T1,T2:Types, x,y:variables, W:expresion(@), (rel [x:T1,y:T2] (W)) ::@(T1,T2) = {(x,y)||(W)}.

   A binary relation can be treated as a function or infix operator that maps pairs of objects into @:
   

8. (STANDARD)|- (r2f): for T1,T2,R, x:T1, y:T2, x R y = R(x,y) = (x,y).R.
   
9. (STANDARD)|- (r1in): R = (1st) R (2nd).

   The following is a convenience for English speakers.

10. For R:@(T1,T2),x:T1,x:T2, x is R y::=x R y.

    Equality between relations of the same type is determined by the set of pairs defining the relation.
    

11. (euclid)|- (req1): For R,S:@(T1,T2), if R=S then for all x,y(x R y=x S y).
    
12. |- (req2): For R,S, if for all x,y(x R y iff x S y) then R=S.

    Relations as Maps

    In a context demanding a mapping, a relation can be used.
13. For R:@(T1,T2), R::T1->@T2=map[x:T1]{y:X||x R y}.
    
14. (above)|- (r2m): For R:@(T1,T2), x:T1, x.R= R(x)= {y:X||x R y}.

    .Dangerous_Bend Mathematical relations do not work like English verbs. A sentence like `x is the parent of y is natural formalized as x parent y` and as a result the children of x as represented parent(x).

15. For R:@(T1,T2), R::@T1->@T2=map[X:@T1]{y:Y||for some x:A(x R y)}.
    
16. (above)|- (r2ms): For R, A:@T1, A.R= R(A)= {y:Y||for some x:A(x R y)}.
    
17. (r2ms, r2m)|- (r2mu): For R, A, A.R = = R(A) = |[x:A](R(x)).

    Elementary Relations

    Inherited from Principia Mathematica and Z is a symbol for the relation that holds between a pair of objects:
18. For a:T1, b:T2, a+>b::= {(a,b)}.
    
19. (above)|- (rs): a+>b = rel [x:T1, y:T2](x=a and y=b).

    MATHS also has the following useful over-loadings for the '+>' symbol:

20. For A:@T1, b:T2, A+>b::= {(a,b) :T1><T2 (a in A )}.
21. For B:@T2, a:T1, a+>B::= {(a,b) :T1><T2 (b in B)}.

    However for two sets A and B, A+>B is a pair {(A,B)} and the set of pairs is A><B: (above) |-For A:@T1, B:T2, A><B::= {(a,b) :T1><T2 (a in A and b in B)}.

    Elementary relations can be combined to give more complex relations by using the operations defined below [ #Operations on Relations ]

    
    

22. (r2m, def)|-a.(a+>b)={b}.
    
23. (r2m, def)|-For x:A~{a}, x.(a+>b)={}.

    Converse Relations

24. For R:@(T1,T2), /R::@(T2,T1) = rel [x,y](y R x), /R::= the converse relation to R.
    
25. (above)|- (c1): /R = (2nd) R (1st).
    
26. (above)|- (c2): /(a+>b)=(b+>a).
    
27. (above)|- (c3): /(A+>b)=(b+>A). (above) |-(c4): /(rel [x:T1,y:T2] (W)) ::=(rel [y:T2,x:T1] (W))

    By combining the properties of converses and relations as maps (above) we get
    

28. (above)|- (cm1): For y:T2, R:@(T1,T2), y./R=/R(y)={x:T1 || x R y}.
    
29. (above)|- (cm2): For R:@(T1,T2), B:@T2, B./R=/R(B)={x:T1 || for some y:B(x R y)}.

    .Dangerous_Bend Mathematical relations do not work like English verbs. A sentence like `x is the parent of y is natural formalized as x parent y` and as a result the parents of y are shown as /parent(y) and the children of x as parent(x).

    Operations on Relations

    The binary operations on relation of a given type follow from their definition as sets:
30. sets::= See http://csci.csusb.edu/dick/maths/logic_30_Sets.html

    
    

31. (sets)|- (sr1): For R:@(T1,T2), S:@(T1,T2), R & S = rel [x:T1,y:T2] (x R y and x S y).
    
32. (sets)|- (sr2): For R:@(T1,T2), S:@(T1,T2), R | S = rel [x:T1,y:T2] (x R y or x S y).
    
33. (sets)|- (sr3): For R:@(T1,T2), S:@(T1,T2), R ~ S = rel[ x:T1,y:T2] (x R y not x S y).

    
    

34. (Boolean)|- (relations_Boolean): (@(T1,T2), |, {}, &, @(T1,T2), ~ ) in Boolean_algebra.

35. Boolean::= See http://csci.csusb.edu/dick/maths/math_41_Two_Operators.html#Boolean Algebra.

    Convenient notations

    Operators (|) and (&) are both serial. So
36. |(A,B,C) = A| (B|C) = A|B|C = (A|B)|C, for example.

    MATHS provides a set of synonyms for talking about the sets of objects involved on each side of a relationship. Each suggests a different metaphor, and each is used by some authority or other somewhere:

37. post::= dom(_).(_), -- post condition.
38. rng::=post, -- range.
39. img::=post, --image.

40. pre::=cod(_)./(_), pre-condition.
41. cor::=pre, -- co-range.
42. ddef::=pre, domain of definition (Z).
    
43. (def)|- (d1): For R:@(T1,T2), rng(R)= post(R) = img(R) = dom(R).R.
    
44. (def)|- (d2): For R:@(T1,T2), cor(R) = pre(R) = ddef(R) =cod(R)./R.

    
    

45. (def)|- (d3): post(R)=|(R) and pre(R)=|(/R), -- using conventions for treating relations as maps and taking unions of maps.

    
    

46. (def)|- (d4): For T1,T2,R, R = |[x:pre(R),y:x.R](x+>y) = |[x:pre(R)](x+>x.R) = |[y:post(R)](y./R+>x).

    For those who would like symbols, it can be shown that (|) can opearate as an img in the right context:
    

47. |- (bar2img): For R:@(T1,T2), | /R=pre(R) and |R=post(R).
48. For R:@(T1,T2), |/(R)::= |(/(R)).

    
    

49. (above)|- (duality): pre ( / (_) ) = post and post(/(_))=pre and ...

    Structures of the Domains of Relations

    A relationship induces structures on tits domain and codomain.

    Totality

    Notice that the pre-image of a relation is often less than its domain. This happens whenever the relation is partial rather than total...
    1. STANDARD::= See http://csci.csusb.edu/dick/maths/math_11_STANDARD.html#Types of relationships.
       
    2. (STANDARD)|-R is total iff pre(R)=post(R)

       Structure of the Domain

       A relation R defines a structure(a complex) on its codomain,
    3. For R:@(T1,T2), coi(R)::={ X:@T1 | for some y( X=y./R ), -- (co-image) [ logic_31_Families_of_Sets.html ]

       
       

    4. (STANDARD)|-R is regular iff post(R)>=={x.R||x:pre(R)}.

       If a relation is a many to one then the coimage (coi) defines a partition. For more on domain structure see [ coi in logic_42_Properties_of_Relation ]

       Weakest Preconditions

       The following idea comes from Dijkstra's Discipline of Programming. For any relation R and set of codomain objects A, there is a weakest precondition (largest set) of preconditions that guarantee that their objects can be related to at least one object in A:
    5. For R:@(T1,T2), A:@cod(R), wp(A,R)::= {x:pre(R) || x.R==>A}, -- weakest pre-condition for A,

    . . . . . . . . . ( end of section Domain Structure) <<Contents | End>>

    Products of Relations

    Binary relations are PARALLEL operators.

50. For R:@(T1,T2), S:@(T2,T3), x R y S z::= x R y and y S z.

51. For R:@(T1,T2), S:@(T2,T3), R;S::@(T1,T3) = rel[x:T1,y:T3](for some z:T2 (x R z S y))
52. |- R;S::=for some z:dom(S)( (1st)R z S (2nd) ).

    The semicolon is a SERIAL operator: (;(R,S,T,...)) ::=(R;S;T;...)

    The Identity Relationship

53. Id(X)::= rel [x,y:T](x in X and x=y)

    Algebra of Products

54. MONOID::= See http://www.csci.csusb.edu/dick/maths/math_33_Monoids.html
    
55. |-MONOID.
    
56. (MONOID)|-(@(X,X),(;), Id(X)) in Monoid
    
57. (above)|-R ; /R ==> Id(X)

    Beware of treating converse as if it cancels relations out since

    
    

58. (finding an example)|-for all A,R, ( A==>a.R./R ) and for some A,R, ( a.R./R <> A )

    Relations between Subsets

    Given a pair of types each with subsets we can define the idea of a relation between the subsets. Notice that if A:@T1 and B:@T2 then x:A><B has type T1><T2, similarly @(A,B)=@(A><B) has type @(T1><T2).

    An Explanation

    The model is rather odd. It is based on a long chain of reasoning, presented below. But it was worked out back-wards from the difficulty of programming with strings in Pascal. The following paragraph describes the chain of logic... However I traversed this road back-wards, each step taking several years...

    To create a usable yet strong theory of types it was necessary to distinguish sets from objects in the sets. In turn the type of a set of objects depends on the type of the objects in the set - or to be more precise - the type of object from which the subset could have been chosen. All sets are seen as subsets of a particular type of object... roughly as in Ada. This approach was chosen because it also groups relationships into types that are determined by the type of of their elements but not the particular elements involved: if a is of type T1 and b of type T2 then a+>b is of type @(T1,T2) not of type @({a},{b}). So a relation's type R:@(T2,T1) is somewhat independent of its pre-image or domain of definition. This in turn leads to the property that a functions type f:T2^T1 is independent of its pre-image or domain of definition. Since arrays are modeled as special kinds of functions, this means that an array of 10 integers has the same type as an array of 5 integers. Similarly for arrays of characters. Now equality is only defined between objects of the same type... it may be true or false, but at least defined! Therefore, the MATHS theory allows us to compare strings of characters.

    It is said that Nasrudin saw a mouse stagger out from the rubble fallen from a volcano that had just finished erupting and he laughed and saying "it took all that noise for the mountain to give birth to a mouse!"

    Definitions

    1. For A:@T1, B:@T2, A><B::@(T1><T2) = {(a,b) :(T1><T2) || a in A and b in B}

       
       

    2. (above)|- (cardprod): |A><B| = |A|*|B|, -- |A| = card(A)...

    3. For A:@T1, B:@T2, @(A,B)::= @(A><B).

    4. For A:@T1, B:@T2, R:@(A,B), dom(R)=T1 and cod(R)=T2 and pre(R)==>A and post(R)==>B.

       The relations between A and B are relations of type @(T1,T2). Thus in MATHS the domain of definition of a relation is a subset of the domain of the relation(a type) and equals its corange, similarly the range of the relation is a subset of its codomain.

       Consequences

       
       
    5. (above)|-For A:@T1, B:@T2, R:@(A,B), |/R=cor(R) in @dom(R) and |R=rng(R) in @cod(R)

       
       

    6. (above)|-For A:@T1, B:@T2, R:Sets (R in @(A,B) iff R==>(A><B))

    7. For R:@(A,B), x:T1,y:T2, x R y::= (x,y) in R,

       
       

    8. (above)|-R(x,y)= (x,y).R = (x,y) in R.

       
       

    9. (above)|-For R:@(A,B), if x R y then x in A and y in B.

       |- For a:T1, b:T2, a+>b::= {(a,b)}=rel [x:T1, y:T2](x=a and y=b).

       |- For A:@T1, b:T2, A+>b::= {(a,b) :T1><T2 (a in A and y=b)}.

       Concept Analysis

       A recent development shows how to construct a picture of the domain and codomain of a relation. Given R:@(X,Y) and a set A:@X, define
       A' = the set of y:Y that are related to every a in A
    10. = {y:Y. for all a:A(a R y)}
    11. = &[a:A](R(a)) and for B:@Y,
    12. B'={x:X. for all b:B( x R b)}=&[b:B](/R(b)),

        For example if X is a set of publications and Y a set of topics and R is the relation that is true when a publication refers to a topic, then if you have a couple of publications A then A' is the topics that are dhared by both. A'' is a larger collection of publications that share all the topics that the original two publications.

        A concept is a pair (A,B) where B=A' and A=B'. Magically, this produces a comparatively simple diagram (a lattice) describing the ideas underlying the relation R. These ideas have been used to extract the ideas hidden in source code and so aid software maintenance.

        For more see [ CONTEXT in logic_42_Properties_of_Relation ] for the formal definition of a context and its concepts.

    . . . . . . . . . ( end of section Relations between Subsets) <<Contents | End>>

    Abuses of notation

    For relations with small numbers of pairs, we use tables and diagrams.

    The following are convenient short hand notations:

    1. For Types T, (=) ::@(T,T)= Id(T)
    2. For R:@(T1,T2), B:@T2, R;B::= R;Id(B)
    3. For A:@T1, S:@(T1,T2), A;R::= Id(A);R
    4. For A, B:@T, A;B::= Id(T) & @(A,B).

       
       

    5. (above)|-For A,B:@T, A;B <> @(A,B).

       
       

    6. (above)|-For R:@(T1,T2), A:@T1, B:@T2, A;R;B = R & @(A,B).

       Thus in MATHS we avoid the need for special symbols or words to indicate the limiting of relations used in other systems - Principia Mathematica and Z for example.

       The following abbreviations are natural and unambiguous:

    7. x R y and z...::= x R y and x R z and...
    8. x and y and...Rz::= x R z and y R z and ... [Compare COBOL relations]

    . . . . . . . . . ( end of section Abuses of notation) <<Contents | End>>

    Operations Used in Formal Specifications

    The following are not developed from philosophical or theoretical reasons. They are created and documented because they are needed to make formal specifications easier to write and read.

    "Or else"

    It is very useful to have special operation that makes a relation total by linking all the unconnected objects in the domain to an item in the codomain:
    1. For T1,T2,R, b:T2, R|+>b:@(T1, T2) ::= R | ( (T2~pre(R))+>b ).

       Read |+> as or else.

       An Operation used in the Formal Semantics of Programming languages

       In programming we have an assigment operator:
    2. variable := expression; (Ada, Algol 60 Ada, and Pascal notation). It indicates that the value associated with the variable is changed to the value of the expression. In abstract we often want to change a single value in an array (map) of values like this:
    3. (a,b,c) = (1+>a | 2+>b | 3+>c).
    4. (a,b,c).(2:=x) = (a,x,c).

       Here is the formal definition:

    5. For T1,T2, f:T1->T2, v:pre(f), e:T2, f.(v:=e)::= f~>(v+>e).

       The "~>" is the over_ridden_by operator defined in the next section.

       Other books Nielson & Nielson 92 [NielsonNielson92] use a notation like this
       f [ v +> e] = f.(v:=e).

       This is a handy model for: the state of the RAM in a computer, changing an item in an array, operating on a direct access file, changes in registers in a processor, ... [ RAM in math_14_Dynamics ]

       Operations from Z(Zed)

       Research in Europe has discovered that a particular operation on relations is useful for specifying many different problems and domains. In many specification written in Z the idea of modifying a relation by removing items that don't lie in a subset of the domain or codoman is quite common.
    6. A \dashed_triangle_left R::= ~A;R.
       
    7. (above)|- (dtl): A \dashed_triangle_left R ={(x,y) :T1><T2 || x not in A and x R y} = (cor(R)~A);R.
    8. R \dashed_triangle_right B::= R;~B.
       
    9. (above)|- (dtr): R \dashed_triangle_right B ={(x,y) :T1><T2 || y not in B and x R y} = R; (ran(R)~B)

       Similarly the idea of one relation over riding another one is often needed. In Z the idea of over-riding is used to express the dynamics of maps and functions. This is also used to define the meaning (effect) of operations in a programming language on an abstract state associating variables with their values.

    10. For T1,T2, R, S:@(T1,T2), R \circle_plus S::= ( (cor(R)~cor(S)); R) | S.
    11. For T1,T2, R, S:@(T1,T2), R ~> S::serial(@(T1,T2)) = R \circle_plus S.
    12. over_ridden_by::= map[R,S] ( R ~> S ).

        In Z these are typically used to represent the behavior that is implemented by classical data structures and files. There is a more abstract model found in SSADM or OOA/D where dynamics is defined by a network of interacting and cooperating processes, from which the files (if any) and other data structures are developed to meet various performance criteria. [ Z-like Operators in logic_44_n-aryrelations ]

    . . . . . . . . . ( end of section Operations from Z) <<Contents | End>>

. . . . . . . . . ( end of section Binary relations) <<Contents | End>>

Notes on MATHS Notation

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see