[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / intro_standard
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Thu Jul 18 11:36:41 PDT 2013


    A "Cheat Sheat" Of Standard MATHS Notation


      This page is a summary of the standard notational conventions of the MATHS language for writing mathematics and logic. These conventions are defined to pack as much mathematical/logical meaning into the ASCII character set as possible.


      and, or, notinfix(@)Boolean operators
      if P then Q@implication, true iff P false or Q true.
      if P then Q else R@= (if P then Q)and(if not P then Q) = (P and Q)or(not P and R).
      iffinfix(@)If and only if

      (Close Table)
      [ PROPOSITIONS in logic_10_PC_LPC ]

      Quantifiers include: all, some, 0,1, 2,3,..., n, . 0..1, 0..2, .... n..m
      for all x:A (P)For all x in A, P is true
      for some x:A (P)For some x in A P is true
      for 0 x:A (P)= not for some x:A(P), for no x in A is P true
      for 1 x:A (P)For exactly one x in A, P is true
      for n x:A (P )For exactly n x...
      for 0..1 x:A (P)for 0 x:A (P) or for 1 x:A (P)
      for n..m x:A (P)Between n and m x's in A satisfy P
      for any x:T (P )Any number including none.
      for abf x:T (P )for all but a finite number
      for Q1 x1:T1, Q2 x2:T2... (P )You can put many quantifiers after one for.
      for Q T x (P )If the type is a name you can out it first.
      the x:A (P)The unique x in A satisfying P (or else undefined)
      x = yTrue if x and y are defined and equal, else false.
      x <> yNegation of x=y, Pascal and BASIC notation.
      x != yNegation of x=y, The C/C++/Java/PHP/ ... notation

      (Close Table)
      [ Lower_Predicate_Calculus_with_equality in logic_10_PC_LPC ]


      For Type T
      @TType whose elements a sets of objects of type T
      x in Ax is a member of A
      A ==>Bsubset or equalfor all x:A (x in B)
      |A|The cardinallity or size of A.
      {}empty set
      {a,b,c,...}"extension", set of elements a, b, c, ...
      {x:T || P}, $[x:T](P), set(x:T. P)The set of x's of type T satisfying P
      @BSubsets of B{ A || A ==> B }
      B@nSubsets of a given size{ A: @B || |A| = n }
      A | BUnion{ x:T. x in A or x in B }
      Union={a:T||for some A:α(a in A)}
      A & BIntersection{ x:T. x in A and x in B }
      &(α)Intersection{a:T||for all A:α( a in A )}
      A are BA ==>B
      A=>>BA==>B and not A=B.
      A>=={X1, X2,... }Partition
      A><BCartesian Product{ (a,b)|| a:A, b:B}
      (x1, x2, x3, ... xn)n-tuple/list/string
      X1><X2><X3...><Xnset of n-tuples
      For Q:quantifiers, Q Afor Q x:T (x in A)
      some AA is not empty A <> {}.
      no AA is empty A = {}.
      1 AA = { the A }

      (Close Table)
      [ Set Expressions in logic_30_Sets ]

      Large and complex sets can be defined by using special formats including tables, mappings, and "long sets":

       		One element per line


      For types T1,T2, @(T1,T2) is the type of relationships between T1 and T2.

      We use R, S: @(T1,T2) as typical relations with A:@T1 and B:@T2:
      dom(R), cod(R)dom(R)=T1 and cod(R)=T2.
      R=rel [x:T1,y:T2]( x R y)
      x R y=(x,y).R=R(x,y)=(x,y)in R
      R(as a set)={ (x,y) || x R y}
      x.R, R(x)= { y || x R y }
      y./R, /R(y)= { x || x R y }
      A.R, R(A)= { y || some a:A ( a R y) }
      B./R, /R(B)= { x || some b:B ( x R b) }
      post(R)=rng(R)=img(R)=dom(R).R = |(R)
      pre(R)=cor(R)=cod(R)./R = |(/R)
      R | S=rel[x:T1,y:T3] (x R y or x S y), relational union
      R & S=rel[x:T1,y:T3] (x R y and x S y), relational intersection
      R; S=rel[x:T1,y:T3] for some z(x R z and z S y) , relational product
      A; R=rel[x:T1,y:T3] (x in A and x R y) , left limit
      R; A=rel[x:T1,y:T3] (x R y and y in B) , right limit
      inv(R)={ Q:@dom(R) || all Q.R ==> Q}, the invariant sets of R:@(T1,T1).
      do R=rel[x,y:dom(R)](for all Q:inv(R) (if x in Q then y in Q}), transitive etc closure
      no(R)=rel[x,y:dom(R)](x=y and 0 x.R)
      Id(U)=rel[x,y:dom(R)](x=y )
      R is nondeterministic=for some x:dom(R), 2.. y:cod(R) ( x R y )
      U(Q1)-(Q2)V= {R || for all x:U, Q2 y (x R y) & all y:V, Q1 x (x R y) }
      many-1= (any)-(0..1)

      (Close Table)
      The above are for relationships that link or pair up objects in pairs. There are also n-ary relations but they do not have such a rich set of notations.

      Notice the programming language-like notation for relations because do is borrowed from FORTRAN, PL/1 and Algol 68:

    1. do(x<10; x'=x+1; y'=y*x); no(x<10)

      is equivalent to the shorter

    2. while(x<10)(x:+1; y:*x)

      Long or complicated relations are often expressed as table

       	.Row One tuple per Row, Items separated by tabs or
       	.Item in a special item line
      Or in an alternate format is used by W Ross Ashby for funactions and maps:
       	.Row Items in domain
       	.Row Items in codomain


      A function or mapping is a many-1 relation between two types.

      For T1, T2: Types, T2^T1 is the type of functions mapping T1 to T2.

      For A:@T1, B:@T2,
      A -> B= A >-> B = A (any)-(1)B ==> T2^T1.
      map [x:A](e)The map taking x into e (e an expression of type T2)
      fun [x:A](e)The function taking x into e, λ[x:A](e).
      x+>y{(x,y)} maplet, the map taking x to y.
      A+>y{(x,y)||for some x:A}
      f(x), x.f=the f of x= the image of x under f
      f is one-oneiff f in dom(f)(1)-(1)cod(f)

      (Close Table)
      For example:

    3. (1+>2)(1) = 2 = 1.(1+>2).
    4. (1+>2) = map[x:{1}](2).
    5. (0+>1 | 1+>0) = complement function = fun[i:Bits](1-i). Long or complicated functions and maps are often expressed as table
       	.Row One pair per Row, Items separated by tabs or
       	.Item in a special item line

      Lists and Strings

      For any type T, %T and #T represent the type of lists and strings of elements of that type respectively,
      ()empty list/string
      (x,y,z)list with three elements, 1st, 2nd, and 3rd.
      z=x?yiff x is the first(z) and y rest(z).
      #XAny number of X's, Semigroup generated from X by (!)
      z = x! yiff z is the concatenation of x and y.

      (Close Table)
      Long list can be encoded in a long form
       		One paragraph or formula per item

      Sets of Sequences

      For any type T, @#T is the set of languages based on alphabet T
      A B{ z || for some a:A, b:B ( z =a!b ) }
      A^n= if n=0 then 1 else A A^(n-1)
      #A= {()}| A | A A | A A A | ...
      #A=|[i:0..]A^i = min{ B || (A B | ())==>B}
      #A= {()}.do fun[X:Sets] (X A}

      (Close Table)


      For any sets X,Y,... and identifiers x,y, $ Net{x:X, y:Y, ...} is a set of labelled tuples or record structures.
      $ Net{x:X, y:Y, ...}{ (x=>a, y=>b,...) || a in X and b in Y and ...}
      xmaps $ Net{...., x:X, ....} into an X.
      variables(U){x,y,z,...}, the names of parts/variables

      (Close Table)
      These structures are the MATHS equivalent of classes. objects and tuples. Sets of structured objects/tuples act very like data bases and can be described by using a table:
       	.Table Attribute	Attribute	Attribute	...
       	.Row List of attribute values separated by tabs

      Documentation Nets

      Warning: This area is undergoing remodelling and renovation A network of comments, declarations, defintions, assumptions etc is shown betwenn braces like this Net{...} or like this
      In theory all documentation represents a schema or binding
       [ List_of(declaration | constraints) ].
      and such bindings can be used in several ways:
       Derivation/Inheritance/subtyping:	Base with [Extension]
       Parts of expressions:	name[binding](expression).

    6. For string D where Net{D} in documentation,
      $ Net{D}The type of objects described by D,
      $ Net{D, W(v)} set v:$ Net{D} satisfying W(v),
      $ Net{D, W(v',v)} relation v,v':$ Net{D} satisfying W(v',v).

      (Close Table)

      Documentation is often named via a definition:

       	Name ::= Net{....}.
       	Name ::=following,
      or remotely

    7. For Name_of_documentation N,
      a(N)tpl of variables in N,
      $(N)an(N), a(N),
      $ Nset of $(N) that fit the N,
      set N$ N,
      the N(P)the($ N and P)the unique $ N that also fits P,
      @Ncollection of sets of objects satisfying N,
      #Nstrings of objects that fit N,
      %NLISP-like lists of objects that fit N,
      |-NAsserts a copy of N in current document.
      Uses NInserts a copy of N's definition into current document.
      With NInserts a copy of what N is defined to be into current document.
      By NDerivation of theorem from axioms in N
      for Q N(wff)for Q x:$ N (wff where x=$(N)),
      @{N || for Q1 v1, ...}Set of sets of @N satisfying the Qs,
      N(x=>a, y=>b,...)substitute in N,
      N(for some x,...)hide x.. in N,
      N.(x,y,z,...)hide all but x,y,z,...`.

      (Close Table)
    8. For N1, N2:Name_of_documentation|set_of_documentation, Q1, Q2, ...:Quantifiers
      not N1complementary documentation to N1,
      N1 o N2combine pieces of documentation,
      N1 and wNet{D. w } where N is the name of {D},
      N1 with{D2}Net{D. D2 } where N is the name of {D},
      N1->N2Sets in @(N1 and N2) with N1 as an identifier,
      N1^N2functions from type $ N2 to type $ N1,
      N1(Q1)-(Q2)N1Relations between N1 and N2.

      (Close Table)



    9. (above)|-For f:X->Y, A1,A2:@X, B1,B2:@Y, following,
      1. f({})={}
      2. and /f({})={}
      3. and for all x:X( x in A iff f(x) in f(A)
      4. and for all x:X( f(x) in A iff x in /f(A) )
      5. and (if A1 ==> A2 then f(A1) ==> f(A2))
      6. and (if B1 ==> B2 then /f(B1) ==> /f(B2))
      7. and f(A1 | A2) = f(A1) | f(A2)
      8. and /f(B1 | B2) = /f(B1) | /f(B2)
      9. and f(A1 & A2)==>f(A1) & f(A2)
      10. and /f(B1 & B2) = /f(B1) & /f(B2)
      11. and f(A1~A2)<==f(A1)~f(A2)
      12. and /f(B1~B2)= /f(B1)~/f(B2).

    10. ()|-For f:X->Y,
      1. f o /f ==> Id ==> /f o f
      2. and (f o /f = Id iff f:X>--Y)
      3. and (/f o f = Id iff f:X->Y)
      4. and (f o /f = Id = /f o f iff f:X---Y)

    11. (above)|-For X,Y:Sets, f:X>--Y, P:Y->@, for all x:X (P(f(x)) iff for all y:Y(P(y)).

      unary operations

      Unary operations are like functions in most respect but form an algebra.
    12. For X:Set, unary(X) =X^X.
    13. For X:Set, f:unary(X), x:X,
      fix(f)@X{ x:X || f(x)=x }.
      f @X->@X fun A:@X {f(a) || a:A},
      f #X->#X fun a:#X (fun i:1..|a| (f(a[i])),
      fX^A->X^A fun g:X^A ( fun [a:A] (f(g(a))),

      (Close Table)
    14. square((1,2,3)) = (1,4,9).
    15. square({1,2,3}) = {1,4,9}.

      infix operations

      For *:infix(X), x,y:X.
      infix(X) X^( X><X )
      associative(X){* || for all x,y,z:X(x*(y*z)=(x*y)*z)},
      commutative(X){* || for all x,y:X (x*y = y*x)},
      idempotent(X){* || for all x:X (x*x = x)}.
      units(X,*){u:X || x * u = u * x = x},
      zeroes(X,*){z:X || for all x:X( z*x = x*z= z},
      idempotents(X,*){i:X || i * i = i},

      (Close Table)

    16. (above)|-(x*y) = (*)(x,y) = (x,y).(*). (above) |-For *:infix(X), x:X, (x*_) ::= fun y:X(x*y), (_*x) ::= fun y:X(y*x),
    17. (above)|-For *:infix(X), x:X, y:X, (x*_)(y)=y.(x*_)=(_*y)(x)=x.(_*y)=x*y in X,


    18. For *:infix(X), x,y:variable(X), e:expression(X),
      x:*e (x' = x * e ),
      e*:y (e * y = y')

      (Close Table)


    19. For *:infix(X), Y:=@X, Z:=X^A,
      * Y><Y->Yfun [A,B] {a*b || a:A, b:B},
      * X><Y->Yfun [x,B] {x*b || b:B},
      * Y><X->(@X)fun [A,x] {a*x || a:A},
      * Z><Z->Zfun [f,g](fun a:A (f(a)*g(a) ) ),
      * X><Z->Zfun [x,f] (fun a:A (x* f(a) ) ),
      * Z><X->Zfun [f,x] (fun a:A (f(a) * x) ).

      (Close Table)

      SERIAL operations

    20. Some call x:X^A a family, and define (x[i] || i:A) ::=[i:A]x[i].
    21. For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets, f:X^A,
      +f in X,
      if | A|=0 then +f=0,
      if |A|=1 then for some y:A(+f=f(y)),
      if |A|>1 then for all Y:@A( +f=+(f o Y) + +(f o (A~Y)).

      (Close Table)
    22. for p:A---A, +(f o p)=+f.
    23. For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X), e:expression(Type(X)) +[x:A](e) ::= +(fun[x:A](e)).
    24. (above)|-For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X),
      +A in X
      if|A|=0 then +A=0,
      if |A|=1 then +A=the (A),
      if |A|>1 then for all Y:@A(+(A&Y) + +(A~Y))}.
      for p:A---A, +p(A)=+(A).

      (Close Table)


    25. |-For X:Sets, Y:=@(X,X), R:Y, n,m:Nat0, N:=n..m, S:N->X, R(S)=for all i:N~{m} (S(i) R S(i+1)) For X:Sets, I:=Id(X), 0:Y:={},
      Transitive(X){R:Y || R;R ==> R },
      Reflexive(X){R:Y || R = /R },
      Irreflexive(X){R:Y || 0 = I & /R },
      Antireflexive(X){R:Y || 0 = R & /R },
      Dichotomettic(X){R:Y || Y >== {R, /R }},
      Trichotomettic(X){R:Y || Y >== {R, /R, I}},
      Symmetric(X){R:Y || R = /R },
      Antisymmetric(X){R:Y || R & /R = I},
      Asymmetric(X){R:Y || R ==> Y~/R },
      Total(X){R:Y || Y~R = /R },
      Connected(X){R || Y~R= /R and R | /R = Y},
      Regular(X){R:Y || R; /R; R ==> R },
      Right_limited(X){R:Y || for no S:Nat-->X (R(S) ) },
      Left_limited(X){R:Y || for no S:Nat-->X ( /R(S) ) },
      Serial(X)(Transitive(X)&Connected(X))~Reflexive( X),
      Strict_partial_order(X)Irreflexive(X) & Transitive(X),
      Partial_order(X)Reflexive(X) & Transitive(X) & Antisymmetric(X),
      Equivalences(X)Reflexive(X) & Symmetric(X) & Transitive(X).
      Irreflexive(X) & Transitive(X)= Asymmetric(X) & Transitive(X).

      (Close Table)
    26. For X,Y: Sets, R,S: @(X,Y),
      R is_more_defined_than Spre(S)==>pre(R) and for all x:pre(S) (x.R==>x.S).

      (Close Table)
      [Mili et al. 89]

      Standard Types

      Generic: Alphabets, Any, Sets, Finite_sets of a given type, Types.
      Specific: @, Char, Documentation, Events, Numbers, Times
      Ranges n..m, n.., ..m, [x..y], (x..y), (x..y], [x..y)
      Subsets of Numbers: Int, Rational, Real, Fixed(n), Float(p,s), Decimal(n, p), Money.
      Nat0{0}|Natural = 0..,

      (Close Table)


      Proofs are made up of steps like this
       	(givens) |- (name): derive
      where the name can be used in later steps as a given.

      Standard valid derivations
      P and QP
      P and QQ
      not(P and Q)not P or not Q
      P,QP and Q
      P or Q, not PQ
      P or Q, not QP
      not(P or Q)not P
      not(P or Q)not Q
      P, if P then QQ
      not Q, if P then Qnot P
      not(if P then Q)P, not Q
      P iff Qif P then Q
      P iff Qif Q then P
      e1=e2, W(e1)W(e2)
      not for some x:T(W(x))for all x:T(not W(x))
      not for all x:T(W(x))for some x:T(not W(x))
      for some x:T(not W(x))not for all x:T( W(x))
      for all x:T(not W(x))not for all x:T( W(x))

      (Close Table)

      W(e)(x=>e)for some x:T(W(x))e is an expression of type T
      for some x:T (W(x))(x=>v) v:T, W(v) v must be a free variable
      for 1 x:T(W(x))(v=the x) W(v)v must be a free variable
      for all x:T(W(x))(x=>e) W(e)e can be any expression of type T

      (Close Table)
      Standard ways to prove conclusions
      for x:T, if P then Q.Let{ x:T,|-P. ...|-Q }
      P or Q.Let{ not P. ...|-Q }
      for one x:T (W2(x))Let{x1,x2:T,|-W(x1) and W(x2).... |-x1=x2 }

      (Close Table)

      GivenLet{Case1|-Conclusion}Else Let{Case2...|-Conclusion}|-Conclusion
      P or QPQ
      if P then Qnot PQ
      P iff QP,Qnot P, not Q
      not(P iff Q)P,not Qnot P,Q

      (Close Table)

    27. Reductio ad Absurdum
      ConclusionsLet{|-hypothesis....|-(lab):R. ...|- not R, (lab)}|-RAbs
      if P then QP,not Q
      P or Qnot P,not Q
      Pnot P
      for all x:T(W(x))x:T, not W(x)
      for some x:T(W(x))for all x:T(not W(x))

      (Close Table)
      Notice that when an proof becomes long the following is used
       |- Hypothesis
       (reasons) |- theorem

      In informal documents, you can also put a rebuttal for a statement or an argument:



      These a functions used to talk about documentation, rather than used in everyday documentation of applications and systems.
    28. symbol:@( Strings, Types, Values)
    29. For s: documentation | name_of_documentation,
      terms(s)Setsterms defined in s,
      expressions(s)Setsexpressions used to define terms in s,
      definitions(s)@(terms(s), types(s), expressions(s))definitions in s,
      declarations(s)@(variables(s), types(s))declared and defined types of variables in s,

      (Close Table)
    30. For s: documentation | name_of_documentation,
      types(s)types in declarations and definitions in s,
      variables(s)symbols bound in declarations in s,
      axioms(s)wffs assumed to be true | defined equalities,
      theorems(s)wffs proved to be true,
      assertions(s)(axioms(s) | theorems(s))

      (Close Table)


      To Be announced

    . . . . . . . . . ( end of section A "Cheat Sheat" Of Standard MATHS Notation) <<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


  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 of document ) <<Contents | Top