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



    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


  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.