[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_11_STANDARD
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun Oct 2 12:00:11 PDT 2011

Contents


    The standard MATHS assumptions and definitions

      Definition of the standard package

      As with the Ada STANDARD package, all MATHS documents can use the definitions collected in STANDARD without having to explicitly refer to it. In other words it is as if the term STANDARD is asserted at the start of all MATHS documents. This invisible term is defined as a package of conventions as follows:
    1. 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.

      Standard Terms and abbreviations

      The following are handy terms to use in many documents.
    2. TERMS::=following
      Net
        In describing a problem:
      1. given::variable="I'll be given a value or object like this...", used to describe a problem.
      2. goal::variable="The value or object I'm trying to find or construct".

        In proofs:

      3. given::reason="I've been told that...", used to describe an assumption.
      4. goal::theorem="The result I'm trying to prove right now".
      5. 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). "(above)" can be abbreviated "()".

      6. 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.
      7. hyp::reason="I assumed this in my last Let/Case/Po/...".
      8. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
      9. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
      10. RAA::conclusion="Reducto Ad Absurdum". This forces you to discard the last assumption (let) that you introduced but lets you include its negation as a new result.

      (End of Net)

      Coercions

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

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

    5. 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:
    6. UNARY::syntax=Net{ u:#char, a:@#char, e:= a | u a | a dot u }.

    7. Example::=
      Net{
        Given this definition then the following MATHS statement,
      1. |-UNARY( u=>"sqrt", a=>term, e=>expression) generates the following documentation:
      2. expression::= term | "sqrt" term | term dot "sqrt".

      }=::Example.

    8. UNARY::semantics=
      Net{
      1. MAP.
      2. For X:Set, unary(X)::=X^X.
      3. For X:Set, f:unary(X), f:: @X->@X = map [A:@X] {f(a) || a:A},
      4. 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))).
      5. For X:Set, f:unary(X), fixed_points(f)::@X= {x:X. f(x)=x}.

      }=::UNARY.

      Infix operations

      1. INFIX_SYNTAX::syntax=Net{ f:#char, s:@#char, S:= f P(s) | P(s) dot f | "(" L(s, f) ")" }.
      2. Example_infix::=
        Net{
          So,
        1. INFIX_SYNTAX(f=>"<", s=>expression, S=>relation) which is short for
        2. expression::= "+" P(product) | P(product) dot "+" | "(" L(product, "+") ")", and
        3. INFIX_SYNTAX(f=>"+", s=>product, S=>expression) means
        4. relation::= "<" P(expression) | P(expression) dot "<" | "(" L(expression, "<" ) ")".

        }=::Example_infix.

        Standard infix operator priorities

        [ notn_12_Expressions.html#Precedence and Typing ]
      3. (*) and (/) take precedence over (+) and (-)
      4. (and) and (not) take precedence over (or)
      5. (&), (;), (o), (!) and (~) take precedence over (|)

        Serial and Parallel Operators

        In normal mathemetics
      6. a<b<c means (a<b) and (b<c)

        but

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

      8. SERIAL_AND_PARALLEL::=
        Net{
          -- syntax

        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. SERIALITY::=
          Net{
          1. INFIX_SYNTAX(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.

        10. 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:

        11. PARALLELISM::=
          Net{
          1. INFIX_SYNTAX.
          2. T::Types,
          3. g::T><T->@.
          4. |-symbol( f, T><T->@, g).
          5. |-For a,b:T, a g b = (a,b).g = g(a,b).
          6. |-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).
          7. |-for n:4.., a:T^n, g(a) = a.g = g ( g(front(a)) and g(a(n-1),a(n) ) ).

          }=::PARALLELISM.

        12. 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, @).


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

      9. INFIX::semantics=
        Net{
          For X:Sets,
        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, (x *_) ::= map [y:X](x * y),
        10. For *:infix(X), y:X, (_* y) ::= map [x:X](y * x),
        11. For *:infix(X), (*) ::=map [x,y](x*y).
        12. (def)|- (I0): For *:infix(X), x, y:X, (x*y) = (*)(x,y) = (x,y).(*) = (x*_)(y)=y.(x*_)=(_*y)(x)=x.(_*y).
        13. (M0)|- (I1): For *:infix(X), x, y:X,
        14. (_*x);(_*y)=(_*(x*y))
        15. and (x*_);(y*_)=((y*x)*_)
        16. and (x*_)=x*(_)
        17. and (_*y)=(_)*y.

          Note. (_)*(_) and (*) have different domains, (_)*(_) is a unary operator but (*) is a binary one.

          Overloadings -- Sets and maps in infix expressions

        18. For *:infix(X), *::(@X)><(@X)= map [A,B] {a * b|| a:A, b:B},
        19. For *:infix(X), *::( X)><(@X)= map [x,B] {x * b|| b:B},
        20. For *:infix(X), *::(@X)><( X)= map [A,x] {a * x|| a:A}.
        21. {1,2,3} + 1 = 1+ {1,2,3} = {2,3,4}.
        22. {1,2} + {3,4} = {4,5,6}.

        23. For *:infix(X), *::(X^A)><(X^A)= map [f,g] (map [a:A] ( f(a) * g(a) ) ),
        24. For *:infix(X), *::( X) ><( X^A)=map [x,f] (map [a:A] ( x * f(a) ) ),
        25. For *:infix(X), *::(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 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.

          Serial operations

        26. For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X).
        27. For A, +A :: X,
        28. |- (Ser0): if |A|=0 then +A=0,
        29. |- (Ser1): if |A|=1 then +A=the (A),
        30. |- (Ser2): if |A|>1 then for all Y:@A(+(A&Y) + +(A~Y))}.
        31. (def, induction)|- (Ser3): for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, p:A(1)-(1)A, +p(A)=+A ).
        32. (def, induction)|- (Ser4): for +:associative(X) & commutative(X), 0:units(X,+), A:Finite_Sets, for B, (if B<==A then +A = +(A&B) ).
        33. (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)).

        34. For X, A, f:X^A, +f :: X,
        35. |- (SerF0): if |A|=0 then +f=0,
        36. |- (SerF1): if |A|=1 then for some y:A(+f=f(y)),
        37. |- (SerF2): if |A|>1 then for all Y:@A( +f=+(f o Y) + +(f o (A~Y)).

          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.

        38. (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 ).
        39. (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) ).
        40. (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

        41. ASSIGNMENTS::=
          Net{

            [ math_14_Dynamics.html ]

          1. For U:documentation, x:variable(U), e:expression(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.


        }=::INFIX.

      . . . . . . . . . ( end of section Infix operations) <<Contents | End>>

      Indexed Sets and Families

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

    10. PARTIALLY_ADDITITIVE::=
      Net{
        It is sometimes possible to generalize the standard MATHS convention for serial operations from finite sets to functions over countable infinite sets. See Chapter 3 of Manes and Arbib [86]. For example
      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.

    11. |-PARTIALLY_ADDITITIVE(X=>Sets, +=>(|), summable=>|[A]A->X).

      Binary Relations

      1. RELATIONS::=
        Net{

          Parallelism

          In normal mathematics, unlike must programming language, we have
        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),
        4. R(x,y)::=(x,y).R,
        5. x R y R z::= R(x,y,z),
        6. R(x,y,z)::= (x R y) and (y R z),
        7. w R x R y R z::=R(w,x,y,z),
        8. R(w,x,y,z)::=(w R x) and (x R y) and (y R z),
        9. if |L| > 1 then R(L)::= (L.1st R L.2nd) and R(L.rest).

          This can be extended so that

        10. (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,

        11. x R y S z::= (x R y) and (y S z),
        12. 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:={},
        13. Transitive(X)::={R:Y || R;R ==> R },
        14. Reflexive(X)::={R:Y || R = /R },
        15. Irreflexive(X)::={R:Y || 0 = I & /R },
        16. Antireflexive(X)::={R:Y || 0 = R & /R },
        17. Dichotomettic(X)::={R:Y || Y >== {R, /R }},
        18. Trichotmettic(X)::={R:Y || Y >== {R, /R, I}},
        19. Symmetric(X)::={R:Y || R = /R },
        20. Antisymmetric(X)::={R:Y || R & /R = I},
        21. Asymmetric(X)::={R:Y || R ==> Y ~/R },
        22. Total(X)::={R:Y || Y ~R = /R },
        23. Complete(X)::={R:Y || Y = R | /R },
        24. Euclidean(X)::={R:Y || /R;R ==> R },
        25. Dense(X)::={R:Y || R ==> R;R },
        26. Confluent(X)::={R:Y || /R;R ==> R;/R },
        27. Rooted(X)::={R:Y || Y = do(/R);do(R) },
        28. Transitively_Connected(X)::={R:Y || Y = do(/R|R) },

        29. Connected(X)::= Total(X) & Complete(X),
        30. Serial(X)::=(Transitive(X) & Connected(X))~Reflexive(X).


        31. (above)|- (ITisAT): Irreflexive(X) & Transitive(X) = Asymmetric(X) & Transitive(X).

          Ordering

          Orders are defined by special kinds of relations:
        32. Strict_partial_orders(X)::=Irreflexive(X) & Transitive(X).
        33. Quasi_orders(X)::= Reflexive(X) & Transitive(X) .
        34. Partial_orders(X)::=Quasi_orders(X) & Antisymmetric(X).

          The symbols <, <=, >, and >= are used to indicate orders and the following interval notation is standard:

        35. x..y::= {z. x<=z<=y).
        36. x..*::= {z. x<=z).
        37. *..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.

        38. Right_limited(X)::={R:Y || for no S:@Nat-->X ( R(S) ) },
        39. Left_limited(X)::={R:Y || for no S:@Nat-->X ( /R(S) ) }.


        40. |- (Nat_well_ordered): < in Left_limited(Nat)~Right_Limited(Nat).
        41. These left and right limited orders are used to prove the termination and correctness of algorithms.


        42. (above)|- (LR): For all X, R, R in Left_limited iff /R in Right_limited.

          Equivalence Relations

        43. Equivalences(X)::=Reflexive(X) & Symmetric(X) & Transitive(X).

        44. equivalence_relation::=Equivalences.


        45. (partitions)|- (EP): For X:Sets, R:equivalence_relation(X), X>==X/R. [See Logic.Sets.partitions.]

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

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

          Source: Mili et al. 89, Jaoua Mili et al 91

        48. 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).
        49. |- (Semi Inv): for all R, R==>R;/R;R.
        50. For X,Y, Regular(X,Y)::@@(X,Y)={R || R;/R;R ==> R},
        51. Rational(X,Y)::@@(X,Y)={R||for some X, f,g :dom(R)->X(R=f;/g)},
        52. Uniform(X,Y)::@@(X,Y)={R || (post(R)>=={u.R||u:pre(R)}) }.
        53. |- (RRU): For X,Y, Regular(X,Y) = Rational(X,Y) = Uniform(X,Y).
        54. |- (RI): Regular(X,Y) = {R || R;/R;R=R}.
        55. For X,Y, R, kernel(R)::@(X,X)= ({}<>(2nd).R==>(1st).R),
        56. nucleus(R)::@(X,X)=R;/R.
        57. (above)|- (KR): kernel(R) in reflexive & transitive.
        58. (above)|- (NR): nucleus(R) in reflexive & symmetric.
        59. (above)|- (ER): For all X,Y, if equivalence(R) then R is Regular(X,Y).
        60. (above)|- (CR): For all X,Y, R, W:Sets, f:W->X, if R:Regular(X,Y) then f;R is Regular(W,Y).
        61. (above)|- (RNK): For all X,Y, R, if R:Regular(X,Y), nucleus(R) = kernel (R) in reflexive & symmetric & transitive.
        62. (above)|- (Ass R): form(x'=f(x,...)) is regular.
        63. ...


        }=::RELATIONS.

      2. MODULUS::=following,
        Net
          Mathematicians are familiar with
        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>>

    12. QUOTIENT_SETS::=
      Net{

        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

      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

    13. MORPHISMS::=
      Net{
        If B is a mathematical structure and f:B^A then A/f can have an identical structure defined on it.

        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

      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 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 ]

    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

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

    Glossary

  2. 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).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. 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.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

End