[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci ] / [R J Botting] / [ MATHS ] / logic_32_Set_Theory
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Sep 18 15:18:03 PDT 2007


    Theories of Sets


      This page is for worriers, hard core set theorists, logicians, and meta-mathematicians. I expect that practitioners will not need this information.

      For an introduction to set theory from the point of view of a computer professional using ASCII see [ intro_sets.html ] , For the traditional notation see [ sets.html ]

      Modeling sets by maps

      1. Sets can be modeled as maps from T into @={true,false}.
      2. @T::= @^T,...
      3. The $ schema notation reflects this model. {x:T||W(x)}::@^T= map[ x:T](W(x)), for A:@^T, x:T, x in A ::@= A(x),

      4. |-{x:T || W(x)}=the [f:@^T](for all x:T(f(x)=W(x)))=map[x:T](W(x)),


      The purpose of recording the above is to point out that if you allow the idea of a mapping or function then you also allow the set of functions/mappings that will have the properties of sets.

      Zermelo-Fraenkel Axiomatic Set Theory vs MATHs Sets


        These notes are for people interested in the theory of MATHS. It is of little practical import and is not referred to in manuals other than a reference in Logic.30 Sets" [ THEORY in logic_30_Sets ]

        Some ZF axioms can not be expressed in correctly in MATHS. The MATHS system disallows some of the more infinite constructions. We can however use MATH to talk about the ZF language by encapsulating its statements:

      1. name::=ZF(ZF notation).

      2. ZF_axioms::=
        1. Extensionality::=ZF(for all x,y( for all z( z in x iff z in y ) iff x = y).
        2. Null_set::=ZF( for some x, all y (not y in x) ).
        3. Unordered_pairs::=ZF( for all x,y, some z, all w( w in z iff (w=x or w=y) ).
        4. Sum_set::= ZF(for all x, some y, all z( z in y iff for some t(z in t and t in x)) ).
        5. Infinity::=ZF(for some x ( {} in x and for all y( if y in x then y | { y } in x ) ).
        6. Replacement::=ZF(for all t1,...( if for all x, one y (A(x,y,t1,...)) then for all u, some v (B(u,v)) ) where
          B(u,v) := ZF( for all r ( r in v iff for some s( s in u and A(s,r,t1,...) )).
        7. Power_set::=ZF( for all x, some y, all z(z in y iff z ==> x).
        8. Choice::=ZF(for all x, A, if (for all y, if y in x then not A(y)={}) then for some f ( for all y, if y in x then f(y) in A(y)) ).
        9. Regularity::=ZF( For all x, some y( x={} or ( y in x and for all z( if z in x then not z in y))) ).
          This last is how ZF prohibits formulas like x in x.
        10. The above comes from a figure from the following paper - and correcting several typographical errors: .Reference Cohen & Hersh 67, Paul J Cohen & Reuben Hersh, Non-Cantorian Set Theory, Scientific American Dec 1967.


        Notice that the above net merely labels the formulas without actually asserting any of them.

        Some of these can be mapped into theorems, one can not be expressed, and one becomes a meta_linguistic definition.

        With T, T1,T2,... as generic types, the following are theorems in MATHS:

      3. (above)|- (Extensionality): for all A,B:@T( A=B iff for all x:T( x in A iff x in B)).
      4. (above)|- (Null_set): for all y:T (not y in {}).
      5. (above)|- (Unordered_pairs): for all x,y,w:T,( w in {x,y} iff (w=x or w=y) `).
      6. (above)|- (Sum_set): for all X:@@T, z:T ( z in |X iff for some t:X(z in t)) `).
      7. (above)|- (Power_set): for all X:@T, all z (z in @X iff z ==> x).
      8. (above)|- (Choice): for all X:@T, g:X->non_null@T, some f:X->T, for all y:X (f(y) in g(y)).
      9. (above)|- (Regularity): for all B:@T, A:@B (A|(B~A) = B )

        The ZF Axiom of Replacement is equivalent to the definition of (above) |-{ f(x) || x:T1(W(x) ) } ::= {y:T2 || for some x:T1( W(x) and y=f(x) ) for any f:T1->T2, x:a list of variables and W(x) : any well formed formula in these variables.

        The ZF Axiom of Infinity can not be expressed in standard MATHs because it requires the existence of a set that has elements that are both in a type and subsets of a type. It is therefore not possible to tell what is the type of the elements in the set. This destroys a key requirement for the language of MATHS - that all elements of a set are of the same type.

        The meta_level construct of co-product (or multi-verse) lets form a mixture of different types of elements by tagging them with the names of the types. For example if M=\/{ T1, T2, ... , T[n] } then for all m:M, there is a unique t:{ T1, T2, ... , T[n] } and an x:t such that m=x.t. For each m this t is symbolized as type(m). These allow us to define mixed universes like

      10. M::=\/{ T, @T }. Now it follows that all though there are elements of M whose untagged forms are in @T and also there are elements of M whose untagged forms are in T. But no element of M, after untagging, is in both... but only any element that is in both T and @T is legally placed on either side of ∈. So no element of M can be used to make M in M well typed. Even so definitions like this:
      11. ILLEGAL::="S::= \/{ T, @S}" are forbidden to be sure of avoiding any paradoxes arising from them.

        But see Plotkin Power domains.

      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

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


    3. 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).
    4. given::reason="I've been told that...", used to describe a problem.
    5. given::variable="I'll be given a value or object like this...", used to describe a problem.
    6. goal::theorem="The result I'm trying to prove right now".
    7. goal::variable="The value or object I'm trying to find or construct".
    8. 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.
    9. hyp::reason="I assumed this in my last Let/Case/Po/...".
    10. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
    11. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
    12. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.