Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

2.1 Abschnitte und Abschnittsfolgen

Theorem 2-16. Eigenschaften von Abschnittsfolgen

Wenn ft ∈ SEQ und G ∈ ABSF(ft), dann:

(i)    G ist eine Injektion von Dom(G) in Ran(G),

(ii) G ist eine Bijektion zwischen Dom(G) und Ran(G),

(iii) Dom(G) = ∣Ran(G)| und

(iv) G ist eine endliche Folge.

Beweis: Sei ft ∈ SEQ und G ∈ ABSF(ft). Dann ist G eine Folge mit Ran(G) ⊆ ABS(ft)
und fur alle i, j ∈ Dom(G) gilt: Wenn i < j, dann min(Dom(G(i))) < min(Dom(G(j))) und
max(Dom(G(i))) < min(Dom(G(j))).

Zu (i): Seien nun i, j ∈ Dom(G) und sei G(i) = G(j). Dann ist min(Dom(G(i))) =
min(Dom(G(j))). Ware i ≠ j. Dann ist i < j oder j < i und damit ware min(Dom(G(i))) <
min(Dom(G(j))) oder min(Dom(G(j))) < min(Dom(G(i))). Beides steht jedoch im Wi-
derspruch zu min(Dom(G(i))) = min(Dom(G(j))). Also ist fur i, j ∈ Dom(G) mit G(i) =
G(j) auch i = j und somit G eine Injektion von Dom(G) in Ran(G).

Zu (ii): G ist eine Surjektion von Dom(G) auf Ran(G) und mit (i) ist G dann eine Bi-
jektion zwischen Dom(G) und Ran(G).

Zu (iii): Da G eine Folge ist, gilt mit (ii): Dom(G) = |Ran(G)|

Zu (iv): G ist eine Folge und mit (iii) ist G dann eine endliche Folge, denn Ran(G) ⊆
ABS(ft) ⊆ POT(ft) und somit (da mit ft ∈ SEQ gilt, dass ∣ft∣ ∈ N): Dom(G) = ∣Ran(G)∣
≤ ∣ABS(ft)∣ ≤ ∣POT(ft)∣ = 2^lftl ∈ N. ■

Theorem 2-17. Existenz von Abschnittsfolgen, die alle Elemente einer Menge von disjunkten
Abschnitten aufzahlen

Wenn ft ∈ SEQ und X ⊆ ABS(ft) und fur alle 21, W ∈ X gilt: Wenn 21. ≠ W, dann 21. ∩ W = 0,
dann: Es gibt es G ∈ ABSF(ft), so dass Ran(G) = X.

Beweis: Sei ft ∈ SEQ und X ⊆ ABS(ft) und gelte fur alle 2f 21' ∈ X: Wenn 21 ≠ ^^,, dann
21 ∩ 2t' = 0. Nun ist ® = {(l, ft_l) ∣ Es gibt ein 21 ∈ X und l = min(Dom(^))} ⊆ ft und da-
mit gibt es nach Theorem 2-10 eine passende Folge naturlicher Zahlen g fur ®. Dann ist g
mit Theorem 2-11 eine Bijektion zwischen Dom(g) und Dom(®) und damit gilt nach De-
finition von ® fur alle 21 ∈ X: mιn(Dom(2l)) = g(i) fur ein i ∈ Dom(g). Sodann gilt

<<   57   58   59   60   61   62   63   >>

More intriguing information