Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

152   3 Der Redehandlungskalkul

fur (vi) VAN(S') ⊂ VAN(S). Dann gilt VAN(S) £ VAN(S') und damit mit Theorem
2-75 VANS(S) £ VANS(S'). Damit gilt mit (ii): VANS(S') ⊂ VANS(S) und damit mit
(iii), dass S' ∈ SEF(S) и NEF(S) и PBF(S). ■

Theorem 3-28. Ohne AR, SE, NE oder PB gibt es keine VAN-Veranderung

Wenn S ∈ RGS und S ∉ AF(StDom(S)-1) ∪ SEF(SiDom(S)-1) ∪ NEF(SiDom(S)-1) ∪
PBF(StDom(S)-1), dann VAN(S) = VAN(Sl'Dom(S)-1).

Beweis: Sei S ∈ RGS und S ∉ AF(SΓDom(S)-1) и SEF(SΓDom(S)-1) и
NEF(SΓDom(S)-1) и PBF(SΓDom(S)-1). Dann ist S = 0 oder S ≠ 0. Im ersten Fall ist
SΓDom(S)-1 ⊆ S = 0 und das Theorem gilt. Sei nun S ≠ 0. Nach Theorem 3-6 und
Definition 3-18 gilt dann erstens S ∈ KEF(SΓDom(S)-1) oder S ∈ BEF(SΓDom(S)-1)
oder S ∈ AEF(SΓDom(S)-1) oder S ∈ UEF(SΓDom(S)-1) oder S ∈ PEF(SΓDom(S)-1)
oder S ∈ IEF(SΓDom(S)-1) oder zweitens S ∈ SBF(SΓDom(S)-1) oder S ∈
KBF(SΓDom(S)-1) oder S ∈ BBF(SΓDom(S)-1) oder S ∈ ABF(SΓDom(S)-1) oder S
∈ NBF(SΓDom(S)-1) oder S ∈ UBF(SΓDom(S)-1) oder S ∈ IBF(SΓDom(S)-1). In den
ersten sechs Fallen folgt VAN(S) = VAN(SΓDom(S)-1) aus Theorem 3-26-(v) und -(vi).
In den restlichen Fallen folgt VAN(S) = VAN(SΓDom(S)-1) aus Theorem 3-27-(v) und
-(vi). ■

Theorem 3-29. VERS, VANS, VER und VAN bleiben aus Beschrankungen, deren Konklusion
verfugbar bleibt, in der unbeschrankten Sequenz erhalten.

Wenn S ∈ RGS und Γ in S bei i verfugbar ist, dann:

(i)   VERS(SN+1) ⊆ VERS(S),

(ii) VANS(SN+1) ⊆ VANS(S),
(iii) VER(SN+1) ⊆ VER(S) und
(iv) VAN(SN+1) ⊆ VAN(S).

Beweis: Sei S ∈ RGS und Γ in S bei i verfugbar. Dann gilt nach Definition 2-26: i ∈
Dom(S) und Γ = A(Si) und es gibt keinen geschlossenen Abschnitt `d in S, so dass
mιn(Dom('d)) ≤ i < max(Dom(^)).

Zu (i): Sei zum Nachweis von VERS(SΓi+1) ⊆ VERS(S) (j, ∑) ∈ VERS(SΓi+1). Also
mit Definition 2-28: j ∈ Dom(SΓi+1) und (SΓi+1)j = Σ und Α(Σ) ist in SΓi+1 bei j ver-
fugbar. Damit gibt es nach Definition 2-26 keinen geschlossenen Abschnitt `d in Sti+1,
so dass min(Dom(^)) ≤ j < max(Dom(^)). Ware nun (j, Σ) ∉ VERS(S), dann ware j ∉

<<   126   127   128   129   130   131   132   >>

More intriguing information