Tarski Grothendieck Set Theory (TG)

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
  

  pair		singleton		ordered 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