Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

6.1 Korrektheit des Redehandlungskalkuls 241

K(AtDom(A)-1). Mit Theorem 5-15 folgt VAN(A)\{A(Amax(Dom(VANS(AiDom(A)-1))))} I=
^rA(‰χ(Dom(VΛNS(⅛∣Dom(⅛)-i)))) → K(AiDom(A)-1)^π. Theorem 5-13 fuhrt zu VAN(A) =
^rA‰aχ(Dom(VΛNS(⅛∣Dom(f_l)-i)))) → K(AiDom(A)-1)^π und damit zu VAN(A) = K(A).

(NEF): Sei A ∈ NEF(AiDom(A)-1). Nach Theorem 3-20-(x) gilt dann K(A) =
^r-A(^max(Dom(VANS(⅛∣Dom(⅛)-1))))^π. Mit Theorem 3-20-(i) und Theorem 2-92, gibt es sodann
Γ ∈ GFORM und j ∈ Dom(A)-1, so dass max(Dom(VANS(AiDom(A)-1))) ≤ j und (j,
Aj) ∈ VERS(Ai Dom(A)-1) und entweder A(Aj) = Γ und A(A_Dom(_A)_-2) = ^r—Γ oder A(Aj)
= ^r—Γ und A(⅛Dom(⅛)-2) = Γ.

Damit ist entweder Γ = K(Aij+1) und ^r—Γ = K(AiDom(A)-1) oder ^r—Γ = K(Aij+1)
und Γ = K(AiDom(A)-1). Sei nun zunachst Γ = K(Aij+1) und ^r—Γ = K(AiDom(A)-1).
Dann gilt VAN(Aij+1) = Γ und VAN(AiDom(A)-1) = ^r—Γ^π. AuBerdem ist Γ in
AiDom(A)-1 bei j verfugbar und daher nach Theorem 3-29-(iv) VAN(Aij+1) ⊂
VAN(AiDom(A)-1) und mit Theorem 5-13 dann VAN(AiDom(A)-1) = Γ. Sei nun ^r— Γ
= K(Aij+1) und Γ = K(AiDom(A)-1). Dann gilt VAN(Aij+1) = ^r—Γ und
VAN(AiDom(A)-1) = Γ. Sodann ist dann ^r—Γ in AiDom(A)-1 bei j verfugbar und da-
her mit Theorem 3-29-(iv) wiederum VAN(Aij+1) ⊂ VAN(AiDom(A)-1) und mit
Theorem 5-13 dann VAN(AiDom(A)-1) = ^r—Γ^π. In beiden Fallen gilt also
VAN(AiDom(A)-1) = Γ und VAN(AiDom(A)-1) = ^r—Γ^π. Mit Theorem 3-20-(ix) gilt
VAN(AiDom(A)-1) = VAN(A) и {A(Amax(Dom(VANS(AiDom(A)-1))))} und damit auch
VAN(A) U {A(Amax(Dom(VANS(AiDom(A)-1))))} = ^{γ und} VAN(A) ∪
{A(Amax(Dom(VANS(⅛∣Dom(⅛)-1))))} = ^r— Γ. Mit Theorem 5-25 (wobei sowohl X als auch Y
durch VAN(A) U {A(Amax(Dom(VANS(AiDom(A)-1))))} instanziiert werden) und Theorem 5-13
folgt VAN(A) = ^r—A(Amax(Dom(VANS(A∣Dom(A)-1))))^^l und damit dass VAN(A) = K(A). Fur
^r—Γ = K(Aij+1) und Γ = K(AΓDom(A)-1) verlauft der Fall analog.

(PBF): Sei A ∈ PBF(AΓDom(A)-1). Nach Theorem 3-21-(x) gilt dann K(A) =
K(AΓDom(A)-1). Mit Theorem 3-21-(i) und Theorem 2-93 gibt es sodann β ∈ PAR, ξ ∈
VAR, Δ ∈ FORM mit FV(Δ) ⊆ {ξ} und Γ ∈ GFORM, so dass
^A(Amax(Dom(VANS(AiDom(A)-1)))-1⁾ = ^rVξΔ^π und (max(Dom(VANS(AiDom(A)-1)))-1,
^Amax(Dom(VANS(AiDom(A )-1)))-1) ∈ VERS(AiDom(A)-1) und A(Amax(Dom(VANS(AiDom(A)-1)))) = [β,
ξ, Δ] und β ∉ TTFM({Δ, K(A)}) und es kein j ≤ max(Dom(VANS(AiDom(A)-1)))-1
gibt, so dass β ∈ TT(Aj). Sodann gilt VAN(AiDom(A)-1) = K(AiDom(A)-1) = K(A).
Mit Theorem 3-21-(ix) gilt sodann VAN(AiDom(A)-1) = VAN(A) и

<<   <   211   212   213   214   215   216   217   >   >>