There is a less formal introduction to this theory in [ intro_sets.html ]
The classic argument looks like this in the language of sets:
Let
Here is another 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...
.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:
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) |
{e(x) || x:S, W(x)} {e(x). x:S, W(x)} | set of vales of e(x) for som x satisfying W(x) | @T | (comprehension) |
$ 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.
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 ]
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
Animal~Dog~Cat
Note. The above definition is expressed recursively to express the associativity of complements:
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
Note "{}" is ambiguous as to type.... is a setof no animals, or a set of no real numbers. The type of "{}" needs to be worked out from the context. To remove the ambiguity use
{}.@Animal
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`.
null set or empty set
{}::@T= {x:T||false},
Note "{}" the type of "{}" above is @T and not determined by the symbol itself.
It is determined by the context of the symbol. To remove all ambiguity use the standard
MATHS technique of using ".type" to define the type.
(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))}.
(Comprehension semantics): an expression like {e || x:X, y:Y, ..., W} should be interpreted as a generalisation of the above whenever e is an expression and W a proposition:
If the W is missing it should be taken to be true.
For example
Note. This is one place where variables are declared after they are used.
However, the null set symbol {} has no defined type and so it's complement is undefined.
Here is an attempt to catch this
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 ]
Note: avoid using /Card(n) or /|_|(n) as it does not define the types of objects being counted. Instead the expression T@n defines the type and the number of elements.
Notice that
We can define a property of sets:
However me must avoid expressions that contain "/finite(P)".
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:
Note. ~A is a well defined set expression as long as A is a subset of a known type T. Instead in MATHS if A is a subset of a Type T then ~A= T~A.
(Cartesian products): these look like set expressions but are
really part of the MATHS theory of types.
(subsets): predicates.
\subseteq::="==>"
\subset::="=>>"
There are many useful theorems for subsets:
Note: these are easier to write using the relational product:
We could use the above two eqivalences to reason algebraically about subsets. They are both inspired by lattice theory.
Some of these theorems are also stated below... TBA?
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 practicing mathematicians without qulams. 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 ]
Use '&' and '~' to construct terms
Representing complex families of sets -- ontologies or domains of discourse -- in this form make many consequence transparent. For example
For more on this see [ logic_8_Natural_Language.html ] (Semantics) and [ notn_16_Classification.html ] (Notation). Caveats when translating natural language into sets.
First, these classifications in natural language are often based on defining arbitrary boundaries. Sometimes you need to attach attributes to the elements of a set to get a consistent and realistic logic. The classic example would be the adjective bearded when applied to the set of men. Here is the argument of the beard`. Where do you draw the boundary between bearded and beardless? What happens when you take a bearded person and start removing hairs from the face... when do they become beardless. If we reverse the process and let one hair grow at a time... when has the person become bearded.
Second, one needs to be careful of adjectives that define subsets relative to the superset. For example: large and small are not absolutes. A 'small elephant` is larger (I guess) than a large dog. So large & dog does not encode the semantics of large correctly. It can not be a separate set. Instead it should be defined as a map from a set into a subset:
Possibly with this definition in terms of an attribute size:object->Real&Positive.
By the way, as a final warning -- what about bearded dog? One must be careful to defines sets as subsets and not translate the terms that move the subsets outside of their sets -- except for humorous, poetic, or other creative processes.
Perhaps a traditional Philosophy 101 course would be wise...
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
Source: Knuth 69, Vol 1, Section 2.3 Trees p305
A typical tree is T where
|-For T:$ TREE, i:Nat0, T[i]::=T.subtree[i].
??{convergence because lim |nodes|=0}??
. . . . . . . . . ( end of section Sets) <<Contents | End>>
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