Aksjomatyczna teoria mnogości Zermelo-Fraenkla (ZF)
1. Definicja języka
Z pojęć pozalogicznych mamy tylko jeden predykat dwuargumentowy: ∈, „jest elementem”.
2 rodzaje wyrażeń:
Wyrażenia nazwowe (termy, nazwy, nazwy indywiduowe, indywidua).
Wyrażenia zdaniowe (zdania, formuły).
V = {x0, x1, x2, ... } - zbiór zmiennych indywiduowych (przeliczalny, zawierający wszystkie termy)
Definicja zbioru formuł (wskazujemy dopuszczalne konstrukcje)
Formuły atomowe
Formuły atomowe są to dowolne wyrażenia postaci x∈y oraz x = y, gdzie x, y ∈ V. Identyczność traktujemy jako predykat logiczny.
Przykłady formuł atomowych - x0∈x0, x17∈x3, x5 = x1.
Rekurencyjna (indukcyjna) definicja zbioru formuł.
Formułami ZF są wszystkie formuły atomowe oraz dodatkowo:
(1) jeśli φ jest formułą ZF, to ~ φ też jest formułą ZF.
(2) jeśli φ i ψ są formułami ZF, to (φ ⇒ ψ) też jest formułą ZF.
(3) jeśli φ jest formułą ZF oraz x jest zmienną (x∈V), to ∀x φ też jest formułą ZF.
Tworzenie formuł złożonych z formuł prostych.
x = y nie jest formułą atomową, ale x = y, gdzie x, y ∈ V, jest formułą atomową (ciągiem symboli).
Podajemy syntaktyczne warunki tworzenia formuł jako ciągów symboli, którym na razie nie przypisujemy żadnego znaczenia.
Definiując formuły, używamy symbolu ∈ - symbol języka definiowanego, którego nie musimy rozumieć. Używamy w języku, który definiujemy. Użyty jako symbol naszego języka, który rozumiemy.
3. Wyróżnienie zbioru zdań (formuł bez zmiennych wolnych)
Frm - zbiór wszystkich formuł teorii ZF
ZW(φ) - zbiór zmiennych wolnych formuły φ
Dla formuł atomowych:
ZW(x∈y) = {x, y},
ZW(x = y) = {x, y} dla x, y∈V.
Definicja indukcyjna funkcji określonej na zbiorze formuł, przyporządkowującej tym formułom zbiór ich zmiennych wolnych.
Warunki indukcyjne:
(1) ZW(~ φ) = ZW(φ)
(2) ZW((φ ⇒ ψ)) = ZW(φ) ∪ ZW(ψ)
(3) ZW(∀x φ) = ZW(φ) - {x}, dla φ, ψ ∈ Frm, x∈V.
F - zbiór zdań ZF, czyli formuł bez zmiennych wolnych.
F = {φ∈Frm: ZW(φ) = ∅}
Konwencje notacyjne
Piszemy:
1. (φ ∧ ψ) zamiast ~ (φ ⇒ ~ ψ)
2. (φ ∨ ψ) zamiast (~ φ ⇒ ψ)
3. (φ ⇔ ψ) zamiast ((φ ⇒ ψ) ∧ (ψ ⇒ φ))
4. ∃x φ zamiast ~ ∀x ~ φ
5. t ≠ t' zamiast ~ t = t'
6. t∉t' zamiast ~ t∈t'
(skróty notacyjne nie są wyrażeniami języka)
(…)
…)
3. (φ ⇔ ψ) zamiast ((φ ⇒ ψ) ∧ (ψ ⇒ φ))
4. ∃x φ zamiast ~ ∀x ~ φ
5. t ≠ t' zamiast ~ t = t'
6. t∉t' zamiast ~ t∈t'
(skróty notacyjne nie są wyrażeniami języka)
Aks - zbiór aksjomatów ZF
Aks F Frm
4. Wyróżnienie aksjomatów
(ZF0) (Aksjomat ekstensjonalności)
∀x ∀y [x = y ⇔ ∀z (z∈x ⇔ z∈y)]
(ZF1) (Aksjomat istnienia zbioru pustego)
∃x ∀y ~ y∈x
(ZF2) (Aksjomat istnienia pary nieuporządkowanej)
∀x ∀y…
… zbioru pustego - ∅
∀x (x = ∅ ⇔df ∀y y∉x)
Istnienie
∃x ∀y ~ y∈x (aksjomat ZF1).
Jednoznaczność
∀x ∀x' [(∀y y∉x ∧ ∀y y∉x') ⇒ x = x']
Dowód. Niech x, x' takie, że
(1) ∀y y∉x, (2) ∀y y∉x'. Na mocy ZF0 możemy zastosować schemat dowodzenia identyczności zbiorów.
(⊆)
1. z∈x (zał.)
2. z∉x (zał. 1)
3. z∉x ∨ z∈x' (DA, 2.)
4. z∈x' (OA, 1., 3.)
(⊇)
1. z∈x' (zał.)
2. z∉x' (zał. 1)
3. z∉x' ∨ z∈x (DA, 2.)
4. z∈x (OA, 1., 3.)
Zatem x = x'. □
Zatem definicja zbioru pustego jest poprawna na gruncie ZF.
Ad. ZF2. Wprowadzamy nową stałą indywiduową na oznaczenie pary nieuporządkowanej - {x, y}
∀x ∀y ∀z {z = {x, y} [nieużyteczne w dowodzie] ⇔df ∀w [w∈z ⇔ (w = x ∨ w = y)]}
Istnienie
∀x ∀y ∃z ∀w [w∈z ⇔ (w = x ∨ w = y)] (aksjomat ZF2).
Jednoznaczność
∀x ∀y ∀z ∀z' ({∀w [w∈z ⇔ (w = x ∨ w = y)] ∧ ∀w [w∈z' ⇔ (w = x ∨ w = y…
…') ⇔ (x = x' ∧ y = y')]
Schemat wyróżniania (ograniczony)
(ZF5φ) (Ograniczony schemat wyróżniania)
∀Y ∀x ∃z ∀w [w∈z ⇔ (w∈x ∧ φ)]
ZW(φ) ⊆ {Y, w}
∀Y ∀x ∀z {{w∈x: φ} = z ⇔df ∀w [w∈z ⇔ (w∈x ∧ φ)]
O ile ZW(φ) ⊆ {Y, w}.
Istnienie. Aksjomat.
Jednoznaczność. Z Lematu.
Poprawność definicji iloczynu kartezjańskiego
∀y ∀z ∀w (y × z = w ⇔df ∀u {u∈w ⇔ ∃s ∃t [s∈y ∧ t∈z ∧ u = (s, t)]})
y × z = [(s, t)∈... : s∈y ∧ t…
… ∃z ∀w [w∈z ⇔ (w = x ∨ w = y)]
W szczególności aksjomat ten gwarantuje istnienie singletonu {x}, ponieważ {x} = {x, x}. Wówczas aksjomat ZF2 dla singletonu (Aksjomat istnienia singletonu) wygląda następująco:
(ZF2') ∀x ∃y ∀z (z∈y ⇔ z = x)
Tworzenie nowych zbiorów
Definicja inkluzji
∀x ∀y [x ⊆ y ⇔df ∀z (z∈x ⇒ z∈y)] [nie skrót - kwantyfikator wiąże zmienne]
Ad. ZF1. Wprowadzamy nową stałą indywiduową na oznaczenie…
... zobacz całą notatkę
Komentarze użytkowników (0)