.Open 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 Symbol	Type	Meaning
.Row @	Types	={true,false}
.Row and, or, not	infix(@)	Boolean operators
.Row if P then Q	@	implication, true iff P false or Q true.
.Row if P then Q else R	@	= (if P then Q)and(if not P then Q) = (P and Q)or(not P and R).
.Row iff	infix(@)	If and only if 
.Close.Table
.See http://www.csci.csusb.edu/dick/maths/logic_10_PC_LPC.html#PROPOSITIONS

Quantifiers include: all, some, 0,1, 2,3,..., n, . 0..1, 0..2, .... n..m
.Table Formula	Meaning
.Row for all x:A (P)	For all x in A, P is true
.Row for some x:A (P)	For some x in A  P is true
.Row for 0 x:A (P)	= not for some x:A(P), for no x in A is P true
.Row for 1 x:A (P)	For exactly one x in A, P is true
.Row for n x:A (P )	For exactly n x...
.Row for 0..1 x:A (P)	for 0 x:A (P) or for 1 x:A (P)
.Row for n..m  x:A (P)	Between n and m x's in A satisfy P
.Row for any  x:T (P )	Any number including none. 
.Row for abf  x:T (P )	for all but a finite number
.Row for Q1 x1:T1, Q2 x2:T2... (P )	You can put many quantifiers after one `for`.
.Row for Q T x (P )	If the type is a name you can out it first.
.Row the x:A (P)	The unique x in A satisfying P (or else undefined)
.Row x = y	True if x and y are defined and equal, else false.
.Row x <> y	Negation of x=y, Pascal and BASIC notation.
.Row x != y	Negation of x=y, The C/C++/Java/PHP/ ... notation
.Close.Table
.See http://www.csci.csusb.edu/dick/maths/logic_10_PC_LPC.html#Lower_Predicate_Calculus_with_equality
. Sets 
For Type T
.Table Symbols	Meaning
.Row @T	Type whose elements a sets of objects of type T
.Row x in A	x is a member of A
.Row A ==>B	iff for all x:A (x in  B), subseteq
.Row |A|	The cardinallity or size of A.
.Row {}	empty set
.Row {a,b,c,...}	"extension", set of elements a, b, c, ...
.Row {x:T || P}, $[x:T](P), set(x:T. P)	The set of x's of type T satisfying P
.Row @B	Subsets of B	{  A ||  A ==>  B }
.Row B@n	Subsets of a given size	{  A: @B || |A| = n }
.Row A | B	Union { x:T. x in A or x in B }
.Row |\alpha	={a:T||for some A:\alpha(a in A)}
.Row A & B	Intersection { x:T. x in A and x in B }
.Row &(\alpha)	={a:T||for all A:\alpha( a in A )}
.Row A are B	A ==>B
.Row A=>>B	A==>B and not A=B.
.Row A>=={X1, X2,... }	Partition
.Row A><B	Cartesian Products, { (a,b)||  a:A, b:B}
.Row (x1, x2, x3, ...    xn)	n-tuple/list/string
.Row X1><X2><X3...><Xn	set of n-tuples
.Row  For Q:quantifiers, Q A	for Q x:T (x in A)
.Row  some A	A is not empty, A <> {}.
.Row  no A	A is empty, A = {}.
.Row  1 A	A = { the A }
.Close.Table
.See http://www.csci.csusb.edu/dick/maths/logic_30_Sets.html#Set Expressions

