Schemat Aksjomatu Zastępowania

Schemat Aksjomatu Zastępowania


Kolejnym aksjomatem lub raczej schematem aksjomatu jest aksjomat zastępowania. Aksjomat ten, wraz z aksjomatem zbioru pustego, implikuje aksjomat wyróżniania i dlatego aksjomat wyróżniania jest często omijany w liście aksjomatów. Intuicyjna interpretacja tego aksjomatu jest następująca. Jeśli pewna własność, opisana formułą, ma cechy funkcji, to obrazem każdego zbioru, względem tej własności, jest również zbiór.

Aksjomat Zastępowania Dla dowolnej formuły \( \varphi \) nieposiadającej zmiennych wolnych innych niż \( w \) i \( v \) następująca formuła jest prawdą:

\( (\forall w \exists u \forall v\; \varphi \Longrightarrow u=v) \Longrightarrow (\forall x \exists y\forall v\; (v\in y \iff \exists w\; w\in x \land \varphi)) \)

Aksjomat zastępowania posiada specyficzną formę. Istnienie zbioru \( y \) jest zagwarantowane pod warunkiem, że formuła \( \varphi \) spełnia wymaganą własność. Formuła \( \varphi \) musi działać jak "funkcja częściowa", to znaczy, że jeśli jest spełniona dla zbiorów \( w,v \), to nie może być prawdą dla żadnych innych zbiorów \( w,v' \). Nieformalnie, formuła \( \varphi \) przyporządkowuje jednoznacznie pewnym zbiorom inne zbiory. Pod tym warunkiem istnieje zbiór bytów przyporządkowany bytom z danego zbioru \( x \). Zupełnie nieformalnie możemy stwierdzić, że dla zdefiniowanej formułą częściowej funkcji, jeśli jako dziedzinę weźmiemy dowolny zbiór \( x \), to przeciwdziedzina tej funkcji również jest zbiorem.

Aksjomat zastępowania nie był jednym z aksjomatów zaproponowanych przez Ernsta Zermelo. Został on dodany później przez Adolfa Abrahama Halevi Fraenkela i jest stosowany obecnie jako część aksjomatyki, którą nazywamy potocznie ZF. Pokażemy teraz, że aksjomat zastępowania implikuje aksjomat wyróżniania.

Rozpoczynając dowód, ustalamy \( x \) i \( \varphi \), do których chcielibyśmy zastosować aksjomat wyróżniania. Jedyną zmienną wolną w \( \varphi \) jest \( z \) i aksjomat wyróżniania gwarantuje istnienie zbioru \( y \) będącego podzbiorem \( x \) i składającego się dokładnie z tych elementów, dla których \( \varphi \) jest prawdą. Aby istnienie zbioru \( y \) zostało zagwarantowane przez aksjomat zastępowania, musimy zmienić formułę \( \varphi \). Nowa formuła \( \varphi' \) wygląda następująco

\( \exists z\; \varphi \land z=w=v. \)

Formuła \( \varphi' \) posiada dwie zmienne wolne \( w \) i \( v \) i spełnia warunek jednoznaczności, gdyż jeśli jest prawdą dla \( w \) i \( v \), to niewątpliwie \( w=v \). Co więcej formuła jest prawdą dla wyłącznie tych \( w=v \), dla których \( \varphi \) jest prawdą przy założeniu, że \( z=w=v \). Stosując aksjomat zastępowania dla tego samego \( x \), dla którego chcielibyśmy stosować aksjomat wyróżniania, otrzymujemy zbiór tych \( v \), dla których \( \varphi' \) jest prawdą dla pewnego \( w\in x \). Ale skoro tak, to \( w=z=v \) i \( \varphi \) jest prawdą dla \( z \), co dowodzi, że otrzymaliśmy dokładnie ten sam zbiór. Dowiedliśmy, że aksjomat zastępowania implikuje aksjomat wyróżniania.