[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ ] / intro_sets
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun Oct 2 11:45:34 PDT 2011

# Sets

This introduces set theory from the point of view of a computer professional using ASCII. For the traditional notation see [ 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`
There 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

1. |-For x:T, x in T and not x in {}
2. |-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

3. A & B::={c || c in A and c in B},
4. A | B::={c || c in A or c in B},
5. A ~ B::={c || c in A and not( c in B) },

Definitions of relationships

6. |-For A,B, A = B iff A==>B and B==>A,
7. For A,B, A==>B::= for all a:A(a in B),
8. For A,B, A=>>B::= A==>B and not A=B.

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

Useful abbreviations

11. For A:Sets, a:Elements, A|a::=A|{a},
12. a|A::={a}|A,
13. etc.

Cardinallity -- size of a set

14. |A|::Nat0= the number of elements in A.
15. 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

16. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

# Glossary

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