Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

2.2 Geschlossene Abschnitte

Gelte nun ANS(ft) ∩ ^ = i(mm(Dom(ft)), ft_mm(D_om(a)))}∙ Dann ergibt sich damit, dass
fur alle k ∈ Dom(ft) gilt, dass ^∖k kein geschlossener Abschnitt in ft ist, und Theorem
2-32, dass ∖λ ein minimaler geschlossener und damit ein geschlossener Abschnitt in ft ist.
Da ∖λ ein SE-artiger Abschnitt in ft ist, ist ∖λ damit ein SE-geschlossener Abschnitt in ft.

Gebe es nun ein i ∈ Dom(ANS(ft)) ∩ Dom(ft) mit mm(Dom(ft)) < i ≤
max(Dom(^))-1. Sei nun C = {(l, ft_l) | min(Dom(^))+1 ≤ l ≤ max(Dom(^))-1}. Dann ist
C ein Abschnitt in ft und i ∈ Dom(ANS(ft)) ∩ Dom(C). Sodann gibt es fur jedes r ∈
Dom(ANS(ft)) ∩ Dom(C) einen geschlossenen Abschnitt ® in ft, so dass (r, ft_r) ∈ ®
und ® ⊆ C. Sei namlich r ∈ Dom(ANS(ft)) ∩ Dom(C). Dann ist mπι(Dom(ft)) < r ≤
max(Dom(ft ))-1 und somit gibt es nach Klausel (iv) einen geschlossenen Abschnitt 'B in
ftΓmax(Dom(^.)), so dass (r, ft_r) ∈ 'K Dann ist min(Dom(C)) ≤ min(Dom(Φ)), denn an-
dernfalls ware mιn(Dom('B)) ≤ mm(Dom(ft)) < r ≤ max(Dom(Φ)), was Klausel (ii) wi-
derspricht. Zum anderen ergibt sich daraus, dass 'B ein Abschnitt in ftΓmax(Dom(^.)) ist,
dass max(Dom(Φ)) ≤ max(Dom(^))-1 = max(Dom(C)). Also ist mit Theorem 2-5 'B ⊆
C.

Damit erfullt C die Voraussetzungen von Theorem 2-59. Also gibt es ein G ∈
ANSUMF(ft), so dass G eine ANS-umfassende Abschnittsfolge fur C in ft ist und {ft} ×
Ran( G) ⊆ GS. Nun gilt nach Definition von C, dass C ∈ ABS(ft) und min(Dom(^))+1 =
min(Dom(C)) und ma∖(Dom(ft)) = max(Dom(C))+1 und ANS(ft) ∩ C ≠ 0. Sodann ist ∖λ
ein SE-artiger Abschnitt in ft. Damit gilt mit Theorem 2-28 auch, dass ∖λ kein NE-artiger
Abschnitt in ft ist. Ferner gilt damit, dass fur alle i ∈ Dom(ft) gilt, dass ^Γi kein ge-
schlossener Abschnitt in ft ist, dass auch fur alle i ∈ Dom(ft) gilt: ^↑i ist kein minimaler
geschlossener Abschnitt in ft.

Damit ist gemaβ Definition 2-18 ft ∈ PERZ((ft, G)). Ware es nun der Fall, dass es ein k
∈ Dom(ft) und ein l ∈ Dom(G) gabe, so dass ft↑k ∈ PERZ((ft, Gt(l+1)))∙ Dann ist nach
Theorem 2-25 G∣^(l+1) eine ANS-umfassende Abschnittsfolge fur ft↑max(Dom(G(l)))+1.
Damit ist dann nach Definition 2-10 Gf^(l+1) ∈ ANSUMF(ft) und nach Annahme ft↑k ∈
PERZ((ft, G∣^(l+1)>) und andererseits ft ∈ SEQ und {ft} × Ran(G∣^(l+1)) ⊆ {ft} ×
Ran(G) ⊆ GS, was insgesamt im Widerspruch zu Theorem 2-65-(ii) steht. Also gibt es
kein k ∈ Dom(ft) und kein l ∈ Dom(G), so dass ft↑k ∈ PERZ((ft, Gt(l+1)))∙ Damit ist
nach Definition 2-19 ft ∈ ERZ((ft, G)) und weil {ft} × Ran( G) ⊆ GS mit Theorem 2-41

<<   70   71   72   73   74   75   76   >>

More intriguing information