MML Id  title  authors  FM  abstracts  full 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:
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):911, 1990):
reserve x for Any; axiom :: TARSKI:1 x is set;
axiom :: TARSKI:2 for X, Y being set st for x being set holds x in X iff x in Y holds X = Y 
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; 
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 :: 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) 
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.
For every set N there exists a system M of sets which satisfies the following conditions:
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.
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_nonempty_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_nonempty_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;
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])).
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;
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;
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;
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  20090723
WebForm  

TopicClassification  Select one... 
ProjectGroup? 

ImplementationDate?  N/A 