Informatyka MIMUW

Iloczyn kartezjański i podobne konstrukcje

W definicji iloczynu kartezjańskiego (patrz Wykład 5: "Para uporządkowana, iloczyn kartezjański, relacje, domykanie relacji, relacja równoważności, rozkłady zbiorów" Definicja 2.1) jest pewna nieścisłość. Konstrukcja iloczynu kartezjańskiego odwołuje się do aksjomatu wyróżniania w wersji nieuprawomocnionej. Konstrukcja, którą zobaczą państwo w tym rozdziale, usuwa tę poprzednią niedogodność.

Twierdzenie 5.1.

Dla dowolnych dwóch zbiorów $\displaystyle x$ i $\displaystyle y$ istnieje zbiór $\displaystyle x\times y$ zawierający wszystkie pary postaci $\displaystyle (w,z)$, gdzie $\displaystyle w\in x$ i $\displaystyle z\in y$.

Dowód

Ustalmy dwa dowolne zbiory $\displaystyle x$ i $\displaystyle y$. Jeśli $\displaystyle x=\emptyset$ lub $\displaystyle y=\emptyset$, to $\displaystyle x\times y = \emptyset$ istnieje na podstawie aksjomatu zbioru pustego. W przeciwnym przypadku $\displaystyle x\cup y$ jest zbiorem jednoelementowym $\displaystyle \{z\}$, to $\displaystyle x\times y=\{\{\{z\}\}\}$ istnieje na podstawie aksjomatu pary. W dalszej części dowodu zakładamy, że zbiory $\displaystyle x$ i $\displaystyle y$ są niepuste i że $\displaystyle x\cup y$ ma więcej niż jeden element. Na podstawie aksjomatu zbioru potęgowego, aksjomatu unii i aksjomatu wycinania następujące zbiory istnieją:

$\displaystyle \begin{align*} A & =\{z\in\mathcal{P}(x)\,|\, \exists w\; z =\{w\}\}, \\ B & =\{z\in\mathcal{P}(x\cup y)\,|\, \exists w \exists v\; (w \neq v \land z=\{v,w\})\}, \\ C & =\{z\in\mathcal{P}(\mathcal{P}(y))\,|\, \exists v\; z=\{\{v\}\}=(v,v)\}. \end{align*}$

Nasze założenia gwarantują, że żaden z powyższych zbiorów nie jest pusty. Kontynuując, możemy stworzyć:

$\displaystyle \begin{align*} D_0 & =\{z\in\mathcal{P}(A\cup B)\,|\, \exists w \exists v\; w\neq v \land z=\{\{w\},\{w,v\}\}=(w,v)\}, \end{align*}$

w którym to zbiorze mamy pewność, że $\displaystyle w$ jest elementem $\displaystyle x$. Kontynuujemy, definiując:

$\displaystyle \begin{align*} D_0' & =\{z\in\mathcal{P}(D_0\cup C)\,|\, \exists w \exists v\; w\neq v \land z=\{(w,v),(v,v)\}\}, \end{align*}$

gdzie mamy pewność, że $\displaystyle w$ jest elementem $\displaystyle x$, a $\displaystyle v$ elementem $\displaystyle y$ oraz:

$\displaystyle \begin{align*} D_0'' & =\{z\in\mathcal{P}(D_0\cup C)\,|\, \exists w \exists v\; w\neq v \land z=\{(w,v),(w,w )\}\}, \end{align*}$

gdzie mamy pewność, że $\displaystyle w\in A\cap B$. Kończąc:

$\displaystyle \begin{align*} x\times y & =\{z\in\bigcup D_0' \,|\, \exists w \exists v\; w\neq v \land z=(w,v)\}\cup \{z\in\bigcup D_0'' \,|\, \exists w\; z=(w,w)\}. \end{align*}$

Twierdzenie 5.2.

Jeśli $\displaystyle x,y$ i $\displaystyle z$ są zbiorami i $\displaystyle z\subseteq x\times y$, to zbiorem jest również ogół $\displaystyle v$ takich, że istnieje $\displaystyle w$ spełniające $\displaystyle (v,w)\in z$. Zbiór takich $\displaystyle v$ oznaczamy przez $\displaystyle \pi_1(z)$ i nazywamy projekcją na pierwszą współrzędną.

Dowód

Zbiór $\displaystyle \pi_1(z)$ istnieje na podstawie aksjomatów ZF i jest równy:

$\displaystyle \pi_1(z) = \bigcup\{w\in\bigcup z\,|\, \exists u\; w=\{u\}\}.$

W tej chwili jesteśmy gotowi dowieść własność zapowiedzianą w Wykładzie 4 (patrz Wykład 4: "Teoria mnogości ZFC. Operacje na zbiorach"). Dla dowolnej formuły $\displaystyle \varphi'$ nieposiadającej zmiennych wolnych innych niż $\displaystyle z'$ i $\displaystyle x_1'$, następująca formuła jest prawdą:

$\displaystyle \forall x_1' \forall x' \exists y' \forall z'\; z'\in y' \iff (z'\in x' \land \varphi').$

Aby dowieść tę własność, ustalmy dowolną formułę $\displaystyle \varphi'$ i dowolny zbiór $\displaystyle x_1'$. Stosujemy aksjomat wyróżniania do $\displaystyle x=x\times \{x_1'\}$ (który istnieje na mocy Twierdzenia 5.1 i do formuły

$\displaystyle \exists z' \exists x_1'\; z=(z',x_1')\land\varphi',$

otrzymując zbiór $\displaystyle y$. Wymagany zbiór $\displaystyle y'$ istnieje na mocy Twierdzenia 5.2 i jest równy $\displaystyle \pi_1(y)$.

Przykładem zastosowania powyższego twierdzenia może być otrzymanie drugiej projekcji z iloczynu kartezjańskiego. Aby otrzymać $\displaystyle \pi_2(z)$, stosujemy powyższe twierdzenie do $\displaystyle x_1'=z$, $\displaystyle x=\bigcup\bigcup{z}$ i wyrażenia $\displaystyle \varphi'$ mówiącego $\displaystyle \exists w\; (w,z')\in x_1'$.