Tarski Grothendieck Set Theory (TG)

Mizar article:
MML IdtitleauthorsFMabstractsfull article
tarski Tarski Grothendieck Set Theory Andrzej Trybulec FM abstracts: jfm (old), plain text, gab. full article: plain text, linked

TG includes the following axioms: Set Axiom, Extensionality Axiom, Axiom of pair, Axiom of union, Axiom of regularity, Fraenkel scheme, and Tarski Axiom A.

Some consequences: Axiom schema of separation, Axiom of power set, Axiom of infinity, Axiom of induction, Axiom of choice.

Mizar has three properties which work together with TG:

  • non-emptiness of Mizar types and type choice functor
  • permissive definitions
    for x1 being T1,...,xn being Tn of x1,...,x(n-1) st P[x1,...,xn] holds
    (ex y being T of x1,...,xn st Q[x1,...,xn,y]) &
    (for y1,y2 being T of x1,...,xn st Q[x1,...,xn,y1] & Q[x1,...,xn,y2] holds y1 = y2)
    ex F st for x1 being T1,...,xn being Tn of x1,...,x(n-1) holds
    F(x1,...,xn) is T of x1,...,xn &
    for y being T st P[x1,...,xn] holds y = F(x1,...,xn) iff Q[x1,...,xn,y]
  • special treatment of equality
    x = y implies F(x) = F(y) & (P[x] iff P[y])

