The standard MATHS assumptions and definitions

Definition of the standard package

STANDARD::=
Net{
}=::STANDARD.
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.

Serial and Parallel Operators
In normal mathemetics
a<b<c means (a<b) and (b<c)
but
a+b+c means (a+b)+c.
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.
SERIAL_AND_PARALLEL::=
Net{
1. Uses SEMANTICS.
2. |- SEMANTICS::=Net{... [Compare Theory of MATHS types]
3. For x:: #lexeme, T::Types, v::T, symbol(x, T, v) ::@=symbol x in T means v . ...
4. For x, T, v, unique_symbol(x, T, v)::= symbol(x,T,v) and for one v:T(symbol(x, T, v)).
5. For x, T, if unique_symbol(x, T, v) then x.T::T= the[v:T](symbol(x, T, v)).
6. For x,y, T, x equivalent(T) y::@= (x.T = y.T).
7. }.
  (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)) }.
8. (strings)|-For T:Types, n:2.., a:T^n, front(a) ! last(a) = a, front(a) =(a1, a2, ..., a[n-1]).
9. INFIX::=Net{ f:#char, s:@#char, S:= f P(s) | P(s) dot f | "(" L(s, f) ")" }.
10. Example_infix::={ So,
11. INFIX(f=>"<", s=>expression, S=>relation) which is short for
12. expression::= "+" P(product) | P(product) dot "+" | "(" L(product, "+") ")", and
13. INFIX(f=>"+", s=>product, S=>expression) means
14. relation::= "<" P(expression) | P(expression) dot "<" | "(" L(expression, "<" ) ")".
}=::Example_infix.
SERIALITY::=
Net{
1. INFIX(f, s, S),
2. T::Types,
3. g::associative(T).
4. |-unique_symbol(f, T><T->T, g).
5. E::@#A=S | s dot f | f P(s).
6. We wish to link a unique value of Type T to each string in E.
7. First the formal equivalent of
8. |-for a,b:T, a g b = (a,b).g = g(a,b),
9. |-for a,b,c:T, a g b g c= (a,b,c).g = g(a,b,c)=g(g(a,b),c),
10. |-for n:3.., a:T^n, g(a) = a.g = g( g(front(a)), a(n)).
11. |-For a,b:s, symbol( a f b, T, g(a.T,b.T)).
12. |-For a,b,c:s, symbol( a f b f c, T, g(g(a.T,b.T), c.T).
13. |-For a,b,c:s, symbol( f"(" a "," b "," c ")" , T, g(g(a.T,b.T), c.T) ).
14. (above)|-For a,b,c:s, a f b f c equivalent(T) f"(" a "," b "," c ")".
15. |-For a:S, b:s, if symbol( a, T, v) then symbol( a f b, T, g(v, a.T) ).
16. |-For n:1.., a:s^n, b:s, if symbol(a,T,v) then symbol( f "(" a ! b")" , T, g(v, b.T) ).
17. (above)|-For s:S, one v:T, symbol(s, T, v).
18. Next establish the formal version of
19. for a:T, a.g = g(a) = a.
20. |-For a:s, symbol(a"."f, T, a.T) and symbol(f"("a")", T, a.T).
21. (above)|-For e:E, one v:T, symbol(e, T, v).
22. (above)|-if units(g) then one units(g).
23. |-if units(g) then for n:=(), g(n)=(n).g=the units(g).
24. (above)|-if units(g) then for e:E|"()", one v:T, symbol( e, T, v).
}=::SERIALITY.
For E,e,f,g,t, SERIAL(E, e,f,g,t)::=SERIALITY(T=>t, s=>e, f=>f, g=>g, E=>E).
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:
PARALLELISM::=
Net{
1. INFIX.
2. T::Types, g:: T><T->@.
3. |-symbol( f, T><T->@, g).
4. |-For a,b:T, a g b = (a,b).g = g(a,b).
5. |-For a,b,c:T, a g b g c= (a,b,c).g = g(a,b,c)=g(a,b)and g(b,c).
6. |-for n:4.., a:T^n, g(a) = a.g = g ( g(front(a)) and g(a(n-1),a(n) ) ).
}=::PARALLELISM.
For E,e,f,t, PARALLEL(E,e,f,g,t)::=PARALLELISM(T=>t, s=>e, f=>f,g=>g, S=>E).
Example - PARALLEL( equivalences, implication, "iff", iff, @).
|-For T:Types, R:@(T, T), r:#A, if symbol (r, @(T, T), R ) then PARALLEL(relational_proposition, expression(T),r, R, @).

SERIAL_AND_PARALLEL

Coercions

COERCIONS::=
Net{
1. For T:Types, x:T. (x) ::%T=(1+>x),
2. set(x)::@T={x},
3. bag(x)::T->Nat0=(x+>1),
4. x::@T=set(x),
5. x::#T=(x),
6. x::%T= (x),
7. x::T->Nat0=bag(x).
8. For x:#T, x::@T=img(x).
9. For x:%T, x::@T=img(x).
  For T, X:@T,
10. the::@X<>->X=rel[A,a](A={a} ),
11. the::#X<>->X=rel[A,a](A=(a) ),
12. the::%X<>->X=rel [A,a] (A=(a) ),
13. the::(X->Nat0)<>->X=rel[A,a](for some n:Nat(A=(a+>n))).
}=::COERCIONS.
Functions and Mappings
MAPS::=
Net{
1. For X:Set, (_) ::X^X=map[x](x).
2. |-For X, Y:Set, f:Y^X, x:X ( f(x)=x.f ),
3. For X, Y, Z:Set, f:Z^Y, f::Y^X->Z^X = map [g:Y^X] ( map [x:X](f(g(x)) ) ).
4. (def)|- (MAP0): f(g) = fun[x] f(g((x))) = f(g(_))).
5. For Set X,Y, x:X, y:Y, x+>y::X->Y={(x,y)}.
6. For Set X,Y, A:@X, y:Y, A+>y::X->Y={(a,y) || a:A}.
}=::MAPS.
ARROWS::=
Net{
1. Arrows::={ ->, >->, -->, >--, ---, ==>, >==, >=>, ...}. The arrows are used to describe sets of maps/functions.
2. For Types T1,T2, A:@T1, B:@T2, a:Arrows, (A a B) :: @(T1><T2).
3. For Types T1,T2, A:@T1, B:@T2, a:Arrows, m:morphisms, ((m)A a B) :: @(A a B). [ MORPHISMS ]
}=::ARROWS.
Unary operations
We can define the idea of an UNARY operator u, as a symbol which can be put in front or after its argument a:
UNARY::syntax=Net{ u:#char, a:@#char, e:= a | u a | a dot u }.
Example::={ Given this definition then the following MATHS statement,
|-UNARY( u=>"sqrt", a=>term, e=>expression) generates the following documentation:
expression::= term | "sqrt" term | term dot "sqrt".

}=::Example.

UNARY::semantics=

Net{

MAP.
For X:Set, unary(X)::=X^X.
For X:Set, f:unary(X), f:: @X->@X = map [A:@X] {f(a) || a:A},
For X:Set, f:unary(X), f:: #X->#X = map [a:#X] (map [i:1..|a|](f(a[i])). (M0) |-(U0): For X:Set, f:unary(X), f::X^A->X^A= map [g:X^A] ( map [a:A](f(g(a))).
For X:Set, f:unary(X), fixed_points(f)::@X= {x:X. f(x)=x}.

}=::UNARY.

Infix operations

INFIX::=
Net{
1. infix(X)::= X^( X><X ),
2. associative(X)::={*:infix(X)||for all x,y,z:X(x * (y * z)=(x * y) * z)},
3. commutative(X)::={*:infix(X)||for all x,y:X (x * y = y * x)},
4. idempotent(X)::={*:infix(X)||for all x:X (x * x = x)},
5. For *:infix(X),
6. units(X,*)::={u:X||x * u = u * x = x},
7. zeroes(X,*)::={z:X||for all x:X( z * x = x * z = z},
8. idempotents(X,*)::={i:X||i * i = i}.
  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 ]
  
  Mappings and infix operations
9. For *:infix(X), x:X, y:Y, (x *_) ::= map [y:X](x * y), (_* y) ::= map [x:X](y * x), (*) ::=map [x,y](x*y).
10. (def)|- (I0): For *:infix(X), x, y:X, (x*y) = (*)(x,y) = (x,y).(*) = (x*_)(y)=y.(x*_)=(_*y)(x)=x.(_*y).
11. (M0)|- (I1): For *:infix(X), x, y:X,
12. (_*x);(_*y)=(_*(x*y))
13. and (x*_);(y*_)=((y*x)*_)
14. and (x*_)=x*(_)
15. and (_*y)=(_)*y.
  Note. (_)*(_) and (*) have different domains, (_)*(_) is a unary operator but (*) is a binary one.
  Overloadings
16. For *:infix(X),
17. *::(@X)><(@X)= map [A,B] {a * b|| a:A, b:B},
18. *::( X)><(@X)= map [x,B] {x * b|| b:B},
19. *::(@X)><( X)= map [A,x] {a * x|| a:A},
20. *::(X^A)><(X^A)= map [f,g] (map [a:A] ( f(a) * g(a) ) ),
21. *::( X) ><( X^A)=map [x,f] (map [a:A] ( x * f(a) ) ),
22. *::(X^A)><( X)= map [f,x] (map [a:A] ( f(a) * x ) ). Notice: since (+):infix(Number), the maps from a set into a class of Numbers are therfore bags, multisets or vectors. Similarly for Bits and bitwise operators.
  
  Serial operations
23. For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X), +A in X,
24. |- (Ser0): if |A|=0 then +A=0,
25. |- (Ser1): if |A|=1 then +A=the (A),
26. |- (Ser2): if |A|>1 then for all Y:@A(+(A&Y) + +(A~Y))}.
27. (def, induction)|- (Ser3): for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, p:A(1)-(1)A, +p(A)=+A ).
28. (def, induction)|- (Ser4): for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, for B, (if B<==A then +A = +(A&B) ).
29. (def, induction)|- (Ser5): for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, for P:@@A( if P==<A then +A = +[p:P](+p)).
30. For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X), f:X^A, +f in X,
31. |-if |A|=0 then +f=0,
32. |-if |A|=1 then for some y:A(+f=f(y)),
33. |-if |A|>1 then for all Y:@A( +f=+(f o Y) + +(f o (A~Y)).
34. For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X), x: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.
35. (def, induction)|- (Ser6): for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, f:X^A, p:A(1)-(1)A, +(f o p)=+f ).
36. (def, induction)|- (Ser7): for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, f:X^A, for B, (if B<==A then +f = +(f o (A&B) ).
37. (def, induction)|- (Ser8): for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, f:X^A, for P:@@A( if P==<A then +f = +[p:P](+(f o p)).
  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.
  
  Assignment operators
38. ASSIGNMENTS::=
  Net{
  1. For U:documentation, x:variable(U), e:expression(type(x)), (*):infix(type(x)), x:=e::= (x'=(e))
  2. For U:documentation, x:variable(U), e:expression(type(x)), (*):infix(type(x)), x:*e::= (x'=x*(e)),
  3. For U:documentation, x:variable(U), e:expression(type(x)), (*):infix(type(x)), e*:x::= ((e)*x=x').
  }=::ASSIGNMENTS.
. . . . . . . . . ( end of section Infix operations) <<Contents | End>>

Indexed Sets and Families
INDEXED_SETS::=
Net{
1. For Type T, Sets S, Indexed(S)::={I->S || I:@T}.
2. For A:Indexed(Set), index(A)::=dom(A).
}=::INDEXED_SETS.
Some call x:A->X a family, and write (x[i] || i:A) ::= fun[i:A](x[i]).

Additivity
PARTIALLY_ADDITITIVE::=
Net{
1. (summable)Natural->Rational is the set of summable series and
2. (_^-2)=map[i](1/i^2) in (summable)Natural->Rational
3. summable::=|[a:Arrows, A:Countable, X:Sets]((summable)A a X).
4. For X:Sets, A:Countable, a:Arrows, ((summable)A a X) ::@(A a X).
5. For X:Sets, A:Countable, a:Arrows, +::((summable)A a X)->X.
6. |- (PA0): For a:Things, all X, f:{}->X(f in summable and +f=0).
7. |- (PA1): For a:Things, all X, f:{a}->X(f in summable and +f=f(a)).
8. |- (PA3): For A, β in partition(A) & countable, f:A->X, f in summable iff for all B:β(f o B in summable) and fun[B:β]( +(f o B) ) in summable and +f = +[B:β]( +(f o B) ).
9. |- (PA4): For A,X, f:A->X, if for all F:finite(A) (f o F in summable) then f in summable.
10. (above)|- (PA5): For all A,f:(summable)A->X, B:@A, B;f = f o B = in summable.
11. (above)|- (PA6): For all f:{}->X ( f:summable and +f=0 ).
}=::PARTIALLY_ADDITITIVE.
Example.
|-PARTIALLY_ADDITITIVE(X=>Sets, +=>(|), summable=>|[A]A->X).

Binary Relations
1. RELATIONS::=
  Net{
  1. x = y = z iff x=y and y=z. So, this convention is adopted in MATHS. It is also generalized so that
  2. =(x,y,z) iff x=y and y=z. This turns out to be useful short hand in many special formal systems. A precisely similar convention is adopted by David Gries and Fred Schneider in thier "A Logical Approach to Discrete Mathematics". Operators with the aboveproperty are said (by them) to be "conjunctional". I call them "parallel operators.
    For X:Sets, R:@(X,X), w,x,y,z:X, L:#X,
  3. x R z::=R(x,y) ::=(x,y).R,
  4. x R y R z::= R(x,y,z) ::= (x R y) and (y R z),
  5. w R x R y R z::=R(w,x,y,z) ::=(w R x) and (x R y) and (y R z),
  6. if |L| > 1 then R(L)::= (L.1st R L.2nd) and R(L.rest).
    This can be extended so that
  7. (x < y <= z = w) iff (x<y and y<=z and z=w).
    For X:Sets, R,S,T:@(X,X), w,x,y,z:X,
  8. x R y S z::= (x R y) and (y S z),
  9. w R x S y T z::=(w R x) and (x S y) and (y T z),
    
    Kinds of relations
    For X:Sets, Y:=@(X,X), I:=Id(X), 0:Y:={},
  10. Transitive(X)::={R:Y || R;R ==> R },
  11. Reflexive(X)::={R:Y || R = /R },
  12. Irreflexive(X)::={R:Y || 0 = I & /R },
  13. Antireflexive(X)::={R:Y || 0 = R & /R },
  14. Dichotomettic(X)::={R:Y || Y >== {R, /R }},
  15. Trichotmettic(X)::={R:Y || Y >== {R, /R, I}},
  16. Symmetric(X)::={R:Y || R = /R },
  17. Antisymmetric(X)::={R:Y || R & /R = I},
  18. Asymmetric(X)::={R:Y || R ==> Y ~/R },
  19. Total(X)::={R:Y || Y ~R = /R },
  20. Complete(X)::={R:Y || Y = R | /R },
  21. Euclidean(X)::={R:Y || /R;R ==> R },
  22. Dense(X)::={R:Y || R ==> R;R },
  23. Confluent(X)::={R:Y || /R;R ==> R;/R },
  24. Rooted(X)::={R:Y || Y = do(/R);do(R) },
  25. Transitively_Connected(X)::={R:Y || Y = do(/R|R) },
  26. Connected(X)::= Total(X) & Complete(X),
  27. Serial(X)::=(Transitive(X) & Connected(X))~Reflexive(X).
  28. (above)|- (ITisAT): Irreflexive(X) & Transitive(X) = Asymmetric(X) & Transitive(X).
    Ordering
    Orders are defined by special kinds of relations:
  29. Strict_partial_orders(X)::=Irreflexive(X) & Transitive(X).
  30. Quasi_orders(X)::= Reflexive(X) & Transitive(X) .
  31. Partial_orders(X)::=Quasi_orders(X) & Antisymmetric(X).
    The symbols <, <=, >, and >= are used to indicate orders and the following interval notation is standard:
  32. x..y::= {z. x<=z<=y).
  33. x..*::= {z. x<=z).
  34. *..y::= {z. z<=y}.
    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 ]
    
    Left and Right Limited relations.
    Limited relations can not be repeated for ever either forward or backward. For example if one repeatedly takes smaller positive numbers then we ultimately hit 1 and stop.
  35. Right_limited(X)::={R:Y || for no S:@Nat-->X ( R(S) ) },
  36. Left_limited(X)::={R:Y || for no S:@Nat-->X ( /R(S) ) }.
  37. |- (Nat_well_ordered): < in Left_limited(Nat)~Right_Limited(Nat).
  38. These left and right limited orders are used to prove the termination and correctness of algorithms.
  39. (above)|- (LR): For all X, R, R in Left_limited iff /R in Right_limited.
    Equivalence Relations
  40. Equivalences(X)::=Reflexive(X) & Symmetric(X) & Transitive(X).
  41. equivalence_relation::=Equivalences.
  42. (partitions)|- (EP): For X:Sets, R:equivalence_relation(X), X>==X/R. [See Logic.Sets.partitions.]
  43. For f:B^A, congruences(f) ::{R:equivalence_relation(A)|| for all x,y:A(if x R y then f(x) R f(y))}.
  44. For f:C^(A><A), congruences(f)::={R:equivalence_relation(A) || for all x,y, x2,y2:A(if x R y and x2 R y2 then f(x,x2)R f(y,y2))}.
    
    Properties of specifications
    Mili et al. 89, Jaoua Mili et al 91
  45. For X,Y: Sets, R,S: @(X,Y), R is_more_defined_than S::=pre(S)==>pre(R) and for all x:pre(S) (x.R==>x.S).
  46. |- (Semi Inv): for all R, R==>R;/R;R.
  47. For X,Y, Regular(X,Y)::@@(X,Y)={R || R;/R;R ==> R},
  48. Rational(X,Y)::@@(X,Y)={R||for some X, f,g :dom(R)->X(R=f;/g)},
  49. Uniform(X,Y)::@@(X,Y)={R || (post(R)>=={u.R||u:pre(R)}) }.
  50. |- (RRU): For X,Y, Regular(X,Y) = Rational(X,Y) = Uniform(X,Y).
  51. |- (RI): Regular(X,Y) = {R || R;/R;R=R}.
  52. For X,Y, R, kernel(R)::@(X,X)= ({}<>(2nd).R==>(1st).R), nucleus(R)::@(X,X)=R;/R.
  53. (above)|- (KR): kernel(R) in reflexive & transitive.
  54. (above)|- (NR): nucleus(R) in reflexive & symmetric.
  55. (above)|- (ER): For all X,Y, if equivalence(R) then R is Regular(X,Y).
  56. (above)|- (CR): For all X,Y, R, W:Sets, f:W->X, if R:Regular(X,Y) then f;R is Regular(W,Y).
  57. (above)|- (RNK): For all X,Y, R, if R:Regular(X,Y), nucleus(R) = kernel (R) in reflexive & symmetric & transitive.
  58. (above)|- (Ass R): form(x'=f(x,...)) is regular.
  59. ...
  }=::RELATIONS.
2. MODULUS::=following,
  Net
  1. 17 = 1 modulo 16 meaning that multiples of 16 can be ignored. This is easy to generalize and turns out to be a useful idea. Formally a function always indicates a degree of ignorance of its arguments: |- For A,B:Sets, R:@(B,B) , f:A->B, R mod f::@(A,A)=f;R;/f.
    Hence
  2. For A,B:Sets, R:@(B,B) , f:A->B, (x R y wrt f) ::@= x (R mod f) y.
  (End of Net)
. . . . . . . . . ( end of section Binary relations) <<Contents | End>>
QUOTIENT_SETS::=
Net{
1. (Quotient set lemma)|- (QS0): For S,X:Sets, E:equivalence_relation(S), f:S->X ( E==>(= mod f) iff for one g:S/E->X(f=g o map [e](e/E])),
2. (Quotient set lemma)|- (QS1): For S,X:Sets, E:equivalence_relation(S), f:S->X ( E=(= mod f) iff for one g:S/E-->X(f=g o map [e](e/E])).
}=::QUOTIENT_SETS.
Structure preserving Maps and functions
MORPHISMS::=
Net{
1. name_of_structure:{unary, semigroup, monoid, group, semiring,...},
2. arrow:Arrows,
3. A,B describe the systems - typically a set and some operations. If several structures are preserved then their names can be listed: (N1,N2,N3,...) A arrow B::= &[i:1..](N[i])A arrow B
  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:
4. For X,Y:T, f:(T^n) ->T, a:arrow, (f)X a Y ::={ m:X a Y||m o (f.X)=(f.Y) o m}, -- (m is implicitly extended from X->Y to X^n->Y^n).
  
  Example
5. double:(+)Nat->Nat. double:(-)Int->Int.
  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:
6. For X,Y:T, R:@(#T), (R)X->Y::={m:X->Y || for all x:#X( if x in R then m(x) in R )}.
  
  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
7. For m:((~R)X->Y) & ((R)X->Y), for all x, x in R iff f(x) in R.
  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:
8. For a:Arrows, X,Y:Sets, x:X,y:Y, (X,x)a(Y,y) ={f:X a Y || f(x)=y}.
9. For a:Arrows, X,Y:Sets, +:infix(X),*:infix(Y), (X,+)a(Y, *) ::={f:X a Y || for all x1,x2:X (f(x1+x2)=f(x1)*f(x2))}.
10. For a:Arrows, X,Y:Sets, R:@(X,X), S:@(Y,Y), (X,R)a(Y, S) ::={f:X a Y || for all x1,x2:X, if x1 R x2 then f(x1) S f(x2))}.
  Hence to declarations like
11. log::(Positive&Numbers,(<),*,1)---(Numbers,(<),+,0).
  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.
}=::MORPHISMS.

. . . . . . . . . ( end of section The standard MATHS assumptions and definitions) <<Contents | End>>

Notes on MATHS Notation

Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

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

The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

For a more rigorous description of the standard notations see

STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

Glossary

above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).

given::reason="I've been told that...", used to describe a problem.

given::variable="I'll be given a value or object like this...", used to describe a problem.

goal::theorem="The result I'm trying to prove right now".

goal::variable="The value or object I'm trying to find or construct".

let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.

hyp::reason="I assumed this in my last Let/Case/Po/...".

QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.

QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.

RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

Contents

The standard MATHS assumptions and definitions

Definition of the standard package

Parallelism

Ordering

Equivalence Relations

Glossary