Damcaniaeth setiau wirebol
Oddi ar Wicipedia
Mewn mathemateg, disgrifiad trylwyr o ddamcaniaeth setiau yw damcaniaeth setiau wirebol. Fe'i grëwyd er mwyn mynd i'r afael a'r croesddywediadau megis croesddywediad Russel a chroesddywediad Burali-Forti, a oedd yn ran annatod o ddamcaniaeth setiau fel y'i datblygwyd gan Frege ac eraill. Mae sawl system wirebol posib i ddamcaniaeth setiau, ond system Zermelo-Fraenkel gyda Gwireb Ddewis yw'r fwyaf poblogaidd o lawer ymysg mathemategwyr.
[golygu] Gwirebau ZF
Strwythur dros resymeg radd-gyntaf yw damcaniaeth setiau Zermelo-Fraenkel. Setiau yw aelodau'r strwythur, a hafaledd a'r perthynas o aelodaeth yw'r perthynasau arno.
1) Gwireb estyniad: Mae dwy set yn hafal os yw'r un aelodau ganddynt.
2) Gwireb sylfaen: Mae gan bob set x nad yw'n wag aelod y fel fod x ac y yn setiau digyswllt.
3) Gwireb wahanu: Os yw z yn set a
yn unrhyw briodwedd a all aelodau x o z gael, yna mae yna is-set y o z sy'n cynnwys yr x hynny yn z sydd ganddynt y priodwedd, a dim arall. Mae'r cyfyngiad i z yn angenrheidiol er mwyn osgoi gwrthddywediad Russel. Noder mai cyfres o wirebau yw hon, a bod yn fanwl gywir.
Ar gyfer unrhyw fformwla
yn iaith ZFC gyda newidynnau rhydd ymysg
:
4) Gwireb bario: Os yw x ac y yn setiau, yna mae yna set sy'n cynnwys y ddwy ohonynt.
5) Gwireb uniad: I bob set
mae yna set A sy'n cynnwys pob set sy'n aelod o set sy'n aelod o
.
6) Gwireb ail-osod: Ar gyfer pob ffwythiant ffurfiol f a'i barth yn set, mae yna set sy'n cynnwys amrediad f (namyn un amod i osgoi wrthddywediad). Cyfres o wirebau ydyw hon hefyd. Ar gyfer pob fformwla
yn iaith ZFC gyda'i newidynnau rhydd ymysg
:
Ystyr y meintiolydd
yw fod
o'r fath yn bodoli, a'i bod yn unigryw namyn hafaledd.
Defnyddia'r gwirebau canlynol y nodiant
. Gellid profi o'r gwirebau uchod fod
yn bodoli a'i bod yn unigryw ar gyfer pob set
. Os mae yna set yn bodoli o gwbl, maent hefyd yn ymhlygu fod y set wag
yn bodoli a'i bod yn unigryw.
7) Gwireb anfeidredd: Mae yna set X sy'n cynnwys y set wag, a phrydbynnag mae y 'n aelod o X, mae S(y) hefyd yn aelod o X.
8) Gwireb set-pŵer: I bob set x mae yna set y sy'n cynnwys pob is-set o x.
Mae
yn dalfyriad o
.
9) Gwireb ddewis: I bob set X mae yna berthynas deuol R sy'n iawn-drefnu X. Golyga hyn fod R yn drefn llinol ar X a bod elfen lleiaf dan R gan bob is-set an-wag o X.
Eginyn erthygl sydd uchod. Gallwch helpu Wicipedia drwy ychwanegu ato.

![\forall x [ \exists y ( y \in x) \Rightarrow \exists y ( y \in x \land \lnot \exists z (z \in y \land z \in x))]](../../../../math/0/c/b/0cba16308b16641ddf69b8825cffce4c.png)



![\forall A\,\forall w_1,\ldots,w_n [ ( \forall x \in A \exists ! y \phi ) \Rightarrow \exists Y \forall x \in A \exists y \in Y \phi].](../../../../math/9/5/d/95d13b10b011f3aef56bc31492613a8e.png)