Axioms

  • Set axiom: Everything is a set.

    There is no direct formulation of the axiom in MML but the axiom is guaranteed in the Mizar system by the fact that every Mizar type is a subtype of the set type. In the result, any quantified variable ranges over set.

    Exisence of a set is the result of the fact that Mizar types are non empty, so set type is non empty too.

    Historical note: First formulation of foundations of the MML (1989) included two types: set and Any and the Set axiom was stated directly (see Tarski Grothendieck Set Theory by Andrzej Trybulec, FM1(1):9-11, 1990):

    
        reserve x for Any;
    
        axiom :: TARSKI:1
          x is set;
    

  • Extensionality axiom: Two sets are equal if they have the same members.

    axiom :: TARSKI:2
    for X, Y being set
          st for x being set holds
               x in X iff x in Y
       holds X = Y
  • Axiom of pair: For any two sets there exists a set whose members are exactly the two sets.

    There is no direct formulation of the axiom in MML like

    reserve a,x,y,z for set;
    
    for x,y ex z st for a holds a in z iff a = x or a = y;
        
    but there are definitions which are consequences of Axiom of pair, Extensionality axiom, and logical laws
    pairsingletonordered pair
    definition
      let x, y be set;
      func {x, y} -> set means
    :: TARSKI:def 2
        for z being set holds
           z in it iff z = x or z = y;
      commutativity;
    ::  for x, y being set holds
    ::  {x,y} = {y,x};
    end;
    definition
      let x be set;
      func {x} -> set means
    :: TARSKI:def 1
        for z being set holds
           z in it iff z = x;
    end;
    definition
      let x, y be set;
      func [x, y] -> set equals
    :: TARSKI:def 5
        {{x,y},{x}};
    end;
    Existence of {x, y} is consequence of Axiom of pair; uniqueness of {x, y} -- Extensionality axiom; commutativity of {x, y} -- commutativity of disjunction.
    Existence of {x} is consequence of Axiom of pair and idempotence of disjunction ("a = x or a = x" is equivalent to "a = x"); uniqueness of {x} -- Extensionality axiom.
    The ordered pair [x, y] = {{x, y}, {x}} according to the standard Kuratowski definition.

  • Axiom of union: For any set X there is a set whose elements are precisely the elements of the elements of X.

    There is no direct formulation of the axiom in MML like

    reserve x,X,Y,Z for set;
    
    for X ex Z st for x holds x in Z iff ex Y st x in Y & Y in X;
        
    but there is a definition which is consequences of Axiom of union and Extensionality axiom
    definition
      let X be set;
      func union X -> set means
    :: TARSKI:def 4
        for x being set holds
              x in it
           iff
              ex Y being set st x in Y & Y in X;
    end;

  • Axiom of regularity: Every non empty set has a member which has no common elements with the set.

    axiom :: TARSKI:7
    for x, X being set st x in X
       ex y being set st
          y in X &
           (for z being set st z in X
              holds not z in y)

    Consequences: Asymmetry (then also irreflexivity) of "in". No set is a member of itself, and circular chains of membership are impossible (see ORDINAL1:3, ORDINAL1:4, ORDINAL1:5, ORDINAL1:6).

  • Fraenkel's scheme: Let the binary predicate P constitute a function. Then the image of the set A through P exists..

    scheme TARSKI:sch 1
    {A -> set}:
    ex x being set st
       for y being set holds
             y in x
          iff
             ex z being set st z in A() & P[z, y]
    provided
       for x, y, z being set st P[x, y] & P[x, z]
          holds y = z;

    This is the axiom schema of replacement of ZFC. It implies the axiom schema of separation, XBOOLE_0:sch 1.

  • Tarski's axiom A: It was proposed by Alfred Tarski in On Well-ordered Subsets of any Set, Fundamenta Mathematicae, vol.32 (1939), pp. 176-183.

    For every set N there exists a system M of sets which satisfies the following conditions:

    1. N in M
    2. if X in M and Y c= X, then Y in M
    3. if X in M and Z is the system of all subsets of X, then Z in M
    4. if X c= M and X and M do not have the same potency, then X in M.

    axiom :: TARSKI:9
    for N being set
       ex M being set st
          N in M &
           (for x, y being set st x in M & y c= x
              holds y in M) &
           (for x being set st x in M
              ex y being set st
                 y in M &
                  (for z being set st z c= x
                     holds z in y)) &
           (for x being set st x c= M & not x,M are_equipotent
              holds x in M)

    Tarski's axiom implies the axioms of power set, infinity and choice and existence of inaccessible cardinals.

    • The axiom of power set, definition of bool.
    • The axiom of infinity is proved in more general form in theorem ORDINAL:51 (due to ORDINAL:41). The theorem is later used to show existence of omega, the smallest set satisfying Axiom of infinity.
    • The axiom of choice is proved as theorem WELLORD2:27 and the proof involves consequences of Axiom A. However, Axiom of choice may be proved in Mizar without Axiom A.
      
        definition
          let X be set;
          assume A: contradiction; :: permissive assumption
          func choose X -> Element of X means not contradiction;
          existence by A;
          uniqueness by A;
        end;
      
        now
          let M be non empty with_non-empty_elements set;
          deffunc F(set) = choose $1;
      
          consider Choice being Function such that
      A1: dom Choice = M and
      A2: for X being set st X in M holds Choice.X = F(X) from FUNCT_1:sch 3;
      
          take Choice;
          :: Choice is a choice function
          let X be set such that
      A3: X in M;
      A4: Choice.X = choose X by A2,A3;
      A5: X <> {} by A3,SETFAM_1:def 9;
          thus Choice.X in X by A4,A5,SUBSET_1:def 2;
        end;
      
      Or, even shorter with the type choice functor:
        now
          let M be non empty with_non-empty_elements set;
          deffunc F(set) = the Element of $1;
      
          consider Choice being Function such that
      A1: dom Choice = M and
      A2: for X being set st X in M holds Choice.X = F(X) from FUNCT_1:sch 3;
      
          take Choice;
          :: Choice is a choice function
          let X be set such that
      A3: X in M;
      A4: Choice.X = the Element of X by A2,A3;
      A5: X <> {} by A3,SETFAM_1:def 9;
          thus Choice.X in X by A4,A5,SUBSET_1:def 2;
        end;
      
      

Discussion

TG in article TARSKI is given in not consistent way: mixture of axioms and definitions (which include axioms). Pure way may be obtained by dividing article TARSKI as follows (by the way, provable properties of "=" and "in" may be removed from HIDDEN; we leave: x = y implies (P[x] iff P[y])).

HIDDEN

definition
  mode set;
end;

definition let x,y be set;
  pred x = y;
:: NO reflexivity and symmetry
end;

notation let x,y be set;
  antonym x <> y for x = y;
end;

definition let x,X be set;
  pred x in X;
:: NO asymmetry
end;

TARSKI_0

environ
begin

reserve x,y,z,X,Y,Z for set;

