[ TERMS ]
[ COERCIONS ]
[ MAPS ]
[ ARROWS ]
[ UNARY ]
[ INFIX ]
[ ASSIGNMENTS ]
[ RELATIONS ]
[ MODULUS ]
[ QUOTIENT_SETS ]
[ MORPHISMS ]
[ INDEXED_SETS ]
Non-standard MATHS is indicated by asserting the term "NONSTANDARD" which removes the (invisible) assertion of STANDARD. Thus the term STANDARD is still defined and so individual parts can be referred to ans asserted if needed. Because non-standard MATHS invalidates nearly a megabyte of documentation its use is to be deprecated.
In proofs:
For T, X:@T,
but
I call operaters like '<' parallel operators and those like '+' serial. The words catch the image in my mind of the kind of electrical circuit that would combine operators in a similar way.
A serial operator is an operator that is used like "+" so that 1+2+3 is 6. A parallel operator is used like "=" so that 1=2=3 is false.
In Gries and Schneider's text "A Logical Approach to Discrete Math", a parallel operator is called conjunctive. They use a similar notation to my serial notation for most operators.
(maps) |-For T:Types, associative(T) ::={f:T><T->T || for all x,y,z:T(f(f(x,y),z)=f(x, f(y,z)) }.
Example - SERIAL(disjunction, conjunction, "or", or, @)
Clearly the formal and precise statements that a given symbol string s, in a given context T, has a particular value v (symbol( s, T, v) ) are a translation of the informal definition... and in the next example the formal translation is ommitted:
Example - PARALLEL( equivalences, implication, "iff", iff, @).
Mathematicians have made an extensive survey of systems made up of a set of elements with an associative operator: [ math_31_One_Associative_Op.html ]
Note. (_)*(_) and (*) have different domains, (_)*(_) is a unary operator but (*) is a binary one.
Notice: since (+):infix(Number), the maps from a set into a class of Numbers are thersfore bags or multisets. Maps from 1..n into Real numbers gives the beginning of vectors. These definitions also give us Bits and bitwise operators.
Forx:variable(type(A), e(x):expression(type(A), +[x:A]e(x) ::= +map[x:A]e(x).
By the definitions in the calculus of relations and maps, notice that if f:X^A and B==>A then (f o B) is the function f restricted to domain B.
Note that if (+) has an inverse operation (-) then +(f o (A|B)) = +(f o B) + +(f o B) - +(f o (A&B)). see Group theory [ Properties in math_34_Groups ]
)=::INFIX.
. . . . . . . . . ( end of section Infix operations) <<Contents | End>>
Some call x:A->X a family, and write (x[i] || i:A) ::= fun[i:A](x[i]).
Example.
For X:Sets, R:@(X,X), w,x,y,z:X, L:#X,
This can be extended so that
For X:Sets, R,S,T:@(X,X), w,x,y,z:X,
The symbols <, <=, >, and >= are used to indicate orders and the following interval notation is standard:
Note that a completely rigorous treatment of intervals requires us to be very clear about the types of data we are refering so.
For more see [ math_21_Order.html ]
Source: Mili et al. 89, Jaoua Mili et al 91
Hence
. . . . . . . . . ( end of section Binary relations) <<Contents | End>>
Source: Godement.
The quotient set lemmas give conditions guaranteeing that there is only one g that fits in this diagram:
S----f----->X
S>==S/E--g->X
| ???
S>==S/f
When A and B have structures of the same type AND the mapping f in some sense or other preserves the structure then the mapping is called a "morphism".
[ ARROWS] . We will symbolize sets of morphisms by (name_of_structure) A arrow B where
If S is the name of the structure we have:
arrow Names Relationship
-> S morphism, (0.. )-(1)
>-- S epimorphism, (1.. )-(1)
--> S monomorphism, (0..1)-(1)
--- S isomorphism, ( 1 )-(1)
==> sub_S, S injection, (1)-(1) and equallity
>== S_partition, (1.. )-(1), and membership
For example, given a system with name SYS, with objects of class T=$ SYS with a n-ary operator f:T^n->T then there is a natural morphism m defined on objects of type T:
A special case is when n = 0, then f.X is an element in X and f.Y in Y and f.Y=m(f.X) and we write: (X,f.X)a(Y,f.Y) ::=(f)X a Y
There is also a common way for n-ary relations to be preserved:
For example if R is a partial order on sets X and Y then (R)X->Y are the monotone mappings from X to Y.
Notice that it is possible for f:(R)X->Y and not x in R and f(x) in R.
Since X~R=rel [x,y:X](not(x R y)) then (~R)X->Y are those maps that do not add new relationships
A strong way to preserve a map f:T^n->T2 (for some T2<>T) is clearly: for all x:X^n( f(x)=f(m(x))).
There are similar natural structure transforming mappings between sets with different operations and mappings - Here are the simple cases:
Hence to declarations like
From here we can either progress to the general theory of all objects and morphisms ( [ math_25_Categories.html ] and [ math_43_Algebras.html ] ), or to the special cases for each type of logistic system.
. . . . . . . . . ( end of section The standard MATHS assumptions and definitions) <<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