Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

2.1 Abschnitte und Abschnittsfolgen

min(Dom(G(i))) ≤ max(Dom( G (i))) und beide Falle widersprechen der Annahme. Also
ist i = j. ■

Theorem 2-19. Verschiedene Glieder einer Abschnittsfolge sind elementfremd

Wenn ʃɔ ∈ SEQ und G ∈ ABSF(⅛), dann gilt fur alle i, j ∈ Dom(G): Wenn G(i) ≠ G(j), dann
G(i) ∩ G(j) = 0.

Beweis: Sei ⅛ ∈ SEQ und G ∈ ABSF(⅛). Dann ist G eine Folge mit Ran(G) ⊆ ABS(⅛)
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))). Seien i, j ∈ Dom(G). Dann gilt: G(i), G(j) ∈
ABS(⅛). Sei nun G(i) ≠ G(j). Dann gilt mit Theorem 2-16-(i), dass i ≠ j. Dann ist i < j
oder j < i. Dann ist

min(Dom(G(i))) < min(Dom(G(j))) und max(Dom(G(i))) < min(Dom(G(j)))
oder

min(Dom(G(j))) < min(Dom(G(i))) und max(Dom(G(j))) < min(Dom(G(i))).

Also ist mit Theorem 2-8 G(i) ∩ G(j) = 0. ■

Definition 2-9. ANS-Umfassende Abschnittsfolge fur einen Abschnitt in f

G ist eine ANS-umfassende Abschnittsfolge fur 21. in ʃɔ
gdw

(i)   £ ∈ SEQ,

(ii)   Я ∈ ABS(⅛),

(iii) G ∈ ABSF(⅛)∖{0} und

a)   min(Dom(^)) ≤ min(Dom( G (0))),

b)   max(Dom( G (max(Dom( G))))) ≤ max(Dom(2l)) und

c) Fur alle l ∈ Dom(ANS(⅛)) ∩ Dom(^) gilt: Es gibt ein i ∈ Dom( G), so dass l
∈ Dom( G (i)).

Definition 2-10. Zuordnung der Menge der ANS-Umfassenden Abschnittsfolgen in f
(ANSUMF)

ANSUMF = {(⅛, X) | ⅛ ∈ SEQ und X = {G | Es gibt ein 21. ∈ ABS(⅛) und G ist eine
ANS-umfassende Abschnittsfolge fur 21. in ⅛}}.

<<   59   60   61   62   63   64   65   >>

More intriguing information