:: Set axiom (redundant but what)
axiom
 x is set;

:: Extensionality axiom
axiom
  (for x holds x in X iff x in Y) implies X = Y;

:: Axiom of pair
axiom
  for x,y ex z st for a holds a in z iff a = x or a = z;

:: Axiom of union
axiom
  for X ex Z st for x holds x in Z iff ex Y st x in Y & Y in X;

:: Axiom of regularity
axiom
  x in X implies ex Y st Y in X & not ex x st x in X & x in Y;

:: Fraenkel's scheme
axiom scheme { A()-> set, P[set, set] }:
  ex X st for x holds x in X iff ex y st y in A() & P[y,x]
 provided
  for x,y,z st P[x,y] & P[x,z] holds y = z;

TARSKI_1

environ
 vocabulary TARSKI;
 axioms TARSKI_0;  :: "theorems" directive does not fit
begin

definition
  let x,y be set;
  redefine pred x = y;
  reflexivity
  proof
    let a be set;
A0: for b being set holds b in a iff b in a;
    thus thesis by A0,TARSKI_0:2;
  end;
  symmetry
  proof
    let a,b be set such that
A1: a = b;
A2: for c being set holds c in b iff c in a by A1;
    thus b = a by A2,TARSKI_0:2;
  end;
end;

definition
  let x,y be set;
  func {x, y} means:
Pair:
  for z being set holds z in it iff z = x or z = y;
  existence by TARSKI_0:3;
  uniqueness
  proof
    let X1,X2 be set such that
A1: for z being set holds z in X1 iff z = x or z = y and
A2: for z being set holds z in X2 iff z = x or z = y;
A3: now
      let z be set;
B1:   z in X1 iff z = x or z = y by A1;
      thus z in X1 iff z in X2 by A2,B1;
    end;
    thus X1 = X2 by A3,TARSKI:2;
  end;
end;

definition
  let x be set;
  func {x} means:
Singleton:
  for z being set holds z in it iff z = x;
  existence
  proof
    consider X being set such that
A1: for z being set holds z in X iff z = x or z = x by TARSKI_0:3;
    take X;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let X1,X2 be set such that
A1: for z being set holds z in X1 iff z = x and
A2: for z being set holds z in X2 iff z = x;
A3: now
      let z be set;
B1:   z in X1 iff z = x by A1;
      thus z in X1 iff z in X2 by A2,B1;
    end;
    thus X1 = X2 by A3,TARSKI:2;
  end;
end;

definition
  let x,y be set;
  func [x, y] equals {{x}, {x, y}};
  coherence;
end;

definition
  let x,y be set;
  redefine pred x in y;
  asymmetry
  proof
    let a,b be set such that
A1: a in b and
A2: b in a;
    set X = {a,b};
A3: a in X by Pair;
    consider Y being set such that
A4: Y in X & not ex x being set st x in X & x in Y by A3,TARSKI_0:5;
A5: Y = a or Y = b by A4,Pair;
    thus contradiction by A1,A2,A4,A5;
  end;
end;

definition
  let x,y be set;
  pred x c= y means
  for z being set st z in x holds z in y;
  reflexivity
  proof
    let a,z be set;
    thus z in a implies z in a;
  end;
end;

reserve X,Y,Z,x,y,z,u for set;

definition
  let X,Y;
  pred X,Y are_equipotent means
    ex Z st
       (for x st x in X ex y st y in Y & [x,y] in Z) &
       (for y st y in Y ex x st x in X & [x,y] in Z) &
        for x,y,z,u st [x,y] in Z & [z,u] in Z holds x = z iff y = u;
end;

TARSKI_A

environ
 vocabulary TARSKI;
 notations TARSKI_1;
 constructors TARSKI_1;
begin

axiom
  ex M st N in M &
     (for X,Y holds X in M & Y c= X implies Y in M) &
     (for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z) &
     (for X holds X c= M implies X,M are_equipotent or X in M);

-- GrzegorzBancerek - 2009-07-23

WebForm
TopicClassification Select one...
ProjectGroup?

ImplementationDate? N/A
Topic revision: r2 - 2009-07-23 - 15:37:36 - GrzegorzBancerek
 
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback