Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

2.3 VERS, VANS, VER und VAN 117

Beweis: Ergibt sich direkt aus Theorem 2-67, Theorem 2-89 und Theorem 2-90. ■

Theorem 2-92. NE-Schlieβt!-Theorem

A ist ein Abschnitt in ft und es gibt ʌ, Γ ∈ GFORM und i ∈ Dom(ft), so dass

(i)   min(Dom(3)) ≤ i < max(Dom(A)),

(ii)   A(⅛min(Dom(α))) = ʌ und (min(Dom(A)), ftmnDomA))) ∈ VANS(ft[max(Dom(A))),

(iii)   A(ft.i) = Γ und A(ftmax(Dom(A))-1) =   Γ

oder

A(fti) = ^r-Γ Und A(ftmax(Dom(A))-1) = Γ,

(iv)   (i, ft_i) ∈ VERS(ft∣max(Dom(A))),

(v) Es kein r mit min(Dom(A)) < r ≤ max(Dom(2l.))-1 gibt, so dass (r, ft_r) ∈
VANS(ft∣'max(Dom(2l.))), und

(vi)   ftmax(Dom(A)) = ^l"Also — ʌ^

gdw

A ist ein NE-geschlossener Abschnitt in ft.

Beweis: Ergibt sich direkt aus Theorem 2-68, Theorem 2-89 und Theorem 2-90. ■

Theorem 2-93. PB-Schlieβt!-Theorem

A ist ein Abschnitt in ft und es gibt ξ ∈ VAR, β ∈ PAR, ʌ ∈ FORM, wobei FV(Δ) ⊆ {ξ}, Γ
∈ GFORM und B ∈ ABS(ft), so dass

(i)   A(ftmin(Dom(S))) = ^rVξΔ¹ und (min(Dom(B)), ftmin(ŋom(æ))) ∈ VERS(ft[max(Dom( A))),

(ii)   A(ftmin(Dom(B))+1) = [β, ξ, ʌ] und (min(Dθm(B))+1, ftmin(Dom(®))+1) ∈

VANS(ft[^ max(Dom(A))),

⁽ⁱⁱⁱ⁾    A(^ftmax(Dom(B))-1) ^Г,

^{(iv)   ft}max(Dom(B))    Also Γ^^{1 ,}

(v) β ∉ TTFM({Δ, Γ}),

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

(vii) A = B∖{(min(Dom(B)), ftmin . m в )} und

(viii) Es kein r mit min(Dom(A)) < r ≤ max(Dom(A))-1 gibt, so dass (r, ft_r) ∈
VANS(ft[^ max(Dom(A)))

gdw

A ist ein PB-geschlossener Abschnitt in ft.

Beweis: Ergibt sich direkt aus Theorem 2-69, Theorem 2-89 und Theorem 2-90. ■

<<   92   93   94   95   96   97   98   >>

More intriguing information