Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

112   2 Verfugbarkeit von Aussagen

(i, Ei) ∈ VANS(EtDom(E)-1). Sei nun (i, Ei) ∈ {(min(Dom(B)), Emin(Dom(B)))}. Dann
gilt mit (vi) ebenfalls (i, E_i) ∈ VANS(EtDom(E)-1).

Zu (viii): Sei Γ ∈ VER(Ei Dom(E )-1)∖VER(E). Dann gibt es ein i ∈
Dom(VERS(EtDom(E)-1)) und Γ = A(E_i). Dann ist (i, E_i) ∈ VERS(EtDom(E)-1) und
(i, E_i) ∉ VERS(E), denn sonst ware Γ ∈ VER(E). Dann gilt mit (iv): (i, E_i) ∈ {(j, Ej) |
min(Dom(B)) ≤ j < Dom(E)-1}. Dann ist Γ ∈ {A(Ej) | min(Dom(B)) ≤ j < Dom(E)-1}.

Zu (ix): Sei Γ ∈ VER(EtDom(E)-1). Dann gibt es ein i ∈ Dom(VERS(EtDom(E)-1),
so dass Γ = A(Ei). Dann ist (i, Ei) ∈ VERS(EtDom(E)-1) und damit auch i < Dom(E)-1.
Sodann ist Γ ∈ {A(Ej) | min(Dom(B)) ≤ j < Dom(E)-1} oder Γ ∉ {A(Ej) | min(Dom(B))
≤ j < Dom(E)-1}. Sei nun Γ ∉ {A(E_j) | min(Dom(B)) ≤ j < Dom(E)-1}. Damit ist dann
auch (i, Ei) ∉ {(j, Ej) | min(Dom(B)) ≤ j < Dom(E)-1} und somit insgesamt (i, Ei) ∈
VERS(EtDom(E)-1)∖{(j, Ej) | min(Dom(B)) ≤ j < Dom(E)-1}. Mit (v) ist dann (i, Ei) ∈
VERS(E) und mit i < Dom(E)-1 gilt (i, Ei) ∈ VERS(E)tDom(E)-1. Also ist i ∈
Dom(VERS(E)tDom(E)-1) und damit Γ ∈ {A(Ej) | j ∈ Dom(VERS(E)tDom(E)-1)}.
Also gilt in beiden Fallen: Γ ∈ {A(Ej) | j ∈ Dom(VERS(E)tDom(E)-1)} и {A(Ej) |
min(Dom(B)) ≤ j < Dom(E)-1}.

Zu (x): Sei Γ ∈ VAN(EΓDom(E)-1)WAN(E). Dann gibt es ein i ∈
Dom(VANS(EtDom(E)-1) und Γ = A(Ei). Dann ist (i, Ei) ∈ VANS(EtDom(E)-1) und
(i, Ei) ∉ VANS(E), denn sonst ware Γ ∈ VAN(E). Dann ergibt sich mit (vi): (i, Ei) =
(min(Dom(φ)), Emin(Dom(B))). Dann ist Γ = A(Ei) = A(⅛,,,,,_l∙∣ >o,,,_l∙⅛_li) ∈ {A(Emin(Dom(B)))}.

Und zuletzt zu (xi): Mit (vii) gilt: VANS(EtDom(E)-1) = VANS(E) ∪ {(min(Dom(B)),
Emin(Dom(B)))}. Damit gilt: Γ ∈ VAN(EtDom(E)-1) gdw es gibt ein i ∈
Dom(VANS(EtDom(E)-1)) und Γ = A(Ei) gdw es gibt ein i ∈ Dom(VANS(E)) ∪
{min(Dom(B))} und Γ = A(Ei) gdw Γ ∈ VAN(E) ∪ {A(Emin(Dom(B)))}. Also gilt
VAN(EtDom(E)-1) = VAN(E) U {A(Emrn(Dom(B)))}. ■

Theorem 2-84. VERS-Verringerung beim Ubergang von EiDom(E)-! zu E dann und nur
dann, wenn dabei ein neuer geschlossener Abschnitt erzeugt wird

Wenn E ∈ SEQ, dann:

VERS(EtDom(E)-1)∖VERS(E) ≠ 0
gdw

Es gibt ein B, so dass

(i) B ein geschlossener Abschnitt in E ist und

(ii)   min(Dom(B)) ≤ Dom(E)-2 und max(Dom(B)) = Dom(E)-1.

<<   87   88   89   90   91   92   93   >>

More intriguing information