Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

150   3 Der Redehandlungskalkul

Theorem 3-24. VERS-Verringerung bei und nur bei SE, NE undPB

Wenn й ∈ SEQ und й' ∈ RGF(⅛), dann:

VERS(⅛) £ VERS(⅛')
gdw

{(j, й';) | max(Dom(VANS(⅛))) ≤ j ≤ Dom(⅛)} ist ein SE- oder NE- oder PB-geschlossener
Abschnitt in й' und й'є SEF(⅛) ∪ NEF(φ) ∪ PBF(⅛).

Beweis: Sei й ∈ SEQ und й' ∈ RGF(#). Die Rechts-Links-Richtung ergibt sich mit den
Klausel (iv) von Theorem 3-19, Theorem 3-20 und Theorem 3-21 sowie Theorem 2-72.
Sei nun fur die Links-Rechts-Richtung VERS(⅛) £ VERS(#'). Dann ist
VERS(⅛)∖VERS(⅛') ≠ 0∙ Sodann ist mit й' ∈ RGF(^) und Theorem 3-1 й' ∈ SEQ. und
mit Theorem 3-5 ist й''І)от(й')-І = й. Mit Theorem 2-83-(vi) und -(vii) gilt dann
VANS(#) ⊂ VANSφ)∙ Mit Theorem 3-23 gilt: й'е SEF(ft) ∪ NEF(ft) ∪ PBF(ft).
Damit ergibt sich mit Theorem 3-19-(i), Theorem 3-20-(i) und Theorem 3-21-(i), dass {(j,
й';) | max(Dom(VANS^))) ≤ j ≤ Dom^)} ein SE- oder NE- oder PB-geschlossener Ab-
schnitt in й' ist. ■

Theorem 3-25. VERS unter Ausschluss von SE, NE und PB

Wenn й ∈ SEQ und й' ∈ RGFφ)∖(SEFφ) ∪ NEF^) ∪ PBFφ)), dann:
VERS(#) = VERS^) ∪ {(Dom(M й'^ед)}.

Beweis: Seien й ∈ SEQ und й' ∈ RGFφ)∖(SEFφ) ∪ NEF(ft) ∪ PBF(ft)). Wegen
Theorem 3-14-(i) ist VERS(^) ⊆ VERS(^) ∪ {(Dom(^), ^D_om(⅛))}∙ Mit Theorem 2-82
ist К(й') = A^Domc^-i) in й' bei Dom(^)-1 verfugbar. Mit Theorem 3-4 ist Dom(^)-1
= l)om(ʃɔ). Also (l)om(ʃɔ), й'_Dom(й)) ∈ VERS(^)∙ Ware VERS^) £ VERS(φ), so ware
mit Theorem 3-24 entgegen der Voraussetzung й' ∈ SEF(^) ∪ NEF(^) ∪ PBF(^)∙ Also
VERS(ft) ⊆ VERS(tf)∙ Also gilt auch VERS(ft) ∪ {(Dom(ft), ^Dom(⅛))} ⊆ VERS(6')∙
■

Theorem 3-26. VERS, VANS, VER und VAN bei KE, BE, AE, UE, PE, IE

Wenn й ∈ SEQ und й' ∈ KEF^) ∪ BEFφ)u AEFφ) ∪ UEFφ) ∪ PEFφ)u IEF(M dann:
(i)  VERS(#) ⊆ VERS(^ ∪ {(Dom(M ‰»)},

(ii)  VANS(#) ⊆ VANSφ),

(iii) Wenn VANS(φ) ⊂ VANS^), dann ist й' ∈ PBF^),

(iv) VER(й') ⊆ VERφ) ∪ {К(й')},

<<   124   125   126   127   128   129   130   >>

More intriguing information