Large and complex sets can be defined by using special formats including
tables, mappings, and "long sets":
.As_is 	.Set
.As_is 		One element per line
.As_is 	.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 Formula	Meaning
.Row  dom(R), cod(R)	dom(R)=T1 and cod(R)=T2.
.Row  R	=rel [x:T1,y:T2]( x R y)
.Row  x R y	=(x,y).R=R(x,y)=(x,y)in R
.Row   R(as a set)	={ (x,y) || x R y}
.Row  x.R, R(x)	= {  y ||  x R y  } 
.Row  y./R, /R(y)	= {  x ||  x R y  } 
.Row A.R, R(A)	= {  y ||  some a:A ( a R y) } 
.Row B./R, /R(B)	= {  x ||  some b:B ( x R b) } 
.Row post(R)	=rng(R)=img(R)=dom(R).R = |(R)
.Row pre(R)	=cor(R)=cod(R)./R = |(/R)
.Row R; S	=rel[x:T1,y:T3] for some z(x R z and z S y) 
.Row R | S	=rel[x:T1,y:T3] (x R y or x S y)
.Row inv(R)	={ Q:@dom(R) || all Q.R ==> Q}, the invariant sets of R:@(T1,T1).
.Row do R	=rel[x,y:dom(R)](for all Q:inv(R) (if x in Q then y in Q})
.Row no(R)	=rel[x,y:dom(R)](x=y and 0 x.R)
.Row Id(U)	=rel[x,y:dom(R)](x=y )
.Row abort	=T1><T2
.Row fail	=rel[x,y:T1](false)
.Row R is nondeterministic	=for some x:dom(R), 2.. y:cod(R) ( x R y )
.Row U(Q1)-(Q2)V	= {R || for all x:U, Q2 y (x R y) & all  y:V, Q1 x (x R y) }
.Row  total	=(any)-(some)
.Row  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:
 do(x<10; x'=x+1; y'=y*x); no(x>=10)

Long or complicated relations are often expressed as table
.As_is 	.Table
.As_is 	.Row One tuple per Row, Items separated by tabs or
.As_is 	.Item in a special item line
.As_is 	.Close.Table
Or in an alternate (W Ross Ashby) format
.As_is 	.Table
.As_is 	.Row Items in domain
.As_is 	.Row Items in codomain
.As_is 	.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 Formula	Meaning
.Row  A -> B	= A >-> B = A (any)-(1)B ==> T2^T1.
.Row  map [x:A](e)	The map taking  x into e (e an expression of type T2)
.Row  fun [x:A](e)	The function taking  x into e, \lambda[x:A](e).
.Row x+>y	{(x,y)} `maplet`, the map taking x to y.
.Row A+>y	{(x,y)||for some x:A}
.Row f(x), x.f	=the f of x= the image of x under f
.Row  f is one-one	iff  f in dom(f)(1)-(1)cod(f)
.Close.Table
For example:
	(1+>2)(1) = 2 = 1.(1+>2).
	(1+>2) = map[x:{1}](2).
	(0+>1 | 1+>0) =` complement function` = fun[i:Bits](1-i).
Long or complicated functions and maps are often expressed as table
.As_is 	.Table
.As_is 	.Row One pair per Row, Items separated by tabs or
.As_is 	.Item in a special item line
.As_is 	.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 Symbol	Meaning
.Row ()	empty list/string
.Row z=x?y	iff  x is the first(z) and y  rest(z).
.Row #X	Any number of X's, Semigroup generated from X by (!)
.Row z = x! y	iff z is the  concatenation of x and y.
.Close.Table
. Sets of Sequences
For any type T, @#T is the set of languages based on alphabet T
.Table Symbol	Meaning
.Row A B	{ z || for some a:A, b:B ( z =a!b ) }
.Row A^n	= if n=0 then 1 else A A^(n-1)
.Row #A	=  {()}| A | A A | A A A | ...
.Row #A	=|[i:0..]A^i = min{ B || (A B | ())==>B} 
.Row #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 Symbol	Meaning
.Row $ Net{x:X, y:Y, ...}	{ (x=>a, y=>b,...) || a in X and b in Y and  ...}       
.Row x	maps $ Net{...., x:X, ....} into an X.
.Row 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:
.As_is 	.Table Attribute	Attribute	Attribute	...
.As_is 	.Row List of attribute values separated by tabs
.As_is 	.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
.As_is .Net
.As_is ...
.As_is .Close.Net
In theory all documentation represents a schema or binding
.As_is [ List_of(declaration | constraints) ].
and such bindings can be used in several ways:
.As_is Derivation/Inheritance/subtyping:	Base with [Extension]
.As_is Parts of expressions:	name[binding](expression).

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

Documentation is often named via a definition:
.As_is 	Name ::= Net{....}.
or
.As_is 	Name ::=following,
.As_is .Net
.As_is 	...
.As_is .Close.Net
or remotely
.As_is 	Name::=URL.

 For Name_of_documentation  N,
