- A "Cheat Sheat" Of Standard MATHS Notation
- : Purpose
- : Logic
- : Sets
- : Relations
- : Maps/Functions
- : Lists and Strings
- : Sets of Sequences
- : Structures
- : Documentation Nets
- : RESULTS and SYSTEMS
- : Maps_and_Sets
- : unary operations
- : infix operations
- : Dynamics
- : Overloadings
- : SERIAL operations
- : Relations
- : Standard Types
- : Proofs
- : Meta-Functions
- : Layout
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- do(x<10; x'=x+1; y'=y*x); no(x<10)
is equivalent to the shorter

- 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**Formula Meaning 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-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
.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**Symbol Meaning () empty list/string (x,y,z) list with three elements, 1st, 2nd, and 3rd. z=x?y iff x is the first(z) and y rest(z). #X Any number of X's, Semigroup generated from X by (!) z = x! y iff 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**Symbol Meaning 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**Symbol Meaning $ Net{x:X, y:Y, ...} { (x=>a, y=>b,...) || a in X and b in Y and ...} x maps $ 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).

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

orName ::=following,

.Net

...

.Close.Net

or remotelyName::=URL.

- For Name_of_documentation N,
**Table**a(N) tpl of variables in N, $(N) an(N), a(N), $ N set of $(N) that fit the N, set N $ N, the N(P) the($ N and P) the unique $ N that also fits P, @N collection of sets of objects satisfying N, #N strings of objects that fit N, %N LISP-like lists of objects that fit N, |-N Asserts a copy of N in current document. Uses N Inserts a copy of N's definition into current document. With N Inserts a copy of what N is defined to be into current document. By N Derivation 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)

- For N1, N2:Name_of_documentation|set_of_documentation, Q1, Q2, ...:Quantifiers
**Table**not N1 complementary documentation to N1, N1 o N2 combine pieces of documentation, N1 and w Net{D. w } where N is the name of {D}, N1 with{D2} Net{D. D2 } where N is the name of {D}, N1->N2 Sets in @(N1 and N2) with N1 as an identifier, N1^N2 functions from type $ N2 to type $ N1, N1(Q1)-(Q2)N1 Relations between N1 and N2.

(Close Table)

## RESULTS and SYSTEMS

## Maps_and_Sets

- (above)|-For f:X->Y, A1,A2:@X, B1,B2:@Y, following,
- 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).

- ()|-For f:X->Y,
- 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)

- (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. - For X:Set, unary(X) =X^X.
- For X:Set, f:unary(X), x:X,
**Table**Symbol Context Meaning fix(f) @X { x:X || f(x)=x }. f(x) X x.f f @X->@X fun A:@X {f(a) || a:A}, f #X->#X fun a:#X (fun i:1..|a| (f(a[i])), 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

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

- (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),
- (above)|-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 x:*e (x' = x * e ), e*:y (e * y = y')

(Close Table)

## Overloadings

- For *:infix(X), Y:=@X, Z:=X^A,
**Table**Symbol Context Meaning * Y><Y->Y fun [A,B] {a*b || a:A, b:B}, * X><Y->Y fun [x,B] {x*b || b:B}, * Y><X->(@X) fun [A,x] {a*x || a:A}, * Z><Z->Z fun [f,g](fun a:A (f(a)*g(a) ) ), * X><Z->Z fun [x,f] (fun a:A (x* f(a) ) ), * 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**+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)

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

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

- For X,Y: Sets, R,S: @(X,Y),
**Table**R is_more_defined_than S pre(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. Nat 1.. Posititive 1.. Bit 0..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 Q P P and Q Q not(P and Q) not P or not Q P,Q P and Q P or Q, not P Q P or Q, not Q P not(P or Q) not P not(P or Q) not Q P, if P then Q Q not Q, if P then Q not P not(if P then Q) P, not Q P iff Q if P then Q P iff Q if 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**Given Annotation Derive Condition 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**Given Let{Case1|-Conclusion} Else Let{Case2...|-Conclusion}|-Conclusion P or Q P Q if P then Q not P Q P iff Q P,Q not P, not Q 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 if P then Q P,not Q P or Q not P,not Q P not 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. - symbol:@( Strings, Types, Values)
- For s: documentation | name_of_documentation,
**Table**Symbol Type Meaning terms(s) Sets terms defined in s, expressions(s) Sets expressions 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)

- For s: documentation | name_of_documentation,
**Table**Formula Meaning 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 - STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
# Glossary

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

Symbol | Type | Meaning |
---|---|---|

@ | Types | ={true,false} |

and, or, not | infix(@) | 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). |

iff | infix(@) | 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**

Formula | Meaning |
---|---|

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 = y | True if x and y are defined and equal, else false. |

x <> y | Negation of x=y, Pascal and BASIC notation. |

x != y | Negation of x=y, The C/C++/Java/PHP/ ... notation |

(Close Table)

[ Lower_Predicate_Calculus_with_equality in logic_10_PC_LPC ]

Symbols | Meaning | Definition |
---|---|---|

@T | Type whose elements a sets of objects of type T | |

x in A | x is a member of A | |

A ==>B | subset or equal | for 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 | |

@B | Subsets of B | { A || A ==> B } |

B@n | Subsets of a given size | { A: @B || |A| = n } |

A | B | Union | { x:T. x in A or x in B } |

|α | Union | ={a:T||for some A:α(a in A)} |

A & B | Intersection | { x:T. x in A and x in B } |

&(α) | Intersection | {a:T||for all A:α( a in A )} |

A are B | A ==>B | |

A=>>B | A==>B and not A=B. | |

A>=={X1, X2,... } | Partition | |

A><B | Cartesian Product | { (a,b)|| a:A, b:B} |

(x1, x2, x3, ... xn) | n-tuple/list/string | |

X1><X2><X3...><Xn | set of n-tuples | |

For Q:quantifiers, Q A | for Q x:T (x in A) | |

some A | A is not empty | A <> {}. |

no A | A is empty | A = {}. |

1 A | A = { 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

We use R, S: @(T1,T2) as typical relations with A:@T1 and B:@T2:
**Table**

Formula | Meaning |
---|---|

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:

. . . . . . . . . ( end of section A "Cheat Sheat" Of Standard MATHS Notation) <<Contents | End>>

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 ]

For a more rigorous description of the standard notations see