Aksiomo de malplena aro

En aroteorio, la aksiomo de malplena aro estas aksiomo de aroteorio de Zermelo-Fraenkel (ZF), la fragmento de ĝenerala aroteorio, kaj de aroteorio de Kripke-Platek.

Formala deklaro

En la formala lingvo de la aksiomoj de Zermelo-Fraenkel, la aksiomo estas:

$\exists x\,\forall y\,\lnot (y\in x)$

aŭ en vortoj:

Ekzistas aro tia ke neniu aro estas membro de ĝi.

Interpreto

Oni povas uzi la aksiomon de ekstensionaleco por montri ke ekzistas nur unu malplena aro. Ĉar ĝi estas unika, oni povas nomi ĝin. Ĝi estas nomata kiel la malplena aro, skribata kiel { } aŭ ∅. La aksiomo, deklarita en natura lingvo, estas esence:

Malplena aro ekzistas.

La aksiomo de malplena aro estas ĝenerale konsiderata kiel nekontraŭdira, kaj ĝi aŭ ĝia ekvivalento aperas en praktike ĉiu alternativa aksiomatigado de aroteorio.

En kelkaj formuliĝoj de ZF, la aksiomo de malplena aro estas fakte ripetata en la aksiomo de malfinio. Tamen, ekzistas aliaj formuliĝoj de ĉi tiu aksiomo kiu ne antaŭsupozas la ekziston de malplena aro. La aksiomoj de ZF ankaŭ povas esti skribataj uzante konstantan simbolon prezentantan la malplenan aron; tiam la aksiomo de malfinio uzas ĉi tiun simbolon sen postulo ki ĝi estas malplena, kaj la aksiomo de malplena aro estas necesa por deklari ke ĝi estas fakte malplena.

Krome, oni foje pripensas aroteoriojn en kiuj ne ekzistas malfinuaj aroj, kaj tiam la aksiomo de malplena aro daŭre povas esti bezonata. Tiel, ĉiu aksiomo de aroteorio aŭ logiko kiu implicas ekziston de iu aro implicas ekziston de la malplena aro, se oni havas la aksioman skemon de apartigo. Ĉi tio estas vera, ĉar la malplena aro estas subaro de iu aro konsistanta el tiuj elementoj kiuj kontentigas malkongruan formulon.

En multaj formuliĝoj de unua orda predikata logiko, la ekzisto de almenaŭ unu objekto ĉiam estas garantiita. Se la aksiomatigo de aroteorio estas formulita en ĉi tia logika sistemo kun la aksioma skemo de apartigo kiel aksiomoj, tiam la ekzisto de la malplena aro estas teoremo.

Se apartigo ne estas postulata kiel aksioma skemo, sed venas kiel teorema skemo de la skemo de anstataŭo (kiel estas iam farite), la situacio estas pli komplika, kaj dependas de la preciza formuliĝo de la anstataŭa skemo. La formuliĝo uzata en la artikolo aksioma skemo de anstataŭo nur permesas konstrui la bildon F[a] se a estas enhavata en la domajno de la klasa funkcio F; tiam la derivaĵo de apartigo postulas la aksiomon de malplena aro. Aliflanke, la limo de tutaĵo de F ofte estas forigita de la anstataŭa skemo, en kiu okazo ĝi implicas la apartigan skemon sen uzo de la aksiomo de malplena aro (aŭ ajna alia aksiomo por ĉi tio).