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.

$\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\forall }z(z\in x\iff 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.

$\mathrm{\forall }x[\mathrm{\exists }y(y\in x)\Rightarrow \mathrm{\exists }y(y\in x\wedge \mathrm{\neg }\mathrm{\exists }z(z\in y\wedge z\in x))]$

3) Gwireb wahanu: Os yw z yn set a $\varphi$ 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 $\varphi$ yn iaith ZFC gyda newidynnau rhydd ymysg $x,z,w_1,\dots ,w_n$:

$\mathrm{\forall }z\mathrm{\forall }{w}_1\dots w_n\mathrm{\exists }y\mathrm{\forall }x(x\in y\iff (x\in z\wedge \varphi ))$

4) Gwireb bario: Os yw x ac y yn setiau, yna mae yna set sy'n cynnwys y ddwy ohonynt.

$\mathrm{\forall }x\mathrm{\forall }y\mathrm{\exists }z(x\in z\wedge y\in z)$

5) Gwireb uniad: I bob set $ℱ$ mae yna set A sy'n cynnwys pob set sy'n aelod o set sy'n aelod o $ℱ$.

$\mathrm{\forall }ℱ\mathrm{\exists }A\mathrm{\forall }Y\mathrm{\forall }x(x\in Y\wedge Y\in ℱ\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 $\varphi$ yn iaith ZFC gyda'i newidynnau rhydd ymysg $x,y,A,w_1,\dots ,w_n$:

$\mathrm{\forall }A\mathrm{\forall }{w}_1,\dots ,w_n[(\mathrm{\forall }x\in A\mathrm{\exists }!y\varphi )\Rightarrow \mathrm{\exists }Y\mathrm{\forall }x\in A\mathrm{\exists }y\in Y\varphi ].$

Ystyr y meintiolydd $\mathrm{\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.

$\mathrm{\exists }X(\varnothing \in X\wedge \mathrm{\forall }y(y\in X\Rightarrow S(y)\in X))$

8) Gwireb set-pŵer: I bob set x mae yna set y sy'n cynnwys pob is-set o x.

$\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(z\subseteq x\Rightarrow z\in y)$

Mae $z\subseteq x$ yn dalfyriad o $\mathrm{\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.

$\mathrm{\forall }X\mathrm{\exists }R(R\text{well-orders}X)$

Gweler hefyd

• Gwireb