Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

116   2 Verfugbarkeit von Aussagen

Af max(Dom(A)). Ware dann min(Dom(C)) ≤ l < max(Dom(C)), dann ware damit (l, Al)
∉ VERS( Af max(Dom( A))), was der Annahme widerspricht. Also ist l < min(Dom(C))
oder max( Dom(C)) ≤ l. (R-L): Gelte nun fur alle geschlossenen Abschnitte C in
Afmax(Dom(A)): l < min(Dom(C)) oder max(Dom(C)) ≤ l. Dann gilt fur alle geschlosse-
nen Abschnitte C in Af max(Dom(A)), dass es nicht der Fall ist, dass mιn(Dom(C)) ≤ l <
max(Dom(C)). Sodann ist nach Voraussetzung l ∈ Dom(Afmax(Dom(A))) und damit ist
A(Al) in Af max(Dom(A)) bei l verfugbar. Also gilt: (l, Al) ∈ VERS(Afmax(Dom(A))). ■

Theorem 2-90. Vorbereitungstheorem (b) fur Theorem 2-91, Theorem 2-92 und Theorem 2-93
Wenn A ein Abschnitt in A ist und l ∈ Dom(Af max(Dom(A))), dann:

(l, Al) ∈ VANS(Afmax(Dom(A)))
gdw

(l, Al) ∈ ANS(A) und fur alle geschlossenen Abschnitte C in Afmax(Dom(A)) gilt: l <
min(Dom(C)) oder max(Dom(C)) ≤ l.

Beweis: Sei A ein Abschnitt in A und l ∈ Dom(Afmax(Dom(A))). (L-R): Sei nun zu-
nachst (l, Al) ∈ VANS(Afmax(Dom(A))). Dann ist (l, Al) ∈ VERS(Afmax(Dom(A))) ∩
ANS( Af max(Dom(A))) und da ANS(Afmax(Dom(A))) ⊆ ANS(A) ist damit (l, Al) ∈
ANS(A). Sodann ergibt sich mit (l, Al) ∈ VERS(Afmax(Dom(A))) und Theorem 2-89,
dass fur alle geschlossenen Abschnitte C in Afmax(Dom(A)) gilt: l < min(Dom(C)) oder
max(Dom(C)) ≤ l. (R-L): Sei nun (l, Al) ∈ ANS(A) und gelte fur alle geschlossenen Ab-
schnitte C in Af max(Dom( A)): l < min(Dom(C)) oder max(Dom(C)) ≤ l. Nach Vorausset-
zung gilt, dass l ∈ Dom( Af max(Dom(A))) und damit, dass (l, Al) ∈
ANS(Afmax(Dom(A))). Sodann ergibt sich mit Theorem 2-89, dass (l, Al) ∈
VERS(Afmax(Dom(A))) und damit insgesamt, dass (l, Al) ∈ VANS(Afmax(Dom(A))). ■

Theorem 2-91. SE-Schlieβt!-Theorem

A ist ein Abschnitt in A und es gibt Δ, Γ ∈ GFORM, so dass

(i)   A(Amin(Dom(A))) = Δ und (min(Dom(A)), Amm(Dom(A))) ∈ VANS(Afmax(Dom(A))),

(ii) A(Amax(Dom(A))-I) = Γ,

(iii) Es kein r mit min(Dom(A)) < r ≤ max(Dom(A))-1 gibt, so dass (r, Ar) ∈
VANS(Afmax(Dom(A))), und

(iv) Amax(Dom(A)) = ^rAlso Δ → Γ^
gdw

A ist ein SE-geschlossener Abschnitt in A.

<<   91   92   93   94   95   96   97   >>

More intriguing information