Domains have large numbers of terms indicating objects of different sets and types. This are typically organized in several hierarchies. It is useful to have a simple way of expressing such hierarchies.

Sets

Enumerations and Finite sets of constants

It would be nice to have a notation that introduces a set of values for a variable. This is allowed in Pascal, C, C++, and Ada. Currently a declaration like

 	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}.

---

[ Enumerating%20Finite%20Sets in logic_30_Sets ]

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 ]

Subsets

The simplest classification system for a set of objects is created by using the Subsets. In the MATHS notation the set of all subsets is indicated by the curly "@" sign. This is reminiscient of the curly P used by mathematicians:

1. (set)|-For Set S, @S = { A. A==>S }.

   ---

   For example to make B and C be special kinds of A we write:
   1. A:Sets,
   2. B::@A,
   3. C::@A.

      The above imply the following:
      

   4. (above)|- (E1): B ==> A.
      
   5. (above)|- (E2): C ==> A.
      
   6. (E1)|-for all b:B, b in A.
      
   7. (E2)|-for all c:C, c in A.

      They do not assume that every A is either a B or C however.

   ---

   BNF

   Bachus Naur Form allows one to define one set as the union of other sets:

   ---

   1. A::= B | C.

      This implies the following deductions:
      

   2. (above)|-for all a:A, a in B or a in B.
      
   3. (above)|-for all b:B, b in A.
      
   4. (above)|-for all c:C, c in A.

      However, it is possible for an item in A to be in both B and C.

      In jargon: A is covered by B and C. See set_families.

   ---

   Partitions: nonoverlapping classification

   The statement
2. A >== {B, C},

   says the same thing as

3. A = B | C and A & B = {}.

   In other words that every A is a either a B or a C, and no A is both a B and C.

   In the UML this is a disjoint and complete specialization.

   For more on the exstensive theory of partitions and their realtionship to mappings and equivalence relations see set_families.

. . . . . . . . . ( end of section Sets) <<Contents | End>>

Nets

Abbreviations

The following are introduced to allow the simple and natural expression of simple ideas like a person is either male or female but not both:

 		Person::=Net{..... Either male or female. .... }.

1. For A, B:word,
2. either A or B::=Net{ A, B:@. A iff not B },
3. Either A or B::=either A or B.

4. For A, B:word, L:#("," word), (either A L, or B) ::=Net{ A, L, B:@. One(A L, B) }, (Either A L, or B) ::=(either A L, or B).

. . . . . . . . . ( end of section Nets) <<Contents | End>>

Polymorphism

MATHS permits the same identifier to have different meanings in different contexts. A context is determined by the type of thing that fits in that context.

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.

---

1. FTA::=following
   Net
   Feeding the Animals.
   1. Animal::Sets.
   2. Food::Sets.
      
   3. |-Animal>== {Wolf, Cow}.
      
   4. |-Food>== {Meat, Grass}.
      
   5. |-Number>== {int, float}.
   6. energy::Animal->Number.
   7. energy::Wolf->float.
   8. energy::Cow->int.
   9. energy::Food->Number.
   10. energy::Grass->int.
   11. energy::Meat->float.
   12. eat::Animal><Food->Animal.
   13. For all c:Cows, g:Grass, eat(c,g)::= the Cow(energy=>energy(c)+energy(g)).
   14. For all c:Wolf, m:Meat, eat(w,m)::=the Wolf(energy=>energy(w)+energy(g)).

       It is now valid to have Cows eat Grass and Wolves eat meat and make reason with the consequences but nothing can be deduced about eat(w,g) and eat(c,m).

   
   (End of Net)
   
   

---

. . . . . . . . . ( end of section Polymorphism) <<Contents | End>>

See Also

1. set::= See http://www.csci.csusb.edu/dick/maths/logic_30_Sets.html.
2. set_families::= See http://www.csci.csusb.edu/dick/maths/logic_31_Families_of_Sets.html.
3. set_theory::= See http://www.csci.csusb.edu/dick/maths/logic_32_Set_Theory.html.
4. enumerations::= See http://www.csci.csusb.edu/dick/maths/math_77_Enumerations.html.

5. ontology::= See http://www.csci.csusb.edu/dick/samples/index.html#Ontologies.
6. an_Ontology_for_English::= See http://www.csci.csusb.edu/dick/maths/logic_8_Natural_Language.html.

. . . . . . . . . ( end of section Classifications and Ontologies) <<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