.Table
.Row a(N)	`tpl of variables in N`,
.Row $(N)	an(N), a(N),
.Row $ N	`set of $(N) that fit the N`,
.Row set N	$ N,
.Row the N(P)	the($ $N and P)	`the unique $ $N that also fits P`,
.Row @N	`collection of sets of objects satisfying N`,
.Row #N	`strings of objects that fit N`,
.Row %N	`LISP-like lists of objects that fit N`,
.Row |- N	`Asserts a copy of N in current document`.
.Row Uses N	`Inserts a copy of N's definition into current document`.
.Row With N	`Inserts a copy of what N is defined to be into current document`.
.Row By N	`Derivation of  theorem from axioms in N`
.Row for Q N(wff)	for Q x:$ N (wff where x=$(N)),
.Row @{N || for Q1 v1,  ...}	`Set of sets of @N satisfying the Qs`,
.Row N(x=>a, y=>b,...)	`substitute in N`,
.Row N(for some x,...)	`hide x.. in N`,
.Row N.(x,y,z,...)	hide all but x,y,z,...`.
.Close.Table
 For N1, N2:Name_of_documentation|set_of_documentation, Q1, Q2, ...:Quantifiers
.Table
.Row not N1	`complementary documentation to N1`,
.Row N1 o N2	`combine pieces of documentation`,
.Row N1 and w	`Net{D. w } where N is the name of {D}`,
.Row N1 with{D2}	`Net{D. D2 } where N is the name of {D}`,
.Row N1->N2	`Sets in @(N1 and N2) with N1 as an identifier`,
.Row N1^N2	`functions from type $ $N2 to type $ N1`,
.Row N1(Q1)-(Q2)N1	Relations between N1 and N2.
.Close.Table
. RESULTS and SYSTEMS
. Maps_and_Sets
()|- For f:X->Y, A1,A2:@X, B1,B2:@Y, following,
.List
 f({})={}
 and /f({})={}
 and for all x:X( x in A iff f(x) in f(A) 
 and for all x:X( f(x) in A iff x in /f(A) )
 and (if A1 ==> A2 then f(A1) ==> f(A2))
 and (if B1 ==> B2 then /f(B1) ==> /f(B2))
 and f(A1 | A2) = f(A1) | f(A2) 
 and /f(B1 | B2) = /f(B1) | /f(B2)
 and f(A1 & A2)==>f(A1) & f(A2) 
 and /f(B1 & B2) = /f(B1) & /f(B2)
 and f(A1~A2)<==f(A1)~f(A2) 
 and /f(B1~B2)= /f(B1)~/f(B2).
.Close.List

() |- For f:X->Y,
.List
 f o /f ==> Id ==> /f o f
 and (f o /f = Id iff f:X>--Y)
 and (/f o f = Id iff f:X->Y)
 and (f o /f = Id = /f o f iff f:X---Y)
.Close.List

()|- 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.
 For X:Set, unary(X) =X^X.
 For X:Set, f:unary(X), x:X,
.Table Symbol	Context	Meaning
.Row fix(f)	@X	{ x:X || f(x)=x }.
.Row f(x)	X	x.f 
.Row f	 @X->@X  	  fun A:@X {f(a) || a:A},
.Row f	 #X->#X  	  fun a:#X (fun i:1..|a| (f(a[i])),
.Row f	X^A->X^A  	 fun g:X^A ( fun [a:A] (f(g(a))),
.Close.Table
Examples:
	square((1,2,3)) = (1,4,9).
	square({1,2,3}) = {1,4,9}.
. infix operations
.Table Symbol	Meaning
.Row infix(X)	 X^( X><X ), For *:infix(X), x,y:X.
.Row associative(X)	{* || for all x,y,z:X(x*(y*z)=(x*y)*z)},
.Row commutative(X)	{* || for all x,y:X  (x*y   =  y*x)},
.Row idempotent(X)	{* || for all   x:X  (x*x = x)}.
.Row units(X,*)	{u:X || x * u  =  u * x  =  x},
.Row zeroes(X,*)	{z:X || for all x:X( z*x = x*z= z},
.Row idempotents(X,*)	{i:X || i * i = i},
.Close.Table
 ()|-(x*y) = (*)(x,y) = (x,y).(*).
()|-For *:infix(X), x:X, (x*_) ::= fun y:X(x*y),
 (_*x) ::= fun y:X(y*x),
 ()|- For *:infix(X), x:X, y:X, (x*_)(y)=y.(x*_)=(_*y)(x)=x.(_*y)=x*y in X,
. Dynamics
 For *:infix(X), x,y:variable(X), e:expression(X),
.Table Symbol	Meaning
.Row x:*e	 (x' = x * e ),
.Row e*:y	 (e * y = y')
.Close.Table
. Overloadings
 For *:infix(X), Y:=@X, Z:=X^A,
.Table Symbol	Context	Meaning
.Row *	 Y><Y->Y	fun [A,B] {a*b || a:A, b:B},
.Row *	 X><Y->Y	fun [x,B] {x*b || b:B},
.Row *	 Y><X->(@X)	fun [A,x] {a*x || a:A},
.Row *	 Z><Z->Z	fun [f,g](fun a:A (f(a)*g(a) ) ),
.Row *	 X><Z->Z	fun [x,f] (fun a:A (x* f(a) ) ),
.Row *	 Z><X->Z	fun [f,x] (fun a:A  (f(a) * x) ).
.Close.Table
. SERIAL operations   
 Some call x:X^A a family, and define
	 (x[i] ||  i:A) ::=[i:A]x[i].
 For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets, f:X^A,
.Table
.Row +f in X,
.Row if  | A|=0 then +f=0,
.Row if |A|=1 then for some y:A(+f=f(y)),
.Row if |A|>1 then for all Y:@A( +f=+(f o Y) + +(f o (A~Y)).
.Close.Table
 for p:A---A, +(f o p)=+f.
 For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X), e:expression(Type(X)) +[x:A](e) ::= +(fun[x:A](e)).
 ()|-For +:associative(X) & commutative(X), 0:units(X,+), A:FiniteSets(X),
.Table
.Row +A in X
.Row if|A|=0 then +A=0,
.Row if |A|=1 then +A=the (A),
.Row if |A|>1 then for all Y:@A(+(A&Y) + +(A~Y))}.
.Row for p:A---A, +p(A)=+(A).
.Close.Table
. Relations
|-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 Symbol	Meaning
.Row Transitive(X)	{R:Y || R;R ==> R },
.Row Reflexive(X)	{R:Y || R = /R },
.Row Irreflexive(X)	{R:Y || 0 = I & /R },
.Row Antireflexive(X)	{R:Y || 0 = R & /R },
.Row Dichotomettic(X)	{R:Y || Y >== {R, /R }},
.Row Trichotomettic(X)	{R:Y || Y >== {R, /R, I}},
.Row Symmetric(X)	{R:Y || R = /R },
.Row Antisymmetric(X)	{R:Y || R & /R = I},
.Row Asymmetric(X)	{R:Y || R ==> Y~/R },
.Row Total(X)	{R:Y || Y~R = /R },
.Row Connected(X)	{R || Y~R= /R  and R | /R = Y},
.Row Regular(X)	{R:Y || R; /R; R ==> R },
.Row Right_limited(X)	{R:Y || for no S:Nat-->X (R(S) ) },
.Row Left_limited(X)	{R:Y || for no S:Nat-->X ( /R(S) ) },
.Row Serial(X)	(Transitive(X)&Connected(X))~Reflexive( X),
.Row Strict_partial_order(X)	Irreflexive(X) & Transitive(X),
.Row Partial_order(X)	Reflexive(X) & Transitive(X) & Antisymmetric(X),
.Row Equivalences(X)	Reflexive(X) & Symmetric(X) &  Transitive(X).
.Row Irreflexive(X) & Transitive(X)	= Asymmetric(X) & Transitive(X).
.Close.Table
 For X,Y: Sets, R,S: @(X,Y),
.Table
.Row R is_more_defined_than S	pre(S)==>pre(R) and for all x:pre(S) (x.R==>x.S).
.Close.Table
.See [Mili et al. 89]
. Standard Types
.Table
.Row Generic: 
.Item Alphabets, Any, Sets, Finite_sets, Types.
.Row Specific: 
.Item @, Char, Documentation,  Events,  Numbers, Times
.Row Ranges
.Item `n`..`m`, `n`.., ..`m`, [`x`..`y`], (`x`..`y`), (`x`..`y`], [`x`..`y`)
.Row Subsets of Numbers:
.Item Int, Rational, Real, Fixed(n),  Float(p,s), Decimal(n, p), Money.
.Row Nat	1..
.Row Posititive	1..
.Row Bit	0..1
.Row Nat0	{0}|Natural = 0..,
.Close.Table
. Proofs
Proofs are made up of steps like this
.As_is 	(givens) |- (name): derive
where the `name` can be used in later steps as a `given`.

Standard valid derivations
.Table Given	|- Derive
.Row P and Q	P
.Row P and Q	Q
.Row not(P and Q)	not P or not Q
.Row P,Q	P and Q
.Row P or Q, not P	Q
.Row P or Q, not Q	P
.Row not(P or Q)	not P
.Row not(P or Q)	not Q
.Row P, if P then Q	Q
.Row not Q, if P then Q	not P
.Row not(if P then Q)	P, not Q
.Row P iff Q	if P then Q
.Row P iff Q	if Q then P
.Row e1=e2, W(e1)	W(e2)
.Row not for some x:T(W(x))	for all x:T(not W(x))
.Row not for all x:T(W(x))	for some x:T(not W(x))
.Row for some x:T(not W(x))	not for all x:T( W(x))
.Row for all x:T(not W(x))	not for all x:T( W(x))
.Close.Table
.Table Given	Annotation	Derive	Condition
.Row W(e)	(x=>e)	for some x:T(W(x))   e is an expression of type T
.Row for some x:T  (W(x))	(x=>v)	 v:T, W(v)  v must be a free variable
.Row for 1 x:T(W(x))	(v=the x) 	 W(v)	v must be a free variable
.Row 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}
.Row for x:T, if P then Q.	Let{ x:T,|-P. ...	|-Q }
.Row P or Q.	Let{ not P. ...	|- Q }
.Row for one  x:T (W2(x))	Let{x1,x2:T, |-W(x1) and W(x2)....
.Item |- x1=x2 }
.Close.Table
.Table Given	Let{Case1|-Conclusion}	Else Let{Case2...|-Conclusion}|-Conclusion
.Row P or Q	P	Q
.Row if P then Q	not P	Q
.Row P iff Q	P,Q	not P, not Q
.Row not(P iff Q)	P,not Q	not P,Q
.Close.Table
 Reductio ad Absurdum
.Table Conclusions	Let{|-hypothesis....|-(lab):R. ...|- not R, (lab)}|-RAbs
.Row if P then Q	P,not Q
.Row P or Q	not P,not Q
.Row P	not P
.Row for all x:T(W(x))	x:T, not W(x)
.Row 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
.As_is .Let 
.As_is |- Hypothesis
.As_is ...
.As_is (reasons) |- theorem
.As_is ...
.As_is .Close.Let

. Meta-Functions
These a functions used to talk about documentation, rather than used
in everyday documentation of applications and systems.
 symbol:@( Strings, Types, Values)
 For s: documentation | name_of_documentation,
.Table Symbol	Type	Meaning
.Row terms(s)	Sets	`terms defined in s`,
.Row expressions(s)	Sets	`expressions used to define terms in s`,
.Row definitions(s)	@(terms(s), types(s), expressions(s))	`definitions in s`,
.Row declarations(s)	@(variables(s), types(s))	`declared and defined types of variables in s`,
.Close.Table
 For s: documentation | name_of_documentation,
.Table Formula	Meaning
.Row types(s)	`types in declarations and definitions in s`,
.Row variables(s)	`symbols bound in declarations in s`,
.Row axioms(s)	`wffs assumed to be true` | `defined equalities`,
.Row theorems(s)	`wffs proved to be true`,
.Row assertions(s)	(axioms(s) | theorems(s))
.Close.Table
. Layout
To Be announced
.Close A "Cheat Sheat" Of Standard MATHS Notation