Sets

sets.html

There is a less formal introduction to this theory in [ intro_sets.html ]

Introduction

The classic argument looks like this in the language of sets:
Let

Socrates is_a Human,
Human are Mortal.
(above)|-Socrates is_a Mortal.

Here is another example, using the language of sets we can say:

birds ==> fly, all birds fly.
penguins ==> birds, penguins are birds.
And so conclude (in the face of the evidence):
penguins ==> fly.
So we might rethink our assumptions:
birds = flightless | flying. Birds are flying or flightless.
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

THEORY::=

Net{

logic_32_Set_Theory.html

}=::THEORY.

A key point is that in theory one can re-express statements in MATHS that use sets into expressions that use predicates instead.

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)
{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.

Long Format Representation

my_pets::@Animals=following,

stranger, AKA "Megan"
shadow
ginger

The raw source code is:

 .Set

 	element

 	element, comment.

...

 .Close.Set

An 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.

Enumerating Finite Sets

In computing and software engineering we often need to introduce and then describe a finite set of distinct named elements. One way to this is:

 	T::Sets,

 	e1::T,

 	e2::T,

...

 	e[n]::T,

 	|- T = {e1,e2,...e[n]}.

If the elements e1,e2,...,e[n] are distinct and free identifiers then the following syntax is natural short hand:

 	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.

 	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)

(Close Table)

Summary of Predicates

Table

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->@

(Close Table)

Syntax of Set Expressions

