Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

146   3 Der Redehandlungskalkul

max(Dom(VANS(A))) und es gilt: ® = {(j, A'j) | max(Dom(VANS(A))) ≤ j ≤ Dom(A)}.
Damit gilt dann (i). Auβerdem gilt dann A(A'_max(Do_m(v_ANs( a >») = A(A_i) = Δ und da K(A') =
AV gilt dann (x). Sodann ergibt sich mit VANS(A)∖VANS(A') ≠ 0 und Theorem 2-73
auch VERS(A)WeRS(A) ≠ 0. Damit und mit A = A'ΓDom(A')-1 und ® = {(j, A'j) |
max(Dom(VANS(A))) ≤ j ≤ Dom(A)} ergeben sich dann mit Theorem 2-83-(iv) bis -(xi)
und mit der eindeutigen Bestimmtheit geschlossener Abschnitte mit demselben Endglied
(Theorem 2-53) die restlichen Klauseln ((ii) bis (ix)). ■

Theorem 3-21. VERS, VANS, VER und VAN bei PB

Wenn A ∈ SEQ und A' ∈ PBF(A), dann:

(i)   {(j, A'_j) | max(Dom(VANS(A))) ≤ j ≤ Dom(A)} ist ein PB-geschlossener Abschnitt in

A',

(ii)   VERS(A)∖VERS(A') ⊆ {(j, A'j) | max(Dom(VANS(A))) ≤ j < Dom(A)},

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

(iv) VANS(A)∖VANS(A') = {(max(Dom(VANS(A))), A'max(Dom(VANS(A))))},

(v)   VANS(A) = VANS(A') U {(max(Dom(VANS(A))), A'max(Dom(VANS(A))))},

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

(vii) VER(A) ⊆ {A(A'j) | j ∈ Dom(VERS(A')iDom(A))} и

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

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

(ix) VAN(A) = VAN(A') U {A(A'max(Dom(VANS(A))))} und
(x)   K(A') = K(A).

Beweis: Sei A ∈ SEQ und A' ∈ PBF(A). Dann gilt mit Definition 3-18 A' ∈ RGF(A). So-
dann gilt mit Definition 3-15: Es gibt β ∈ PAR, ξ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆
{ξ}, Γ ∈ GFORM und i ∈ Dom(A), so dass A(A_i) = ^rVξΔ^^l und (i, A_i) ∈ VERS(A),
A(A_i+1) = [β, ξ, Δ] und (i+1, Ai+1) ∈ VANS(A), und A(Aυom(A)-1) = Γ, wobei β ∉
TTFM({Δ, Γ}), und es kein j ≤ i gibt, so dass β ∈ TT(Aj), und es kein m mit i+1 < m ≤
Dom(A)-1 gibt, so dass (m, A_m) ∈ VANS(A), und A' = A и {(Dom(A), ^rAlso Γ)} und
somit A' ∈ SEQ und A'ΓDom(A')-1 = AlDom(A) = A.

Sodann ist ® = {(j, A'_j) | i+1 ≤ j ≤ Dom(A)} ein Abschnitt in A' und β ∈ PAR, ξ ∈
VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξ}, Γ ∈ GFORM und A(A'i) = VξΔ^π und (i, A'i) ∈
VERS(A'ΓDom(A)), A(A'_i+1) = [β, ξ, Δ] und (i+1, A'_i+₁) ∈ VANS(A'ΓDom(A)-1), und
A(A'Dom<A)-ι) = Γ, wobei β ∉ TTFM({Δ, Γ}), und es gibt kein j ≤ i, so dass β ∈ TT(A'j),
und es gibt kein m mit i+1 < m ≤ Dom(A)-1, so dass (m, A'_m) ∈ VANS(AlDom(A))₅ und

<<   120   121   122   123   124   125   126   >>

More intriguing information