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
|
|---|
| @ | 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 ]
Sets
For Type T
Table| Symbols | Meaning
|
|---|
| @T | Type whose elements a sets of objects of type T
|
| x in A | x is a member of A
|
| A ==>B | iff for all x:A (x in B), subseteq
|
| |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 }
|
| |α | ={a:T||for some A:α(a in A)}
|
| A & B | Intersection { x:T. x in A and x in B }
|
| &(α) | ={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 Products, { (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
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
|
|---|
| 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] for some z(x R z and z S y)
|
| R | S | =rel[x:T1,y:T3] (x R y or x S y)
|
| 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})
|
| 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:
- do(x<10; x'=x+1; y'=y*x); no(x>=10)
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 (W Ross Ashby) format
.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
|
| 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)
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{....}.
or
Name ::=following,
.Net
...
.Close.Net
or remotely
Name::=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
Table| Symbol | Meaning
|
|---|
| infix(X) | X^( X><X ), For *:infix(X), x,y: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, 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
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