propositional_expression::= set_theoretical_proposition |...,
set_theoretical_proposition::= |[T:Types] (expression(T) "in" expression(@T) | expression(@T) "=" expression(@T) | expression(@T)),
For T:Types, expression(@T)::= simple_set_expression | union | intersection,
union::= SERIAL(intersection,"|"),
```
 	Dog | Cat
```
intersection::= SERIAL(complementary_set_expression,"&"),
```
 	Shot_haired & Barkless & Dog
```
complementary_set_expression::= Cartesian_product | complementary_set_expression complement Cartesian_product.
complement::="but_not" | "~", The text form is used in EBCDIC.
```
 	Animal~Dog
```
```
 	Animal~Dog~Cat
```
Note. The above definition is expressed recursively to express the associativity of complements:
A~B~C = (A~B)~C.
complementary_set_expression = Cartesian_Product #(complement Cartesian_product).
Cartesian_product::= SERIAL(possible_prefix_set_expression, "><"). Note: Cartesian products are sets of pairs of elements and are actually a subset of a different type.
```
 	Point = Real >< Real.
```
possible_prefixed_set_expression::= #( "|" | "&") simple_set_expression. Note: in fact the simple expression must return a set of sets for a prefix to be OK. If there are 2 prefixes then it must be a set of set of sets.
```
 	|{ {1,2}, {2,3} }
```
= {1, 2, 3}.
```
 	&{ {1,2}, {2,3} }
```
= {2}.
simple_set_expression::=set_name | elementary_set |"("set_expression")" | set_of_sets | set_of_maps | set_of_relations | simple_set_expression"."relational_expression | relational_expression "("set_expression")".
```
 	Animal
```
```
 	{ shadow, ginger }
```
```
 	( A \cup B ~ C )
```
```
 	@Animal
```
```
 	A<>->B
```
```
  shadow.breeds
```
```
	breeds(shadow)
```
set_of_sets::= "@" simple_set_expression | simple_set_expression "@" expression(Nat0).
```
 	@Animals
```
```
 	Animals@2
```
@A = { B | B==>A }.
A@n = { B:@A | Card(B) = n }.
1. 2008-06-27 Fri Jun 27 08:06 .
elementary_set::= intention | extension |comprehension | singleton | empty_set |type_name | "$"structure_description,
empty_set::="{}"|"$()",
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
```
intention::= "{" loose_binding #(","loose_binding ) "||" proposition "}" | "$" loose_bindings "(" proposition ")",
comprehension::= "{" expression where_lexeme loose_binding #(","loose_binding ) "." proposition "}",
where_lexeme::="||" | "." .
extension::= finite_extension |informal_extension,
finite_extension::="{" list_of_elements "}"| "$(" list_of_elements ")"
informal_extension::= "{" list_of_elements "..." "}"|"$(" list_of_elements "..." ")",
An informal extension will stop most automatic proof checkers from validating results.
list_of_elements::= element #(punctuation element),
singleton::= "{"element"}" | "$(" element ")".
For Type T, e:T, e::@T={e}.
element::= expression,
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:
my_circle::=$ Net{x,y:Real, x^2+y^2=y^2 },
CIRCLE::=Net{x,y:Real, r:Real, x0,y0:Real, (x-x0)^2+(y-y0)^2=r^2 },
(CIRCLE)|-my_circle=$ CIRCLE(r=>1, (x0,y0)=>(0,0)}
structure_description::= "$" documentation, [ notn_13_Docn_Syntax.html ] and [ notn_14_Docn_Semantics.html ]
structure_expression::=R(expression), [ notn_12_Expressions.html ]
|-structure_expression= "(" identifier "=>" expression #( (|",") identifier "=>" expression) ")",

Semantics of Set Expressions
1. |- (set0): t in {x:T||W(x)} iff W(t).
  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.
2. |- (unambiguous_null_set): {}.@T = {x:T||false}.
  Universal set
3. T::@T= {x:T||true},
  (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))}.
4. For f,x,X,W, {f(x) || x:X}::= {y || for some x:X(y=f(x))}.
  
  (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:
5. {z || for some x:X, y:Y, ... (z=e and (W))}
  If the W is missing it should be taken to be true.
  For example
6. even = { 2*n || n:Nat0 }.
  Note. This is one place where variables are declared after they are used.
7. (Set Operators)|- (union_semantics): For A,B: @T, A | B = {x:T || x in A or x in B }.
8. (Set Operators)|- (intersection_semantics): For A,B: @T, A & B = {x:T || x in A and x in B }.
9. (Set Operators)|- (complement_semantics): For A,B: @T, A ~ B = {x:T || x in A and not x in B }.
  
  Unary Complement Operator
  Expression like this
10. ~Cat are best thought of as abbreviations when the type of the set is known. If for example Cat is a subset of a type called Animal then
11. ~Cat = Animal ~ Cat.
  However, the null set symbol {} has no defined type and so it's complement is undefined.
  Here is an attempt to catch this
12. For Type T, A:@T, ~A::= T~A.
  
  Equality of sets
13. |- (eqsets): for A,B:@T, if for all x:T(x in A iff x in B) then A=B.
  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 ]
14. For A,B:@T, A<>B iff not(A=B).
  
  Conveniences
15. For x,y:T1, x is y::=(x = y),
16. For x:T1,X:@T1, x is_a X::=(x in X).
17. For Type T, A:@T, ~A::= T~A. Note, if the type of the elements of a set A is undefined then the complement of A is also undefined.
  
  Cardinality
  How many elements are in this set?
18. For X:@T, n:Nat0, |X| = n iff for n x:T (x:X).
19. For Type T, Card[T]::@T->Nat0= map[X:@T](|X|).
20. For Type T, X:@T, Card(X)::Nat0= Card[T](X).
21. For Type T, A:@T, n:Nat0, A@n = { X:@T || Card[T](X) = n }.
  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.
  
  Finite Sets
  A finite set can be formally defined as a set that can not be put into a one-one correspondence to a proper subset of itself. We can describe:
22. For Type T, Finite_sets(T)::@T=the subsets S of T that are finite. [ types.html#Finite_sets ]
23. For Type T, S:@T. Finite_sets(S)::@T={F:@S. F in Finite_sets(T) }.
  Notice that
24. |- (fin1): For Type T, A,B:@T, if A==>B in Finite_sets(T) then A in Finite_sets(T).
25. |- (fin2): For Type T, A,B:@T, if A in Finite_sets(T) then A&B in Finite_sets(T).
26. |- (fin3): For Type T, A,B:@T, if A,B in Finite_sets(T) then A|B in Finite_sets(T).
27. |- (fin4): For Type T, A,B:@T, if A in Finite_sets(T) then A~B in Finite_sets(T).
28. |- (cardinality_of_union): for Type T, α, β:Finite_sets(T) ( Card(α | β ) = | α | + | β | - |α & β| ).
  We can define a property of sets:
29. For Type T, S:@T, finite(S)::bool= (S in Finite_sets(T)).
  However me must avoid expressions that contain "/finite(P)".
  
  Quantifiers expressed using sets
30. For all X:@T, X=T iff for all x:T(x in X),
  A set in a context that demands a proposition is true iff there exists at least one member.
31. For X:@T, X::@= for some x:T(x in X),
32. For X:@T, for some x:T(x in X) = Card(X)>0.
33. For X:@T, if |X|=1 then the(A)::= the(x:T||x in A).
  There are short hand ways of stating properties of sets so that they can be used easily:
34. some(X)::= (X<>{}).
35. no(X)::= (X={}).
36. all(X)::= (X=T).
37. A and B::= some (A & B).
  Here is a readable distfix expression:
38. no A and B::= no (A & B).
  
  Set Operators
39. For T:Types, A,B:@T, A & B::= {x:T || x in A and x in B} ,
40. ∩::= "&".
41. &::@@T -> @T,
42. |-For β:@@T, &β={x:T || for all B:β(x in B)}.
43. (above)|-A & B = &{A,B}.
44. For T:Types, A,B:@T, A | B::= {x:T || x in A or x in B},
45. ∪::= "|".
46. |::@@T -> @T,
47. |-For β:@@T, |β={x:T || for some B:β (x in B)},
48. (above)|-A | B = |{A,B}.
49. For T:Types, A,B:@T, A ~ B::= {x:T || x in A and not x in B},
50. "but_not"::="~".
51. (above)|-(@T,|,{},&,T,~) in Boolean_algebra.
  1. A&B = B&A.
  2. A|B = B|A.
  3. A&(B&C) = (A&B)&C.
  4. A|(B|C) = (A|B)|C.
  5. A | A = A.
  6. A & A = A.
  7. A~A={}.
  8. ...
    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.
  9. A~B = A & (T~B).
  10. ~(A&B) = T~(A&B) = (T~A)|(T~B) = ~A | ~B.
  11. ...
  (Cartesian products): these look like set expressions but are really part of the MATHS theory of types.
52. For T:Types, A,B:@T, A><B::@(T><T)={ (a,b) || a in A and b in B }.
  
  (subsets): predicates.
53. For T:Types, A,B:@T, A==>B::= for all a in A(a in B),
54. ⊆::= "==>".
```
 		\subseteq::="==>"
