u盘raw
JOURNAL OF FORMALIZED MATHEMATICS
Volume Axiomatics,Relead1989,Published2001
Inst.of Computer Science,University of Bia l ystok
Tarski Grothendieck Set Theory
Andrzej Trybulec
Warsaw University
Bia l ystok
Summary.This is thefirst part of the axiomatics of the Mizar system.It includes the axioms of the Tarski Grothendieck t theory.They are:the axiom
stating that everything is a t,the extensionality axiom,the definitional axiom of
the singleton,the definitional axiom of the pair,the definitional axiom of the union
of a family of ts,the definitional axiom of the boolean(the power t)of a t,the
新闻稿范文300字九日杜甫regularity axiom,the definitional axiom of the ordered pair,the Tarski’s axiom A
introduced in[1](e also[2]),and the Frænkel scheme.Also,the definition of
equinumerosity is introduced.
MML Identifier:TARSKI.
WWW:mizar/JFM/Axiomatics/tarski.html
In this paper x,y,z,u,N,M,X,Y,Z denote ts.
The following proposition is true
(2)1If for every x holds x∈X iffx∈Y,then X=Y.
Let us consider y.The functor{y}is defined by:
(Def.1)x∈{y}iffx=y.
Let us consider z.The functor{y,z}is defined as follows:
板书设计模板
(Def.2)x∈{y,z}iffx=y or x=z.
Let us obrve that the functor{y,z}is commutative.
Let us consider X,Y.The predicate X⊆Y is defined as follows:
(Def.3)If x∈X,then x∈Y.
小学四年级上册数学
Let us note that the predicate X⊆Y is reflexive.
Let us consider X.The functor X is defined as follows:
(Def.4)x∈ X iffthere exists Y such that x∈Y and Y∈X.
The following proposition is true
(7)2If x∈X,then there exists Y such that Y∈X and it is not true that there exists
x such that x∈X and x∈Y.
往后余生的说说1The proposition(1)has been removed.点饥
2The propositions(3)–(6)have been removed.
1c Association of Mizar Urs
tarski grothendieck t theory2 The scheme Fraenkel deals with a t A and a binary predicate P,and states that: There exists X such that for every x holds x∈X iffthere exists y such that
y∈A and P[y,x]
provided the parameters meet the following condition:
•For all x,y,z such that P[x,y]and P[x,z]holds y=z.
Let us consider x,y.The functor x,y is defined as follows:
(Def.5) x,y ={{x,y},{x}}.
Let us consider X,Y.The predicate X≈Y is defined by the condition(Def.6). (Def.6)There exists Z such that
(i)for every x such that x∈X there exists y such that y∈Y and x,y ∈Z,
(ii)for every y such that y∈Y there exists x such that x∈X and x,y ∈Z,and (iii)for all x,y,z,u such that x,y ∈Z and z,u ∈Z holds x=z iffy=u.
The following proposition is true
(9)3There exists M such that
希望你不要介意(i)N∈M,
(ii)for all X,Y such that X∈M and Y⊆X holds Y∈M,
(iii)for every X such that X∈M there exists Z such that Z∈M and for every Y such that Y⊆X holds Y∈Z,and
(iv)for every X such that X⊆M holds X≈M or X∈M.
References
[1]Alfred Tarski.¨Uber Unerreichbare Kardinalzahlen.Fundamenta Mathematicae,30:176–183,1938.
[2]Alfred Tarski.On well-ordered subts of any t.Fundamenta Mathematicae,32:176–183,1939.
Received January1,1989
Published December9,2001
3The proposition(8)has been removed.
