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

# A "Cheat Sheat" Of Standard MATHS Notation

## Purpose

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.

## Logic

Table
SymbolTypeMeaning
@Types={true,false}
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
Table
FormulaMeaning
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 ]

## Sets

For Type T
Table
SymbolsMeaningDefinition
@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":

` 	.Set`
` 		One element per line`
` 	.Close.Set`

## Relations

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:
Table
FormulaMeaning
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 )
abort=T1><T2
fail=rel[x,y:T1](false)
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) }
total=(any)-(some)
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

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

## Maps/Functions

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,
Table
FormulaMeaning
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
` 	.Table`
` 	.Row One pair per Row, Items separated by tabs or`
` 	.Item in a special item line`
` 	.Close.Table`

## Lists and Strings

For any type T, %T and #T represent the type of lists and strings of elements of that type respectively,
Table
SymbolMeaning
()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
` 	.List`
` 		One paragraph or formula per item`
` 	.Close.List`

## Sets of Sequences

For any type T, @#T is the set of languages based on alphabet T
Table
SymbolMeaning
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)

## Structures

For any sets X,Y,... and identifiers x,y, \$ Net{x:X, y:Y, ...} is a set of labelled tuples or record structures.
Table
SymbolMeaning
\$ 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`
` 	.Close.Table`

## 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
` .Net`
` ...`
` .Close.Net`
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,
Table
\$ 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{....}.`
or
` 	Name ::=following,`
` .Net`
` 	...`
` .Close.Net`
or remotely
` 	Name::=URL.`

7. For Name_of_documentation N,
Table
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
Table
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)

## Maps_and_Sets

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,
Table
SymbolContextMeaning
fix(f)@X{ x:X || f(x)=x }.
f(x)Xx.f
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)
Examples:
14. square((1,2,3)) = (1,4,9).
15. square({1,2,3}) = {1,4,9}.

## infix operations

For *:infix(X), x,y:X.
Table
SymbolMeaning
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,

## Dynamics

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

(Close Table)

19. For *:infix(X), Y:=@X, Z:=X^A,
Table
SymbolContextMeaning
* 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,
Table
+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),
Table
+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)

## Relations

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:={},
Table
SymbolMeaning
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),
Table
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

Table
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.
Nat1..
Posititive1..
Bit0..1
Nat0{0}|Natural = 0..,

(Close Table)

## Proofs

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
Table
Given|-Derive
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)

Table
GivenAnnotationDeriveCondition
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
Table
Conclusion.Let{hypothesis...|-closure}
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)

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)

Table
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
` .Let`
` |- Hypothesis`
` ...`
` (reasons) |- theorem`
` ...`
` .Close.Let`

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

` .But`
`  ...`
` .Close.But`

## Meta-Functions

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,
Table
SymbolTypeMeaning
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,
Table
FormulaMeaning
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)

## Layout

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

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