Damcaniaeth setiau wirebol

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 rhan 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.

## 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.
:\forall x \forall y ( \forall z (z \in x \Leftrightarrow z \in y)
\Rightarrow x = y)

2) Gwireb sylfaen: Mae gan bob set *x* nad yw'n wag aelod *y* fel fod *x* ac *y* yn setiau digyswllt.
:\forall x [ \exists y ( y \in x) \Rightarrow \exists y ( y \in x \land \lnot \exists z (z \in y \land z \in x))]

3) Gwireb wahanu: Os yw *z* yn set a \phi\! 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 \phi\! yn iaith ZFC gyda newidynnau rhydd ymysg x,z,w_1,\ldots,w_n\!:
:\forall z \forall w_1 \ldots w_n \exists y \forall x (x \in y \Leftrightarrow ( x \in z \land \phi ) )

4) Gwireb bario: Os yw *x* ac *y* yn setiau, yna mae yna set sy'n cynnwys y ddwy ohonynt.
:\forall x \forall y \exist z (x \in z \land y \in z)

5) Gwireb uniad: I bob set \mathcal{F} mae yna set *A* sy'n cynnwys pob set sy'n aelod o set sy'n aelod o \mathcal{F}.
:\forall \mathcal{F} \,\exists A \, \forall Y\, \forall x (x \in Y \land Y \in \mathcal{F} \Rightarrow x \in A)

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 \phi \! yn iaith ZFC gyda'i newidynnau rhydd ymysg x,y,A,w_1,\ldots,w_n \!:
:\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].
Ystyr y meintiolydd \exists ! y yw fod y\! o'r fath yn bodoli, a'i bod yn unigryw namyn hafaledd.

Defnyddia'r gwirebau canlynol y nodiant S(x) = x \cup \{x\} \!.
Gellid profi o'r gwirebau uchod fod S(x)\! yn bodoli a'i bod yn unigryw ar gyfer pob set x\!. Os mae yna set yn bodoli o gwbl, maent hefyd yn ymhlygu fod y set wag \varnothing 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*.
:\exist X \left (\varnothing \in X \land \forall y (y \in X \Rightarrow S(y)  \in X)\right )

8) Gwireb set-pŵer: I bob set *x* mae yna set *y* sy'n cynnwys pob is-set o *x*.
:\forall x \exists y  \forall z (z \subseteq x \Rightarrow z \in y)
Mae z \subseteq x yn dalfyriad o \forall q (q \in z \Rightarrow q \in x).

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*.
:\forall X \exists R ( R \;\mbox{well-orders}\; X)

## Gweler hefyd 
* Gwireb

Gwirebol
Categori:Sylfeini mathemateg