Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

144   3 Der Redehandlungskalkul

Theorem 3-19. VERS, VANS, VER und VAN bei SE

Wenn S ∈ SEQ und S' ∈ SEF(S), dann:

(i)   {(j, S'j) | max(Dom(VANS(S))) ≤ j ≤ Dom(S)} ist ein SE-geschlossener Abschnitt in

S',

(ii)   VERS(S)WErS(W) ⊂ {(j, S'j) | max(Dom(VANS(S))) ≤ j < Dom(S)},

(iii) VERS(S') = (VERS(S)∖{(j, S'j) | max(Dom(VANS(S))) ≤ j < Dom(S)}) и
{(Dom(S), ^S Dom(S)^)},

(iv) VANS(S)∖VANS(S') = {(max(Dom(VANS(S))), s'.    ..     , );_

(v)   VANS(S) = VANS(S') и {(max(Dom(VANS(S))), S'max(Dom(VANS(S))))},

(vi) VER(S)∖VER(S') ⊂ {A(S'j) | max(Dom(VANS(S))) ≤ j < Dom(S)},

(vii) VER(S) ⊂ {A(S'j) | j ∈ Dom(VERS(S')fDom(S))} и

{A(S'j) | max(Dom(VANS(S))) ≤ j < Dom(S)},

(Viii) VAN(S)∖VAN(S') ⊂ {A(S'max(Dom(VANS(S))))},

(ix) VAN(S) = VAN(S') и {A(S'max(Dom(VANS(S))))} Und

(x)   K(S') = ^rA(S'max(Dom(VΛNS(S)))) → K(SΓ ∙

Beweis: Sei S ∈ SEQ und S' ∈ SEF(S)∙ Dann gilt mit Definition 3-18 S' ∈ RGF(S)∙ So-
dann gilt mit Definition 3-2: Es gibt Δ, Γ ∈ GFORM und i ∈ Dom(S), so dass A(S_i) = Δ
und (i, S_i) ∈ VANS(S) und A(S_Dom(_S)—1) = Γ und es kein l mit i < l ≤ Dom(S)-I gibt, so
dass (l, S_l) ∈ VANS(S) und S' = S и {(Dom(S), ^rAlso Δ → Γ)} und somit S' ∈ SEQ
und S'ΓDom(S')-1 = SlDom(S) = S∙

Sodann ist ® = {(j, S'j) | i ≤ j ≤ Dom(S)} ein Abschnitt in S' und A(S'_i) = Δ und (i, S'_i)
∈ VANS(S'ΓDom(S)) und A(S Dom(S)-i) Γ und es gibt kein l mit i < l ≤ ^Do^n(S)-1, so
dass (l, S'_l) ∈ VANS(S'ΓDom(S)) und A(S'_Dom(_S)) = r∆ → Γ¹∙ Damit gilt mit Theorem
2-91, dass ® ein SE-geschlossener und damit auch ein geschlossener Abschnitt in S' ist.

Da sodann max(Dom(Φ)) = Dom(S) = Dom(S')-1, ergibt sich mit Theorem 2-86,
dass   VANS(SlDom(S')-1)WANS(S')   =    {(min(Dom(Φ)), ^S min(Dom(S))) ^}

{(max(Dom(VANS(SlDom(S')-1))), S'max(Dom(VANS(S'∣Dom(S')-1))))}∙ Da S = SlDom(S')-1
folgt    daraus: VANS(S)∖VANS(S')    =    {(min(Dom(Φ)), ^S min(Dom(®))^)}

{(max(Dom(VANS(S))), S'max(Dom(VANS(S))))}∙ Damit ist i = mi n( Dom(⁴B)) =
max(Dom(VANS(S))) und es gilt: ® = {(j, S'j) | max(Dom(VANS(S))) ≤ j ≤ Dom(S)}∙
Damit gilt dann (i). AuBerdem gilt dann A(S'_max(_Dom(v_ANS(_S)))) = A(S_i) = Δ und da K(S) =
Γ und K(S') = r∆ → Γ^π gilt dann (x). Sodann ergibt sich mit VANS(S)∖VANS(S') ≠ 0
und Theorem 2-73 auch VERS(S)∖VERS(S') ≠ 0∙ Damit und mit S = S'ΓDom(S')-1 und
® = {(j, S'j) | max(Dom(VANS(S))) ≤ j ≤ Dom(S)} ergeben sich dann mit Theorem

<<   118   119   120   121   122   123   124   >>

More intriguing information