Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

60    2 Verfugbarkeit von Aussagen

Theorem 2-20. Existenz von ANS-Umfassenden Abschnittsfolgen fur alle Abschnitte

Wenn ft ∈ SEQ und ^ ∈ ABS(ft), dann gibt es eine ANS-umfassende Abschnittsfolge G fur
A in ft.

Beweis: Sei ft ∈ SEQ und A ∈ ABS(ft). Dann ist {(0, ^)} eine ANS-umfassende Ab-
Schnittsfolge fur A in ft. ■

Theorem 2-21. Eine Sequenz ft ist genau dann nicht-leer, wenn ANSUMF(ft) nicht-leer ist
Wenn ft ∈ SEQ, dann: ft ≠ 0 gdw ANSUMF(ft) ≠ 0.

Beweis: Sei ft ∈ SEQ. Sei nun ft ≠ 0. Dann gibt es mit Theorem 2-1 ein A, so dass A ∈
ABS(ft). Daraus folgt mit Theorem 2-20, dass ANSUMF(ft) ≠ 0. Sei nun umgekehrt
ANSUMF(ft) ≠ 0. Dann gibt es nach Definition 2-10 ein A ∈ ABS(ft) und damit gilt
wiederum mit Theorem 2-1, dass ft ≠ 0. ■

Theorem 2-22. Eigenschaften von ANS-Umfassenden Abschnittsfolgen

Wenn ft ∈ SEQ und G ∈ ANSUMF(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 ∈ ANSUMF(ft). Dann folgt mit Definition 2-9, dass G ∈
ABSF(ft)∖{0} und damit und mit Theorem 2-16 die Behauptung. ■

Theorem 2-23. Alle Glieder einer ANS-Umfassenden Abschnittsfolge liegen innerhalb des
betreffenden Abschnitts

Wenn G eine ANS-umfassende Abschnittsfolge fur 21. in ft ist, dann gilt fur alle i ∈ Dom(G):
min(Dom(^)) ≤ min(Dom( G (i))) und max(Dom( G (i))) ≤ max(Dom(2l)).

Beweis: Sei G eine ANS-umfassende Abschnittsfolge fur A in ft und sei i ∈ Dom(G).
Dann ist 0 ≤ i ≤ max(Dom(G)). Ferner gilt dann - da nach Definition 2-9 G ∈
ABSF(ft)∖{0} - mit Definition 2-7 fur alle k, j ∈ Dom(G): Wenn k < j, dann
min(Dom(G(k))) < min(Dom(G(j))) und max(Dom(G(k))) < min(Dom(G(j))).
Also gilt: min(Dom(G(0))) ≤ min(Dom(G(i))) und max(Dom(G(i))) ≤

<<   60   61   62   63   64   65   66   >>

More intriguing information