Everything on this page depends on
[ logic_30_Sets.html ]
for syntax, semantics and properties.
For Type T.
- For S:@T, @S::= the set of subsets of a set S,
- For S, @S::@@T= @^ S, the set of subsets of S, also known as the power set.
- For S, SetOf(S)::= @S, and form used with audiences unused to MATHS and/or
set theory.
- (above)|-{1,3} and {2} in SetOf({1,2,3}).
- (above)|-@S={B:@T || B==>S}.
- (above)|-|@^S|=|@|^|S|=2^|S|,
A family is a collection of subsets of a given set - Given a set S of
elements {x,y,...} then @S is the set of all subsets of S, @S = {{},{x},
{x,y},{y},...}. @@S is short for @(@S) - the set of subsets of subsets of
S. Thus @@S={{}, {{}}, {{},{x}}, {{},{y}}, {{x},{y}},...}. An element of
@@S is a called a family of subsets of S. It turns out that many important
ideas can be best modelled as particular kinds of families - in particular,
abstract families of languages, families of open and closed sets,
partitions and covers all turn out to be important.
- |- (union): For β:@@T, |(β)={x:T || for some B:β (x in B)},
- |- (intersection): For β:@@T, &(β)={x:T || for all B:β(x in B)}.
For Type T, A,B:@T.
- (union)|- (family1): |{A} = A.
- (intersection)|- (family2): &{A} = A.
- (union)|- (family3): |{ A, B } = A|B.
- (intersection)|- (family4): &{ A, B } = A&B.
- (union, intersection)|- (family5): For α:@@T,A:α( &α ==> S ==> |α).
In the following "{}" is short for the "{}.@T", the null or empty set of subsets of type T.
- (union)|- (null_family_union): |{} = {}.
- (intersection)|- (null_family_intersection): &{} = T.
Can you provide proofs
[click here family if you can fill this hole]
?
. . . . . . . . . ( end of section Quick results) <<Contents | End>>
Families that have every element in them at least once, but may overlap...
- For S:Sets, covers(S)::={α:@@S || |(α)=S},
- (covers)|-{S} in covers(S),
- (covers)|-for A:@S {A,S~A} in covers(S),
- (covers)|-for α, β:covers(S)(α | β in covers(S)),
- (covers)|-for α:covers(S), β:@@S, if α==>β then β in covers(S)).
If S is a finite set and C:@S, then we can call each element of C a simplex. When we do this we imply that the elements of C are classified by the number of elements in them:
- For c:C, dim(c)::=order(c) ::= |C|-1, for p:0..|S|-1, p.simplex={c:C || dim(c)=p}.
A face f of a simplex c in C is any simplex which is subset of c.
- For p,c, p.face(c)::=@c and p.simplex.
For p,c, faces(c)=|[p](p.face(c)).
There are several definitions of a simplicial complex.
Source: According to Ron Atkin(Casti92, Atkin74):
- (atkin): C in simplicial_complex iff S==>C and for all c:C(faces(c) in C).
The dimension of a simplicial complex C, dim(C) ::=max(dim(C)).
If dim(C)=n then S can be embedded in a Euclidean Space of 2n+1 dimensions so that
- (1) each simplex of dimension p is a convex polytope of dimension p
- (2) the convex polytopes overlap iff the simplices do.
Given a family C of subsets of a finite set S then we can construct an Atkin-complex by adding all subsets of elements of C to C:
- complex(C)::={x:@c || for some c:C }.
Another definition (JamesJames68) is
C is a simplicial_complex iff for all c,c':C, either c&c'={} or c&c' in faces(c) and faces(c').
Simplicial Complexes are generated by relations between finite sets
[ complex in logic_42_Properties_of_Relation ]
for example. The link has some nice graphics.
A mosaic is a collection of mutually disjoint subsets of a set that may or may not cover the set.
Source: Botting 1970
- For S:Sets, mosaics(S)::={μ:@@S || for all A,B:μ, if A<>B then A&B={}}.
- For S:Sets, μ:mosaics(S), free(μ)::=S~ |(μ).
- (mosaics)|-for S, ( {S},{{}} )in mosaics(S) ).
- (mosaics, free)|-for A:@S, {A,S~A} in mosaics(S) and free({A,S~A} )={}.
- (mosaics)|-for μ:mosaics(S), ν:@μ (ν in mosaics(S)).
Mutually disjoint covers.
- For S:Sets, partitions(S)::= covers(S) & mosaics(S).
- (mosaics, partitions)|-For μ:mosaics(S) ( (μ | free(μ) ) in partitions(S) ),
- For π:@S, S>==π::=for all a:S, one b:π(a in π),
- (-1, partitions)|-For all π: partitions(S), S>==π,
- (partitions)|-For all A,B:@S, {A&B,A~B} in partitions(S).
- For S,π, s:S, π(s)=the [A:π]( s in A ).
- (partitions)|-For S, π, rel[a,b](π(a)=π(b)) in eguivalence_relation.
[ Equivalence Relations in logic_41_Maps ]
.Used_in topology(continuity, limits,...).
[ math_91_Topology.html ]
Useful whenever the idea of limit is needed to define what happens to iterative and recursive processes.
- For S:Sets, open_family(S):@@S::= { open:@S || (open,&,{}) in monoid and for G:@open(|(G) in open) and S in open },
- |-for all open:open_family(S), G:finite(open)(&(G) in open).
- For S:Sets, closed_family(S):@@S::= { closed:@S || (closed,|,S) in monoid and for all G:@closed( &(G) in closed) and {} in closed },
- |-for closed:closed_family(S), G:finite(closed) (|(G) in closed).
- (Duality): for α:@@S, β={ S~A || A:α} ( α in closed_family(S) iff β in open_family(S))
Bourbaki's Abstract Model of x tends to x0. A filter is closed under finite intersections and supersetting
.Used_in Math.Topology.
[ math_91_Topology.html ]
- For S:Sets, filters(S)::={f:@(@S-{}) || for all B:@S(if for some A:f(A==>B) then B in f) and for all A,B:f ( A & B in f) },
- (above)|-for all G:finite(f) ( &(G) in f).
- For S:Sets, filter_bases(S)::={f:@(@S-{}) || for all A,B:f, some C:f(C==>A&B) },
- (above)|-for all f:filter_bases(S), A,B:f (A & B).
- (above)|-for all f:filter_bases(S) ({A:@S || for some B:f(B==>A)} in filter(S) ).
Every set in a filterbase has its own filterbase,...
- (above)|-for all f:filter_bases(S), F:f, {A&F || A:f} in filter_bases(F).
- For S:Sets, ultrafilters(S)::={f:filters(S) || for all A:@S(A in f or S~A in f) }.
. . . . . . . . . ( end of section Filters Bases) <<Contents | End>>
. . . . . . . . . ( end of section Filters) <<Contents | End>>
An abstract lattice has two operations that are idempotent and absorbative.
A set of sets is a lattice with respect to union and intersection iff every
union and intersection of every pair of sets in the family is also in the family.
This is the same as requiring that all finite intersections and unions are
members of the family.
A collection of sets is a complete lattice is all unions and intersections
of all sets of sets in the family are also in the family ... even with
infinite unions and interesections.
- generate(α)::=the smallest lattice of sets containing all elements of α.
A pair of sets in a complete lattice L form a bracket if the first is a
subset (or is equal to) the other:
- Bracket(L)::@(L><L)={ (B,T):L><L. B ==> T }.
Each Bracket (B,T) determines a sublattice { U:L. B==>U==>T } of L.
A rough set that approximates set Target in lattice L is the bracket (Lower,Upper) where
- Lower:= &{ X:L . Target ==> X},
- Upper:= |{ X:L . X ==>Target }.
rough_set[L](T) ::=(&{ X:L . Target ==> X}, |{ X:L . X ==>Target }).
- |-rough_set[L](T) in Bracket(L).
Given a map f from set X to Y, lattice(f) ::= generate(X/f).
Given maps a:X>->attributes (assumed normalized), b>->decisions,
- rough_sets(c,L)::= { rough_set(L)(c) || c: X/b }.
. . . . . . . . . ( end of section Lattices of Sets) <<Contents | End>>
. . . . . . . . . ( end of section Special types of Families) <<Contents | End>>
- For S:Sets, α:@@S, refinement(α )::={ β in @@S || for all B in β, some A in α (B==>A)}.
- For S:Sets, α,β:@@S, (β finer α ) ::=for all B in β, some A in α (B==>A).
. . . . . . . . . ( end of section Families of Sets/Hypergraphs) <<Contents | End>>
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 ]
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
- 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.