There is a less formal introduction to this theory in [ intro_sets.html ]
Rapid History
Sets are implicit in much of Aristotlean logic (Ancient Greece... Medieval).
George Cantor (1800's) developed the theory as part of his research into
the mathematics of infinity. Sets rapidly became the language of modern
mathematics. Russell (1990's) uncovered paradoxes in the Cantor theory.
This lead to the Zermelo-Frankel axiomatic theory(THEORY below), Halmos's
Naive set theory, and Whitehead and Russell's Theory of Types.
Introduction
These notes are about a language that lets talk both naturally and
rigorously at the same time. Everyday language is full of references to
sets of objects, classes, types of things, and on. The simple notation
proposed here makes much of this rigorous. Sets also form a foundation for
several more complex ideas which together form a simple yet effective way
of talking about complex pieces of software - such IBM's CICS(Customer
Information C?? Systems), elevators, or Hotel Bookings for example.
For example, using the language of sets we can say:
And so conclude (in the face of the evidence):
So we might rethink our assumptions:
This might lead us to think about how big the various sets are and conclude that most birds are not flightless...
Types
Every object belongs to a type T -- where the type describes the kind of
things that can be done to the object or could produce objects of the type.
For any type T there is an another type symbolized by @T with objects that
are sets of objects of type T.
.Note
Some sets are not types - A type by definition is a universal set or domain of discourse, but a set is determined by the type of element plus some rule(predicate) indicating what is in the set. We assume that whenever we have a set of some kind or other than it is a set of objects of the same type. However a subset (or a set for short) does belong to a type and so determines the types of the elements in it. It is therefore safe to use a subset of a type in a declaration of a variable of the right type, and with values/properties limited to those of the set(compare type and subtype in Ada).
The restriction that each set has elements all of the same type is not a particularly restrictive rule given the freedom with which we can construct types as we need them.
The main expressions involving sets in MATHS are:
Set Expressions
Constructors
Table
| Form | Meaning | Type | (Notes) |
|---|---|---|---|
| {} $() | null set | Ambiguous type. | |
| T | universal set | @T | |
| {e1} $(e1) set(e1) | singleton | @T | (e1:T) |
| e1 | {e1} | @type(e1) | (only if context requires a set) |
| {e1,e2,e3,...} set(e1,e2,e3,...) $(e1,e2,e3,...) | set of enumerated items | @T | (extension) |
| {x:T || W(x)} {x:T. W(x)} $[x:T](W(x)) set(x:T WHERE W(x)) | set of things satisfying a property W | @T | (intension) |
| $ Net{...} | structured set | type(Net{...}) | |
| $ Name | set of elements with structure Name | type(Name) |
There is also a more readable format that is suitable for large sets made up of
complex objects --
[ Long Format ]
below.
Long Format Representation
For example
The raw source code is:
.Set
element
element, comment.
...
.Close.SetAn element in a long set can be several lines long. It starts with an indentation. Each element is an expression and may be terminated by a comma and a comment. Comments are ignored.
Long sets are normally used with a definition like this:
Name::@Type = following,When rendered for display or printing a long set should shown as an unordered list with each element marked with a bullet or similar marker.
T::Sets,
e1::T,
e2::T,
...
e[n]::T,
|- T = {e1,e2,...e[n]}.
T::={e1,e2,...,e[n]}
It defines T and declares the elements in T.
For example:
Direction::={down, up}.
means
Direction::Sets.
down::Direction.
up::Direction.
|- Direction={down, up}.
Note, that the above does not guarantee that the elements have to be different -- even if we use different identifiers for the elements. As written, it is possible for some else to take our document and reuse it with a substitution which makes two variables the same. To stop this, and to be very clear about what we want we must add extra assumptions like this:
Direction::={down, up}.
|- down <> up.or
Lights::={Green, Amber, Red}.
|- 3 Lights.See Cardinality below. This is a little clumsy and counter-intuitive, and so I may add a new notation that handles this.
If you want the elements to be in order then see
[ math_77_Enumerations.html ]
Summary of Set Operators
Table
| Symbols | Example | Meaning | Type |
|---|---|---|---|
| & ∩ AND | S1 & S2 | Intersection | @T><@T->@T |
| & ∩ AND | & β | Intersection | @@T->@T |
| | ∪ OR | S1|S2 | union | @T><@T->@T |
| | ∪ OR | |β | union | @@T->@T |
| ~ NOT | S1 ~ S2 | Complement | @T><@T->@T |
| @ \powset SetOf | @S1 | powerset,set_of_subsets | @T->@@T |
| >< Product | S1><S2 | Cartesian product | @T><@T->@(T><T) |
| Symbols | Example | Meaning | Type |
|---|---|---|---|
| in ∈ | e1 in S1 | membership | T><@T->@ |
| <> | S1 <> S2 | inequality | @T><@T->@ |
| != | S1 != S2 | inequality | @T><@T->@ |
| == | S1 == S2 | equality | @T><@T->@ |
| ==> ARE | S1 ==> S2 | subset or equal | @T><@T->@ |
| =>> | S1 =>> S2 | proper subset | @T><@T->@ |
| some | some S1 | S1<>{} | @T->@ |
| - | S1 | some S1 | @T->@ |
| no | no S1 | S1={} | @T->@ |
| all | all S1 | S1=T | @T->@ |
| and | S1 and S2 | some(S1&S2) | @T->@ |
Dog | Cat
Shot_haired & Barkless & Dog
Animal~Dog
Point = Real >< Real.
|{ {1,2}, {2,3} }
&{ {1,2}, {2,3} }
Animal
{ shadow, ginger }
( A \cup B ~ C )
@Animal
A<>->B
shadow.breeds
breeds(shadow)
@Animals
Animals@2
An informal extension will stop most automatic proof checkers from validating results.
MATHS has a special way to define a set - by describing it as a collection of tuples under some constraint. Any piece of documentation contains declarations and axioms that can be interpreted this way. Examples might be:
(in): For Type T, A:@T, t:T, t in A ::@=`it is true that t is a member of
set A`.
{}::@T= {x:T||false},
(singleton_semantics): For a,b,c,...: T, {a}::@T={x:T||x=a}.
(coerced_singleton): For a,b,c,...: T, a::@T={a}.
(extension_semantics): For a,b,c,...: T, {a,b,c,...} ::@T= {a} | {b} | {c}|... .
(projection_semantics): For f,x,W, {f(x) || for some x:T (W)}::= {y || for some x:T(y=f(x) and (W))}.
An object is a set when and only when membership solely determines equality. "Bags" have the same abstract operators as "Sets" but two bags are equal only when their members occur the same number of times in both Bags. Formally a "Bag of X's" is an object of type Nat^X. The most general form of this model will be found under [ semiring in math_41_Two_Operators ]
Cardinality
How many elements are in this set?
Note: avoid using /Card(n) or /|_|(n) as it does not define the types of objects being counted.
Quantifiers expressed using sets
A set in a context that demands a proposition is true iff there exists at least one member.
There are short hand ways of stating properties of sets so that they can be used easily:
Here is a readable distfix expression:
(Cartesian products): these look like set expressions but are
really part of the MATHS theory of types.
(subset): predicates.
The Axiom of Choice
MATHS assumes that given a collection of disjoint sets, then we can choose
one member of each to be a representative of that set. Formally:
Notice that this assumption is obviously true for finite cases.... it is some the weirder infinite sets that make it doubtful.
The following formally asserts that the axiom of choice is part of the
MATHS system:
This appears in other forms as part of the theory of relations and functions, [ Choice in logic_5_Maps ]
The axiom of choice was used long before Zermelo made it an explicit axiom in 1904. It appears as the axiom of selection in Principia Mathematica. It was discussed for a long time but is used by praticing mathematicians without qualams. For more history, see [ Axiom_of_Choice ] in the Wikipedia.
Also see Skolem functions in [ logic_5_Maps.html ]
| To prove | Assume | Derive | Notes |
|---|---|---|---|
| A==>B | a:A | b:B | |
| no(A) | a:A | RAA | |
| A=B | a:A | a:B | And also |
| - | b:B | b:A |
There are a large number of provable facts about sets
There are also some easily proved derivation rules
And so on thru most of the medieval catagorical syllogisms [ syllogisms.html ]
Chapter 42 -- Partly Baked Idea
This comes from rereading section 42 of Principia Mathematica and noticing
a couple of odd theorems about the union and intersection of sets
of sets of set.
I doubt if they will be useful.
They force the use of a nonstandard notation for the set extension of a function, so I'm enclosing them in a Net.
Whiehead and Russell (PM *42) prove that
A typical tree is T where
|-For T:$ TREE, i:Nat0, T[i]::=T.subtree[i].
??{convergence because lim |nodes|=0}??
Idea
This is a new idea designed to handle natural expressions like
flightless bird. An epithet is a word or phrase written in front of
the name of a set (not an expression). It is always a subset of the named
set.
There is a risk of confusion when talking about sets of strings.
A formal justification for the syntax is by defining a prefix operator on sets of the correct type:
Should this be abbreviated to
flightless::epithet(Animal) = `_ can not fly'.
. . . . . . . . . ( end of section Sets) <<Contents | End>>
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 = Net{radius:Positive Real, center:Point}.
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