Sets

sets.html

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	@T

 	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

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

Sample of Assumed Properties

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

Contents

Sets

Notes on MATHS Notation

Notes on the Underlying Logic of MATHS

Glossary

End