Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

3.3 VERS, VANS, VER und VAN in Ableitungen und bei einzelnen Ubergangen 149

e) Es kein r mit min(Dom(¾)) < r ≤ Dom(⅛)-1 gibt, so dass (r, ⅛'_r) = (r, ⅛_r) ∈
VANS(⅛), und

^f    ⅛^lDom(^) = ^rA^{lso — A(}^'min(Dom(a))⁾ⁿ = ^rA^{lso —}A(⅛min(Dom(α)))^ .

Dann ist nach Definition 3-10 ⅛' ∈ NEF(⅛). Sei nun ∖λ ein PB-geschlossener Abschnitt in
⅛'. Dann gilt mit Theorem 2-93, dass es ξ ∈ VAR, β ∈ PAR, Δ ∈ FORM, wobei FV(Δ)
⊆ {ξ}, Γ ∈ GFORM und B ∈ ABS(⅛') gibt, so dass:

a)   A(^'min(Dom(B))) = ' VξΔ ' und (miH(Dθm( B )), ⅛'min(Dom(<B))) ∈ VERS(^),

b)   A(‰n(Dom(<B>1) = [β, ξ, Δ] und (min(Dθm(B))+1, ‰n(Dom(B))+1) ∈ VANS(3),

c)    A(#max(Dom(B ))-1) ^Г,

^d)   ^ max(Dom(B))    ^Also Γ ^,

e) β ∉ TTFM({Δ, Γ}),
f)    Es kein j ≤ min(Dom(B)) gibt, so dass β ∈ TT(^'_j∙),

g) Я = B∖{(min(Dom(B)), ‰n(Dom₀B)))} und

h)   Es kein r mit min(Dom(^)) < r ≤ Dom(⅛)-1 gibt, so dass (r, ⅛'_r) ∈ VANS(⅛).

Dann gilt mit g): min(Dom(^)) = min(Dom(B))+1 und Dom(⅛) = max(Dom(^)) =
max(Dom(B)). Damit gilt dann min(Dom(B)) < min(Dom(^)) ≤ Dom(⅛)-1 und also
insgesamt min(Dom(B)), min(Dom(B))+1 ∈ Dom(.∆) und max(Dom(B))-1 =
Dom(⅛)-1. Damit gilt dann:

a')  A(^min(Dom₀B))) = "VξΔ" und (min(Dom(B)), ⅛j_m<₈))) ∈ VERS(⅛),

b')  A‰in(Dom(<B))+1) = [β, ξ, Δ] und (min(Dθm(B))+1, ‰Dom(<B))+1) ∈ VANS(3),

^c')   ^A(^Dom(^)-1) = ^γ,

d')  ‰mtt>) = ^rAlso Γ,

e') β ∉ TTFM({Δ, Γ}),

f)   Es gibt kein j ≤ min(Dom(B)), so dass β ∈ TT(⅛),

h') Es gibt kein r mit min(Dom(B))+1 < r ≤ Dom(⅛)-1, so dass (r, fi_r) ∈
VANS(⅛).

Dann ist nach Definition 3-15 ⅛' ∈ PBF(⅛). Also ist in allen drei Fallen ⅛' ∈ SEF(⅛) и

NEF(⅛) и PBF(⅛). ■

<<   123   124   125   126   127   128   129   >>

More intriguing information