traffic_light:{Red, Amber, Green}.would not automatically define the terms Red, Amber, etc. However
traffic_lights::={Red, Amber, Green}.is short hand for
traffic_lights::Sets,
Red::traffic_lights,
Amber::traffic_lights,
Green::traffic_lights,
|- traffic_lights={Red, Amber, Green}.
Notice that no order is implied between the elements listed above. In programming, an enumeration is an linearly ordered set and in MATHS the notation is
enum(intuitive, sensing)[ math_77_Enumerations.html ]
The above imply the following:
They do not assume that every A is either a B or C however. Some A's may be neither.
<-------------------------A----------------->
<----------B--->
<----C------------->
You need to be careful of the meaning of words indicating subsets in English
and other natural languages. For example in the set of People we often
distinguish Tall and Short people:
Net
Niether can we assume
What we do have, in this case, is
<--Short--><------------People~Short------------------->
<-------People~Tall-----------------><------Tall------->
This is a common pattern [Leech74] when we have an underlying ordering governed by an attribute -- in the above case height.
There is another trap when you are trying to compare items in different sets... for example consider a large chihuahua vs small saint bernard.
This implies the following deductions:
However, it is possible for an item in A to be in both B and C.
<-------------------------A----------------->
<----------B--------->
<-------------C------------->
In jargon: A is covered by B and C. See set_families.
says the same thing as
A partition implies
In other words that every A is a either a B or a C, and no A is both a B and C.
<-------------------------A----------------->
<----------B---->
<------------C------------->
In the UML this is a disjoint and complete specialization.
For more on the theory of partitions and their relationship to mappings and equivalence relations see set_families.
If we have a set A with two subsets B==>A and C==>A then we can partition A as follows
Similarly with three subsets(B,C,D) we have a partition with 8 sets: {
A Venn Diagram is a handy way to render these structures [ ../samples/nerd-venn-diagram.html ] (humorous example) plus [ http://cartesianproduct.wordpress.com/2012/08/12/venn-diagrams-for-11-sets/ ] (nice layouts for many variables)
More, these partitions give rise to an easy to use logic -- term logic. For example, Leech [Leech74] presents the idea (from anthropology) that terms in natural language can be given meaning in terms of components:
man +HUMAN+ADULT+MALE
woman +HUMAN+ADULT-MALE
boy +HUMAN-ADULT+MALE
girl +HUMAN-ADULT-MALE
Using the approach described above we would define
Net
Sample theorem
. . . . . . . . . ( end of section Sets) <<Contents | End>>
Person::=Net{..... Either male or female. .... }.
. . . . . . . . . ( end of section Nets) <<Contents | End>>
A consequence of allowing multiple polymorphic symbols in documentation is that all functions in MATHS should be seen as "multimethods" [PuppydogRacoon99]. In the classic problem of "Feeding the Animals" for example, we have two types: Animal and Food. Animals are classified as Wolves and Cows. Foods are classified as Meat and Grass. All Animals eat Food and get energy from it, but Wolves only eat Meat and Cows only eat Grass. A language with multimethods or another form of automaic down casting will invalidate the idea of Cows eating Meat and Wolves eating Grass.
It is now valid to have Cows eat Grass and Wolves eat meat and reason with the consequences but nothing can be deduced about eat(wolf,grass) and eat(cow,meat).
Further because Animal and Food are declared separately as Sets they are implictly not in the same type. This means that eat(grass, wolf) is illegitimate in this Net.
However, if this net was instanciated with two sets (Animal, Food) in the same hierarchy then an expression like eats(grass, cow) is definable and may even provoke thought about the meaning intended for eat. Indeed, eats(wolf, cow) starts to look meaningful and ominous.
However if two nets have different variables then they will belong in different types.
In particular, if one net ABC say defines a:A, b:B, c:C then its objects are of a different type to the net AB that only defines a:A and b:B. We would say that ABC extends AB. We could even define ABC as AB with {c:C} as an explicit extension.
. . . . . . . . . ( end of section Polymorphism) <<Contents | End>>
. . . . . . . . . ( end of section Classifications and Ontologies) <<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