```
55. A<==B::= B==>A.
56. all A are B::= (A==>B).
57. For T:Types, A,B:@T, A=>>B::= A ==>B and A<>B,
58. ⊂::= "=>>".
```
 		\subset::="=>>"
```
59. A<<=B::= B=>>A.
  There are many useful theorems for subsets:
  1. (above)|- (subseteq_reflexive): For all Types T, A:@T, A ==> A.
  2. (above)|- (subset_irreflexive): For all Types T, A:@T, not (A =>> A).
  3. (above)|- (subseteq_transitive): For all Types T, A,B,C:@T, if A ==> B ==> C then A ==> C.
  4. (above)|- (subset_transitive): For all Types T, A,B,C:@T, if A =>> B =>> C then A =>> C.
  5. (above)|- (subset_subseteq): For all Types T, A,B,C:@T, if A =>> B ==> C then A =>> C.
  6. (above)|- (subseteq_subset): For all Types T, A,B,C:@T, if A ==> B =>> C then A =>> C.
    Note: these are easier to write using the relational product:
  7. (subseteq_transitive)|-(==>; ==>) = ==>.
  8. (subset_transitive)|-(=>>; ==>>) = =>>.
  9. (subset_subseteq)|-(=>>; ==>) = =>>.
  10. (subseteq_subset)|-(==>; =>>) = =>>.
  11. (above)|- (subset_complement): For all Types T, A,B:@T, if A ==> B then T~B ==> T~A.
  12. (above)|- (intersection_is_subset): for all Types T, A,B:@T, A & B ==> B and A & B ==>A.
  13. (above)|- (union_is_superset): for all Types T, A,B:@T, A ==> A | B and B ==> A | B.
  14. (above)|- (subset_union_form): for all Types T, A,B:@T, A==>B iff A | B = B.
  15. (above)|- (subset_intersection): for all Types T, A,B:@T, A==>B iff A = A&B.
    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?
  16. (above)|- (Product_of_subsets): for all Types T, A,B,C,D:@T, if A==>C and B==>D then A><B ==> C><C. This result is the basis for arguing that a license plate id with three letters and three digits will need six characters to encode it.
  Proofs are omitted but can be supplied by the reader as an exercise... [click here Prove_subset_properties if you can fill this hole]
  
  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:
60. Choice::@=For all A:Sets, π:partitions(A), some choice:π-->A, all B:π ( choice(B) in B).
  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:
61. |- (axiom_of_choice): Choice.
  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 ]
Proofs involving Sets
1. (above)|- (glb): A<==A&B==>B.
2. (above)|- (lub): A==>B|A<==B.
  There are also some easily proved derivation rules
3. (above)|- (seteq): A=B iff A==>B and B==>A.
4. (above)|- (converse): A==>B iff ~B==>~A.
5. (above)|- (barbara): If A==>B==>C then A==>C.
6. (above)|- (celarent): If no A are B and all C are B then no C is B.
7. (above)|- (darii): If all M is P and some S are M then some S are P.
8. (above)|- (ferio): If no M is P and some S are M then some S are ~P.
  And so on thru most of the medieval catagorical syllogisms [ syllogisms.html ]
Epithets and term logic -- Use Sets instead
This is a the 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. What would be very handy would be able to have positive and negative epithets. The effect would be like including term logic into MATHS.
Use '&' and '~' to construct terms
penguin ⊂ aquatic & flightless & bird.
ostriche ⊂ bird & flightless ~ aquatic.
Representing complex families of sets -- ontologies or domains of discourse -- in this form make many consequence transparent. For example
No penguin and ostriche, one is aquatic and the other is not.
penguin | ostriche ⊂ flightless & bird ⊂ bird.
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:
large::@object->@object.
Possibly with this definition in terms of an attribute size:object->Real&Positive.
For S:@object, large(S) = {x:S. size(x) > 75 * mean(size o S)}, perhaps, or
large(S) = top_quartile[size](S), (if you define top_quartile)...
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...

Families of sets
[ logic_31_Families_of_Sets.html ]

Principia Mathematica 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.
Chapter_14::PBI=following
Net
1. |-NONSTANDARD.
2. T::Types.
3. |-Set Operators // :: infix( T^T, @T, @T).
4. For all f:T->T, A:@T, f//A = { f(x) || x:A }.
5. For A,B,C:@T.
6. (-1)|-| //{ {A,B}, {C} } = { |{A,B}, |{C} } = {A|B, C}.
7. (-1)|-| | //{ {A,B}, {C} } = | {A|B, C } = A | B | C.
8. (Set Operators)|-|{{A,B}, {C}} = {A,B,C }.
9. (Set Operators)|-||{{A,B}, {C}} = |{A,B,C } = A | B | C.
10. (above)|-| | //{ {A,B}, {C} } = ||{{A,B}, {C}} .
  Whiehead and Russell (PM *42) prove that
11. (above)|- (infinite_union_associative): For all κ: @@@T, | |// κ = | | κ.
12. (above)|- (infinite_intersection_associative): For all κ: @@@T, & &// κ = & | κ.
(End of Net)
MinTerms
MINTERM::={ A:Sets, B:@A, p::=map[ a:A] (map b:B(a in b)). For each a in A there is an array of true/false values, one for each set in B, named p(a). We can partition A into cells of elements with the same array of values:
P::=A/p Thus, given for a1,a2:A, a1 =/p a2, for all b:B, a1 in b iff a2 in b.

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

MINTERM

Tree by Knuth

Source: Knuth 69, Vol 1, Section 2.3 Trees p305

A typical tree is T where

T::=(nodes=>{1,1.1,1.2,1.2.3}, root=>1, m=>2, subtree=>(T1,T2)),
T1:=(nodes=>{1.1}, root=>1.1, m=>0, subtree=>()),
T2:=(nodes=>{1.2,1.2.3}, root=>1.2, m=>1, subtree=>(T3)),
T3:=(nodes=>{1.2.3}, root=>1.2.3, m=>0, subtree=>()).

Definition of a tree

TREE::=
Net{
1. |-numbers.
2. nodes::Finite(Sets),
3. root::nodes,
4. fan_out::Nat0,
5. subtree::1..fan_out->@nodes, -- These are ordered trees
6. |-nodes~{root}>== {subtree(i) || i:1..m},
7. |-For all i:1..m, subtree(i) in $ TREE.
}=::TREE.
|-For T:$ TREE, i:Nat0, T[i]::=T.subtree[i].
??{convergence because lim |nodes|=0}??
forest::={F:@TREES||for T1,T2:F(no T1&T2)}
(above)|-if T:$ TREE then T~{root} in forest.

. . . . . . . . . ( 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 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

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

Glossary

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).

given::reason="I've been told that...", used to describe a problem.

given::variable="I'll be given a value or object like this...", used to describe a problem.

goal::theorem="The result I'm trying to prove right now".

goal::variable="The value or object I'm trying to find or construct".

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.

hyp::reason="I assumed this in my last Let/Case/Po/...".

QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.

QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.

RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

Contents

Sets

Rapid History

Introduction

Types

Set Expressions

Constructors

Long Format Representation

Enumerating Finite Sets

Summary of Set Operators

Summary of Predicates

Syntax of Set Expressions

Semantics of Set Expressions

Definitions

Unary Complement Operator

Equality of sets

Conveniences

Cardinality

Finite Sets

Quantifiers expressed using sets

Set Operators

The Axiom of Choice

Proofs involving Sets

Epithets and term logic -- Use Sets instead

Families of sets

Principia Mathematica Chapter 42 -- Partly Baked Idea

MinTerms

Tree by Knuth

Definition of a tree

Notes on MATHS Notation

Notes on the Underlying Logic of MATHS

Glossary

End