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:
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:
In practice this is not useful but it does make an interesting exercise.
We have a special notation for expressing the relation associated with a predicate:
A binary relation can be treated as a function or infix operator that maps
pairs of objects into @:
The following is a convenience for English speakers.
Equality between relations of the same type is determined by the set of
pairs defining the relation.
.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).
MATHS also has the following useful over-loadings for the '+>' symbol:
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 ]
By combining the properties of converses and relations as maps (above) we
get
.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).
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:
For those who would like symbols, it can be shown that (|) can opearate
as an img in the right context:
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 ]
. . . . . . . . . ( end of section Domain Structure) <<Contents | End>>
Binary relations are PARALLEL operators.
The semicolon is a SERIAL operator: (;(R,S,T,...)) ::=(R;S;T;...)
Beware of treating converse as if it cancels relations out since
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!"
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.
|- 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)}.
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>>
The following are convenient short hand notations:
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:
. . . . . . . . . ( end of section Abuses of notation) <<Contents | End>>
Read |+> as or else.
Here is the formal definition:
The "~>" is the over_ridden_by operator defined in the next section.
Other books
Source: Nielson & Nielson 92 [NielsonNielson92] use a notation like this
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 ]
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.
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>>
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 might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.
For a complete listing of pages in this part of my site by topic see [ home.html ]
For a more rigorous description of the standard notations see