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
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
Definitions of relationships
Useful abbreviations
Cardinallity -- size of a set
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 ]
For a more rigorous description of the standard notations see