Logika i teoria mnogości/Wykład 5.2

From Studia Informatyczne

[Edytuj]

Iloczyn kartezjański i podobne konstrukcje

Dla zainteresowanych

W definicji iloczynu kartezjańskiego (patrz 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 \aligned 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)\}. \endaligned

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

\displaystyle \aligned D_0 &=\{z\in\mathcal{P}(A\cup B)\,|\, \exists w \exists v\; w\neq v \land z=\{\{w\},\{w,v\}\}=(w,v)\}, \endaligned

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

\displaystyle \aligned D_0' &=\{z\in\mathcal{P}(D_0\cup C)\,|\, \exists w \exists v\; w\neq v \land z=\{(w,v),(v,v)\}\}, \endaligned

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

\displaystyle \aligned D_0'' &=\{z\in\mathcal{P}(D_0\cup C)\,|\, \exists w \exists v\; w\neq v \land z=\{(w,v),(w,w )\}\}, \endaligned

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

\displaystyle \aligned 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)\}. \endaligned

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). 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 (patrz twierdzenie 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 (patrz twierdzenie 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'.

Źródło: "http://wazniak.mimuw.edu.pl/index.php?title=Logika_i_teoria_mnogo%C5%9Bci/Wyk%C5%82ad_5.2"