[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng Dept] / [R J Botting] / [ MATHS ] / math_45_Three_Operators
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Feb 26 11:18:23 PST 2008

Contents

    Three or More Infix operators

      The basis is
    1. ALGEBRA::=Net{ Set:Sets, ... }. to this a number of binary and unary operators are added and certain axioms assumed. These generate a rich set of results.

      Tarski turns up in most specialized systems.

      High School Identities

        Burris & Lee 93, Stanley Burris and Simon Lee, "Tarski's High School Identities", American Math Monthly V100n3(Mar 93) pp231-236
      1. HSI_bar::=
        Net{
          abstracted from the high school algebra of integers wthout powers.
        1. ALGEBRA.
        2. +::infix(Set).
        3. *::infix(Set).
        4. (STANDARD)|-(*) higher_priority_than (+).
        5. 1::Set.
        6. For x,y,z:Set.
        7. |- (HS1): x+y=y+x.
        8. |- (HS2): x+(y+z)=(x+y)+z.
        9. |- (HS3): x*1=x.
        10. |- (HS4): x*y=y*x.
        11. |- (HS5): x*(y*z)=(x*y)*z.
        12. |- (HS6): x*(y+z)=(x*y)+(x*z).

        }=::HSI_bar.
      2. HSI::=
        Net{
          abstracted from the high school algebra of integers with powers.
        1. |- (basis): HSI_bar. (^) ::infix(A).
        2. |- (priority): (^) higher_priority_then (*).
        3. |- (HS7): 1^x = 1,
        4. |- (HS8): x^1 = x,
        5. |- (HS9): x^(y+z) = (x^y) * (x^z),
        6. |- (HS10): (x*y)^z = (x^z) * (y^z),
        7. |- (HS11): (x^y)^z = x^(y*z).

          [click here [socket symbol] if you can fill this hole]


        }=::HSI.

      3. (above)|-(Nat, +, *,^,1) in $ HSI_bar.
      4. (above)|-For many H: $ HSI (H<>(Nat, +, *,^, 1)).

        Suppose that NAT is the system of logic that describes the natuural numbers: Nat=$ NAT.

      5. (above)|-theorems(NAT)<<=theorems(HSI).
      6. Consider{ Wilkie 80, "On exponentiation - a solution to Tarski's high school algebra problem", preprint, Oxford University, 1980.
      7. W(x,y)::=( ((1+x)^y+(1+x+x^2)^y)^x*((1+x^3)^x+(1+x^2+x^4)^x)^y) = ((1+x)^x +(1+x+x^2)^x)^y * ((1+x^3)^y + (1+x^2+x^4)^y)^x).
      8. if NAT then W(x,y).
      9. Some HSI and not W.

      10. }


      11. (above)|-not HSI_bar in decidable_algebras. Because there are no nice normal forms for HSI_bar.

        Constructions of HSI

      12. modified finite quotients of Nat -> (tail+loop)
      13. Heyting algebra(H, ....,0,1) without 0.
      14. Add (1st) to distributive lattice, semilattices, boolean rings,...
      15. 44 3-element HSI_algebras

        [click here [socket symbol] if you can fill this hole]

        Polynomials

      16. For n:Nat0, c:set^(0..n), x:set, poly(c)(x) ::set= +( c*(x^Id(0..n))).

      . . . . . . . . . ( end of section High School Identities) <<Contents | End>>

      .Roadworks_Ahead

      Modules

        [click here [socket symbol] if you can fill this hole]

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

      K-Algebras

        [click here [socket symbol] if you can fill this hole]

      . . . . . . . . . ( end of section K-Algebras) <<Contents | End>>

      Vector Spaces

      1. VECTOR::=following
        Net
        1. Scalar::Field=given.
        2. Vector:: Sets=goal.
        3. |- (VS0): GROUP(Vector, +, 0, -) and Abelian.
        4. For a,b:Scalar, u,v,w:Vector.
        5. *::infix(Scalar, Vector, Vector).
        6. (above)|-a * v in Vector.
        7. |- (VS1): a * (u+v) = a*u+b*v.
        8. |- (VS2): (a+b)*v = a*v + b*v.
        9. |- (VS3): (a*b)*v = a*(b*v).
        10. |- (VS4): 1 * v = v

          Many theorems follow for example

        11. (above)|- (VS5): 0*v = 0.
        12. (above)|- (VS6): -1 * v = -v.

          More Results: [click here [socket symbol] if you can fill this hole]

          Proof of VS5


          Let
          1. v:Vector,
          2. (VS2)|-(0+1)*v = 0*v + 1*v,
          3. (VS4)|-(0+1)*v = 0*v +v,
          4. (Field)|-1*v = 0*v + v,
          5. (-1)|-v = 0*v +v,
          6. (GROUP)|-0*v = v-v = 0

          (Close Let )

          Proof of VS6


          Let

          1. |- (let): v:Vector.
          2. (Scalar, Field)|-1 in Scalar,
          3. (-1)|--1 in Scalar,
          4. (-2)|-1 + -1 = 0,
          5. (-1)|-(1+ -1)*v = 0 * v,
          6. (-1, VS5)|-1*v + (-1)*v = 0,
          7. (-1)|-v + (-1)*v =0,
          8. (-1, GROUP)|-(-1)*v = -v.

          (Close Let )

        (End of Net)

        Simple Scalar Products and Inner Products
      2. For Scalar:Field, x,y: VECTOR(Scalar), <x|y> ::Scalar. [click here [socket symbol] if you can fill this hole]

        Also see example: [ math_95_Function_Spaces.html#Hilbert Space ]

        Linear maps on Vector Spaces

        Given two vector spaces V1 and V2

      3. LINEAR::=following
        Net
        1. Scalar::Sets=given.
        2. V1::VECTOR(Scalar)=given.
        3. V2::VECTOR(Scalar)=given.
        4. f::V1->V2=goal.
        5. For x,y:V1, a:Scalar.
        6. |-for all x,y (f(x+y)=f(x)+f(y)).
        7. |-for all a, x ( f(a*x) = a*f(x)).

        (End of Net)

        Dual Spaces and Inner Products

        For a Scalar:Field, Vector space V:VECTOR(Scalar) then define V*:the set of linear maps from V into Scalar is the dual vector space.
      4. DUAL::=following,
        Net
        1. Scalar::Sets=given.
        2. Vector::VECTOR(Scalar)=goal.
        3. For x,y:V, a:Scalar.
        4. Dual::={ f: Vector->Scalar . for all x,y (f(x+y)=f(x)+f(y))), for all a, x ( f(a*x) = a*f(x)) }
        5. For f,g:Dual.
        6. f+g::= map[x]( f(x)+g(x)).
        7. a * f::= map[x] a*f(x).
        8. (above)|-Dual in VECTOR(Scalar).

        (End of Net)

      5. For Scalar:Field, V1:VECTOR(Scalar), x:V,y: V*, <x|y> ::Scalar.

        Linear Maps

          Linear, quadratic, etc

          [click here [socket symbol] if you can fill this hole]

          Matrices

           Matrices are at least a convenient way to express how linear equations work. They form a complex algebra with addition, zero, subtraction, partial non-commutative multiplication, unit, with partially existing inverses. We can have matrices made up of any kind of numbers: integers, rationals, reals, and complex numbers.

        1. Matrix::@Sets, set of all matrices.
        2. Mat(R,C)::@Sets, set of R><C matrices.
        3. Row(R)::=Mat(R,1).
        4. Col(C)::=Mat(1,C).

          Matrices are two-dimensional arrays of elements and so are naturally related to maps with two-dimensional domains:

        5. Mat(R,C) --- (1..R)><(1..C) >-> Numbers.

          One simple notation is to use a table:

        6. Q::Mat(n,n)=following,
          (n-1)a+b(n-1)b00...00
          2 a(n-2)a+2 b(n-2)b0...00
          03 a(n-3)a+3 b(n-3)b...00
          004 a(n-4)a+4 b...00
          .....................
          0000...a+(n-1)bb
          0000...n an b
          [click here [socket symbol] if you can fill this hole]

          Frames of Reference

           [click here [socket symbol] if you can fill this hole]

        . . . . . . . . . ( end of section Linear Maps) <<Contents | End>>

      Boolean and Relation Algebras

        [Maddux96] Relation algebras have a long history and can be used in a natural way to express the semantics of programming languages. This is done by definining the meaning of a statement as a pair of elements in a relation algebra. The first can be any relation and indicates the relationship between the initial anf final states if the program terminates. The second part of the meaning of a statement is a conditional relation that describes when the statement does not terminate. Notice that in this model we can define about programs that would have an effect if they terminated even tho they but do not terminate

        Boolean Algebras

          Maddux's minimal axiomatic treatment below(BOOLEAN_ALGEBRA) is consistent with an alternate treatment [ BOOLEAN_ALGEBRA in math_41_Two_Operators ]

        1. BOOLEAN_ALGEBRA::=following
          Net

          1. |-ALGEBRA.
          2. B::=Set.
          3. For x,y,z:B.
          4. |- (BA0): ABELIAN_SEMIGROUP(B, +). (-) ::B->B.
          5. |- (BA1): for all x,y:B( x= -(-x+ -y)+ -(-x+y) ).
          6. (above)|- (BA3i): x+ -x = y+ -y.
          7. (above)|- (BA3ii): - -x = x.
          8. (above)|- (BA3iii): -x= -(x+y) + -(x+ -y).
          9. (above)|- (BA3iv): x+(y+ -y) = z+ -z.
          10. (above)|- (BA3v): x+x = x+ -(y+ -y).
          11. (above)|- (BA3vi): x+x = x.
          12. For x,y:B, x*y::=-(-x+ -y).
          13. (STANDARD)|-(*) higher_priority_than (+).
          14. (above)|- (BA3vii): x*x =x.
          15. (above)|- (BA3viii): x*y=y*x.
          16. (above)|- (BA3ix): (x*y)*z=x*(y*z).
          17. (above)|-ABELIAN_SEMIGROUP(B,*).
          18. (above)|- (BA3x): (x+y)*x=x.
          19. (above)|- (BA3xi): x = x*y +(x * -y).
          20. (above)|- (BA3xii): x=(x+ -y)*(x+y).
          21. (above)|- (BA3xiii): (x+y)* -x=y* -x.
          22. (above)|- (BA3xiv): x+x*y=x.
          23. (above)|- (BA3xv): x*(y+z)=x*y+x*z.
          24. (above)|- (BA3xvi): -(x+y)= -x * -y.
          25. (above)|- (BA3xvii): -(x*y)= -x + -y.
          26. (above)|- (BA3xviii): x+(y*z) = (x+y)*(x+z).
          27. (above)|- (BA3xix): ((-x)*y)+(x*z)=(x+y)*(-x+y).
          28. (above)|- (BA3xx): (v*w+ -v*x)* -(v*y+ -v*z) = v*w* -y + -v * x* -z.
          29. (above)|- (BA3xxi): x+y=x+(-x)*y.

            Proofs are on pages 8 to 10 of [Maddox96] where (BA3xx) for example is his 3(xx).


          30. (BA2i)|-one img(x:B. x+ -x) and one img(x:B. -(x+ -x)).

          31. 1::=the img(x:B. x+ -x).
          32. 0::=the img(x:B. -(x+ -x)).
          33. (above)|- (BA5i): 1 = x+ -x.
          34. (above)|- (BA5ii): 0 = x*(-x).
          35. (above)|- (BA5iii): -1 = 0.
          36. (above)|- (BA5iv): -0 = 1.
          37. (above)|- (BA5v): x.1 =1.
          38. (above)|- (BA5vi): x.0 = 0.
          39. (above)|- (BA5vii): x+0 = 0.
          40. (above)|- (BA5viii): x.1 = x.

          41. x<=y::= x+y=y.
          42. x>=y::= y<=x.


          43. (above)|- (BA7i): POSET(B, <=).
          44. (above)|- (BA7ii): 0<=x<=1.
          45. (above)|- (BA7iii): if x<=y then x+z<=y+z and x*y<=y*z.
          46. (above)|- (BA7iv): LATTICE(B, +, *).
          47. (above)|- (BA7v): x<=y iff -y <= -x iff x+y=y iff x*y=x iff -y+x=x iff -x+y=1 iff x*- y=0.
          48. (above)|- (BA7vi): x.y<=z iff y<= -x +z.


          49. (STANDARD)|-For I:Sets, X:I->B,
          50. +X::=sum of all X,
          51. *X::=product of all X,
          52. -X::= map[i:I](-X(i)).

            + and * are only partial maps from (I->B) into B. +X and/or *X may not exist.


          53. (above)|- (BA8i): if I={} then +X=0 and *X=1.
          54. (above)|- (BA8ii): if +X exists then *(-X) exists and -(+X)=*(-X).
          55. (above)|- (BA8iii): if *X exists then +(-X) exists and -(*X)=+(-X).
          56. (above)|- (BA8iv): For every y, *{x. x>=y} and +{x, x<=y} exist and are equal to y.


            (LATTICE): complete=existence of sums and products of any set of elements.

          57. (above)|-If complete then for all I,X(*X and +X exist).

          58. For I:Sets, X,Y:I->B.
          59. (STANDARD)|-
          60. X+Y::= map[i](X(i)+Y(i).
          61. (STANDARD)|-
          62. X*Y::= map[i](X(i)*Y(i).


          63. (above)|- (BA9i): If +X and +Y exist then +(X+Y)= (+X)+(+Y).
          64. (above)|- (BA9ii): If *X and *Y exits then *(X*Y) = (*X)*(*Y).
          65. (above)|- (BA9iii): If for all i(X(i)<= Y(i)) then (if +X and +Y exist then +X<= +Y) and (if *X and *Y exist then *X<= *Y).

          66. For T:Types, I,J:Sets(T), X:(I|J)->B, XI:=map[i:I]X(i), XJ:=map[i:J](X(i)).
          67. (above)|- (BA10i): if +XI and +XJ exist then +X=+XI + +XJ.
          68. (above)|- (BA10ii): BA10i((+)=>(*)).
          69. (above)|- (BA10iii): if +XI and +XJ exist and I==>J then +XI <= +XJ.
          70. (above)|- (BA10iv): BA10iii((+)=>(*)).

            Operators

            Dual functions:
          71. For all f:B->B, dual(f)::= -(f(-(_))).
          72. (above)|- (BA11): dual o dual = Id.

          73. For f, conjugates(f)={g. for all x,y(f(x)*y =0 iff x.g(y)=0}.


          74. (above)|- (BA14i): for all g,h:conjugates(f)(g=h).
          75. (above)|- (BA14ii): f in conjugates(g) iff g in conjugates(f).

            (f and g are conjugate) ::= f in conjugate(g).

          76. normal::@(B->B)={f. f(0)=0}.
          77. monotonic::={f. for all x<=y(f(x)<=f(y)}.
          78. additive::={f. f(x+y)=f(x)+f(y)}.
          79. multiplicative::={f. f(x*y)=f(x)*f(y)}.
          80. completely_additive::={f. for all I:Sets, X:I->B(if +X exists and I<>{} then +f(X) exists and +f(X) = f(+X))}.

            Similarly for complete_multiplicative.

          81. universally_additive::= completely_additive & normal,

          82. universally_multiplicative::=completely_multiplicative & {f. f(1)=1}.


          83. (above)|- (BA16): for all x, (x*_) and (_*x) are universally_additive & completely_multiplicative and (x+_) and (_+X) are universally_multiplicative and completely_additive.


          84. (above)|- (BA17): completely_additive==>additive==>monotonic and completely_multiplicative==multiplicative==>monotonic.
          85. (above)|- (BA19iii): for W:{(universally_additive+>universally_multiplicative), (completely_additive+>completely_multiplictive), (finitely_additive+>finitely_multiplicative), f:B->B, w:W, f in w(1) iff dual(f) in w(2).


          86. (above)|- (BA18i): the congugate(f) = map[y](*{x: y<=dual(f)(x)}) -- if it exists.
          87. (above)|- (BA18ii): some conjugate(f) iff f in univerally_additive and for all y( *{x. y<=dual(f)(x) } exists).


          88. (above)|- (BA19): f and g are conjugate iff for all x,y(f(x*-g(y)) <= f(x)*-y) iff for all x,y( g(y* -f(x))<= g(y)&-x) iff f and g are normal and for all z,y(f(y)*z <= f(y*g(z)) and g(z)*y<=g(z*f(y))) ).

          89. f^i::=result of composing f with itslef i times.
          90. f^0=0.
          91. f^(i+1)=f(f^i).


          92. (above)|- (BA21i): constant_functions are monotonic and Id in monotonic and sum and product of monotonic functions are monotonic.
          93. (above)|- (BA21ii): if complete then for all f: I->monotonic, +f and *f are monotonic.
          94. (above)|- (BA21iii): if complete then for all f:B><B->B(if for all z(f(_,z) in monotonic) then *{z. z>=f(_,z)} and +{z. z<=f(_,z)} are monotonic).

            Tarski Fixed Points

          95. For X:Sets, f:X->X, fixed(f)::={x. x=f(x)}.
          96. For X:Sets, f:X->X, decreased(f)::={x. x<=f(x)}.
          97. For X:Sets, f:X->X, increased(f)::={x. x>=f(x)}.

          98. BA22::=following
            Let
              LATTICE(A, <=, complete). f:monotonic(A->A).


            1. (above)|- (BA22i): fix(f)<>{} and LATTICE(fix(f), <=).
            2. (above)|- (BA22ii): +decreased(f) = +fixed(f) in fixed(f).
            3. (above)|- (BA22iii): *increased(f) = *fixed(f) in fixed(f).

            (Close Let )

          (End of Net)

        . . . . . . . . . ( end of section Boolean Algebras) <<Contents | End>>

        Relation Algebras

          Maddux traces this theory Back from Pierce to Boole and De Morgan, and forwrd to Schoder. Tarski also worked on this.

        1. RELATION_ALGEBRA::=following
          Net

          1. |-BOOLEAN_ALGEBRA(A, +, -).

            Note: complete in {true,false) is inherited from the Boolean algebra.

            Semicolon represents an associative operator with a unit:

          2. |-MONOID(A,;, I)
          3. (;) higher_priority_than (+) and (*).
          4. (;) distributes_over (+).


          5. |-UNARY(A,(/)).


          6. |- (RA4): for all x, /(/x) = x.
          7. |- (RA5): /(x+y) = /x + /y.
          8. |- (RA6): /(x;y) = /y ; /x.
          9. |- (RA7): /x;-(x;y) + -y = -y.
          10. |- (RA7): /x;-(x;y) <= -y and /x;-(x;y)*y =0.
          11. x \dagger y::= - ( -x * -y).

          12. Example::=following
            Net
              U:Sets.
            1. (above)|-RELATION_ALGEBRA(@(U,U), (+)=>(|), (*)=>(&), 1=>U><U, I=>Id, 0=>{}).

            (End of Net)

          13. proper::@=`the relation algebra is of a set of binary relations: for some U(A=@(U,U) and Example)`.
          14. representable::@=isomorphic to a proper relation algebra.

            However, there are an infinity of relation algebras that are not represented by an @(U,U) for any U.


          15. (above)|- (RA24i): x <= y iff /x <= /y.
          16. (above)|- (RA24ii): /0 = 0.
          17. (above)|- (RA24iii): /1 = 1.
          18. (above)|- (RA24iv): /(-x) = -(/x).
          19. (above)|- (RA24v): /(x*y) = (/x)*(/y).
          20. (above)|- (RA24vi): 0 = /x * y iff 0 = x * /y.
          21. (above)|- (RA24vii): (/) is universally additive and universally multiplicative.
          22. (above)|- (RA24viii): /I=I.


          23. (above)|- (RA24ix): x;(y+z)= x;y + x;z.
          24. (above)|- (RA24x): if x <= y then z;x <= z;y and x;z <= y;z.
          25. (above)|- (RA24xi): the functions (x;_) and (/x;_) are conjugate.
          26. (above)|- (RA24xii): -(x;y);/x <= y.
          27. (above)|- (RA24xiii): (_;x) conjugate (_;/x).


          28. (above)|- (RA24xiv): (x;y)*z=0 iff (/x;z)*y=0 iff (z;/y)*x=0.
          29. (above)|- (RA24xv): (x;_) and (_;x) are universally_additive.
          30. (above)|- (RA24xvi): (x;y)*z <= x;(y * (/x; z)).
          31. (above)|- (RA24xvii): (y;x) * z <= (y*(z;/x));x).


          32. (above)|- (RA24xviii): x;0 = 0 = 0;x.
          33. (above)|- (RA24xix): x;I = x = x;I.
          34. (above)|- (RA24xx): x <= x;1.
          35. (above)|- (RA24xxi): x <= 1;x.
          36. (above)|- (RA24xxii): 1;1=1.


          37. (above)|- (RA24xxiii): (x;y_ * -(x;z) = x; (y*-z)*-(x;z).
          38. (above)|- (RA24xxiv): -(x;y) + (x;z) = -(x;(y&-z)) + x;z.

          39. domain_elements::@A={x:A. x;1=x).
          40. For e,d:domain_elements.
          41. (above)|- (RA24xxv): (-e);1= -e.
          42. (above)|- (RA24xxvi): (e*y);z = e*(y;z).
          43. (above)|- (RA24xxvii): (e*d) in domain_elements.
          44. (above)|- (RA24xxviii): (e*I);y=e*y.
          45. (above)|- (RA24xxix): (y*/e);z=y;(e*z) = (y*/e);(e*z).

          46. conditional_elements::@A={c:A. c<=I}.
          47. For c,c1:conditional_elements.
          48. (above)|- (RA24xxx): /c = c.
          49. (above)|- (RA24xxxi): (c;1)*y = c*y.
          50. (above)|- (RA24xxxii): -(c;1)*I= (/c)*I.
          51. (above)|- (RA24xxxiii): c;c1 = c*c1.
          52. (above)|- (RA24xxxiv): (c;z) * (c;c1) = (c*c1);z.
          53. (above)|- (RA24xxxv): (c;y)*-z = (c;z)* -(c;z).

            In the Example.domain_elements={ W><U. W==>U}.


          54. (above)|-BOOLEAN_ALGEBRA(domain_elements, complete)

          55. functional_elements::@A={x. /x;x=I}.

            Example.functional_elements are partial functions.


          56. (above)|- (RA28i+ii): SEMIGROUP(functional_elements, (;)).
          57. (above)|- (RA28iii): x in functional_elements iff for all y( (x;y) * (x;-y) = 0).
          58. (above)|- (RA28iv): conditional_elements ==> functional_elements.

          59. For all x:A, i:Natoo,
          60. x^0::= I,
          61. x^(i+1)::=x;(x^i).
          62. For all x:A, if it exists, x^oo::= +[i:Natoo](x^i).


          63. (above)|- (RA30): If complete then q^oo;p=*{x. x>=p+q;x} and -(q^oo;-p) = +{x. x<= p*-(q;-x))} and *{x. x>=p+q;x};y = *{x. x>=p;y+q;x}.


          64. |-For p,q:A, fixed(p,q)={c. c=p+q;c}.
          65. (above)|-fixed(p,q) = fixed( p+q:(_) ).
          66. |-For p,q:A, decreased(p,q)={c. c<=p+q;c}.
          67. |-For p,q:A, increased(p,q)={c. c>=p+q;c}.
          68. (above)|- (BA31i): for c:fixed(q,t), +decreased(p+q,t)= +decreased(p,t)+c.
          69. (above)|- (BA31ii): +decreased(p+q,t)=+decreased(p,t)+ +decreased(q,t).
          70. (above)|- (BA31ii): *increased(p*q,t)=*increased(p,t) * *increased(q,t).

            Pseudo-inverses

            In general there is no y such that x;y=I.

            Dijkstra's Discipline of Programming turns on defining and using the properties of a kind of pseudo-inverse - the weakest condition needed to guarantee termination with a given property.

            Maddux defines something like this:

          71. wlp(r)::=map[x]( -(r;-x)). This relation does not allow non-x to occur.

            Pierce and De Morgan studied -(-x;y).


          (End of Net)

        . . . . . . . . . ( end of section Relation Algebras) <<Contents | End>>

        Glossary

      1. distributes_over::=* distributes over + iff x*(y+z)=(x*y)+(x*z). img(x:X. e(x)) ::= {y. for some x:X(y=e(x))}. If f is a function from X to Y then f(A)=img(a:A. f(a)). Another equivalent form: img(x:X. e) = X.[x](e)

        Links

      2. STANDARD::= See http://cse.csusb.edu/dick/maths/math_11_STANDARD.html.

      3. ABELIAN_SEMIGROUP::= See http://cse.csusb.edu/dick/maths/math_32_Semigroups.html#ABELIAN_SEMIGROUP.
      4. SEMIGROUP::= See http://cse.csusb.edu/dick/maths/math_32_Semigroups.html.
      5. MONOID::=SEMIGROUP with u:units(Set,op).
      6. GROUP::= See http://cse.csusb.edu/dick/maths/math_34_Groups.html#GROUP.

      7. UNARY::=ALGEBRA with function:Set->Set. [ math_15_Unary_Algebra.html ]

      8. Field::= See http://cse.csusb.edu/dick/maths/math_41_Two_Operators.html#Field.

      9. POSET::= See http://cse.csusb.edu/dick/maths/math_21_Order.html#POSET
      10. LATTICE::= See http://cse.csusb.edu/dick/maths/math_41_Two_Operators.html#LATTICE.

      11. See_also::= See http://cse.csusb.edu/dick/maths/math_31_One_Associative_Op.html

      . . . . . . . . . ( end of section Boolean and Relation Algebras) <<Contents | End>>

      Varieties

        [Maddux96] p23

        If an net is defined as an algebra with nothing but equations in its axioms then it "forms a variety". Therefore there are subalgebras, homomorphic images and direct products with the same axioms.

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

    . . . . . . . . . ( end of section Three or More Infix operators) <<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

  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