.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 Definition .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 subset or equal for all x:A (x in B) .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 Union ={a:T||for some A:\alpha(a in A)} .Row A & B Intersection { x:T. x in A and x in B } .Row &(\alpha) Intersection {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> {}. .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] (x R y or x S y), relational union .Row R & S =rel[x:T1,y:T3] (x R y and x S y), relational intersection .Row R; S =rel[x:T1,y:T3] for some z(x R z and z S y) , relational product .Row A; R =rel[x:T1,y:T3] (x in A and x R y) , left limit .Row R; A =rel[x:T1,y:T3] (x R y and y in B) , right limit .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}), transitive etc closure .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> 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 (x,y,z) list with three elements, 1st, 2nd, and 3rd. .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 Long list can be encoded in a long form .As_is .List .As_is One paragraph or formula per item .As_is .Close.List . 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 For *:infix(X), x,y:X. .Table Symbol Meaning .Row infix(X) X^( X>Y fun [A,B] {a*b || a:A, b:B}, .Row * X>Y fun [x,B] {x*b || b:B}, .Row * Y>(@X) fun [A,x] {a*x || a:A}, .Row * Z>Z fun [f,g](fun a:A (f(a)*g(a) ) ), .Row * X>Z fun [x,f] (fun a:A (x* f(a) ) ), .Row * Z>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 of a given type, 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 In informal documents, you can also put a rebuttal for a statement or an argument: .As_is .But .As_is ... .As_is .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 .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