- |-For x:T, x in T and not x in {}
- |-For e:T, e in {e} and e in {...,e,...} and e in {x:T||W(x)} iff W(e).
Note. The

|-

symbol marks a statement that is asserted as being true - either as an axiom, or because it can be proved from other assertions.Definitions of Set Operations

- A & B::={c || c in A and c in B},
- A | B::={c || c in A or c in B},
- A ~ B::={c || c in A and not( c in B) },
Definitions of relationships

- |-For A,B, A = B iff A==>B and B==>A,
- For A,B, A==>B::= for all a:A(a in B),
- For A,B, A=>>B::= A==>B and not A=B.
- For A,B, A>==B::=( |B=A and for all X,Y:B(X=Y or X&Y={}) ),
- For A,B, A>==B iff for all a:A, one X in B(a in X).
Useful abbreviations

- For A:Sets, a:Elements, A|a::=A|{a},
- a|A::={a}|A,
- etc.
Cardinallity -- size of a set

- |A|::Nat0= the number of elements in A.
- A@n::@A=subsets of n elements taken from set A
# 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

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

For any type T there is an another type (symbolized by @T) of objects that are sets of objects of type T. For example {1,2,3} is a set of type @Nat because 1, 2 and 3 are of type Nat.

The subsets of a given type are not (in MATHS) a type. However a set does belong to a particular type: a set A is of type @T if and only if A's elements must be of type T. It is therefore unambiguous to use the symbol/name for the type to be the universal set of that type.

The main expressions involving sets in MATHS are:

Expression Meaning Type.

------------------------------------------------------------------

{},$() null set Overloaded

T universal set @T

@T Sets of elements of type T @@T

{e1},$(e1) singleton @T

where e1 is of type T

{e1,e2,e3,...} extension @T

$(e1,e2,...) extension @T

where e1,e2 ,e3,... are all of type T

{x:T || W(x) } intension @T

$[x:T](W(x)) intension @TThere is a newer form:

set{x:T. W(x)} intension @T

e1 in S1 membership T><@T -> @

S1 & S2 intersection @T><@T -> @T(serial)

S1 | S2 union @T><@T -> @T(serial)

S1 ~ S2 complement @T><@T -> @T

S1<> S2 inequality @T><@T -> @(parallel operator)

S1 = S2 equality @T><@T -> @(parallel operator)

S1==>S2 subset or equal @T><@T -> @(parallel operator)

S1=>>S2 subset @T><@T -> @(parallel operator)

S1>==S2 Partition @T><@@T ->@(parallel operator)

S1 non-empty set @ (overloaded)

SetOf(S) @S @@T

Finite_sets(S) finite subsets of S @@T

S@n Subsets of size n @@T

------------------------------------------------------------------The '$' (currency symbol) is a theoretical notation, the braces are a traditional shorthand. SetOf spells out the meaning of "@". Finite_sets a very common in computerized systems and computer science.

Sample of Assumed Properties