Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

168  4 Theoreme zur deduktiven Konsequenzschaft

K(⅛*)}) und es kein j ≤ Dom(⅛)+1+i gibt, so dass β ∈ TT(⅛*j). Damit ist dann .ħ' ∈
PBF(⅛*). Sei nun ξ ∉ FV(Δ). Dann ist β ∉ TT([β, ξ, Δ]). Nun gibt es ein β* ∈
PARMTTSEQ(T)) и TTSEQCft')). Dann ist mit Theorem 1-14-(ii) [β*, ξ, Δ] = Δ = [β, ξ,
Δ] = A(ft'_i+ι) = A(ft*D_0m(⅛)+₂+_i). Sodann gilt dann, dass β* ∉ TTFM({Δ, K(ft*)}) und es
kein j ≤ Dom(ft)+1+i gibt, so dass β* ∈ TT(ft*_j). Damit ist dann wiederum ft' ∈
PBF(ft*). Es gilt also insgesamt, dass ft' ∈ PBF(ft*) ⊂ RGS∖{0}. Dass auch (v) gilt,
ergibt sich dann mit v') und Theorem 3-21-(iii) analog zu SEF und NEF.

(SBF, KEF, KBF, BEF, BBF, AEF, ABF, NBF, UBF, PEF, IEF, IBF): Sei nun ft' ∈
SBF(ft'ΓDom(ft')-1). Dann gibt es nach Definition 3-3 Δ, Γ ∈ GFORM, so dass Δ, ^rΔ →
Γ ∈ VER(ft'ΓDom(ft')-1) und ft' = ft'ΓDom(ft')-1 и {(Dom(ft')-1, ^rAlso Γ^π)}. Dann gilt
mit vi'): ft' = ft* и {(Dom(ft)+1+Dom(ft')-1, rAlso Γ^^l)}. Sodann gilt mit Δ, r∆ → Γ ∈
VER(ft'ΓDom(ft')-1), Definition 2-30 und iv'), dass es i, j ∈ Dom(VERS(ft'ΓDom(ft')-1))
gibt, so dass Δ = A(ft'i) = A(.ħ*∣>_l4,,_l-_m.∣.∙) und r∆ → Γ^^, = A(ftj) = Λ(ft*D_θm(⅛)+1+j). So-
dann gilt mit v'), dass Dom(ft)+1+i, Dom(ft)+1+j ∈ Dom(VERS(ft*)). Damit ist dann
insgesamt ft⁺ ∈ SBF(ft*) ⊂ RGS∖{0}.

Sodann ist ft' ∈ SEF(ftTDom(ft')-1) и NEF(ft'ΓDom(ft')-1) и PBF(ftTDom(ft')-1)
oder ft' ∉ SEF(ft'ΓDom(ft')-1) и NEF(ft'ΓDom(ft')-1) и PBF(ft'ΓDom(ft')-1). Im ersten
Fall ergibt sich die Gultigkeit von (v) wie unter den jeweiligen Fallbetrachtungen. Sei nun
ft' ∉ SEF(ft'ΓDom(ft')-1) и NEF(ft'ΓDom(ft')-1) и PBF(ftTDom(ft')-1). Dann gilt mit
ix'), dass auch ft⁺ ∉ SEF(ft*) и NEF(ft*) и PBF(ft*). Dann gilt mit Theorem 3-25, dass
VERS(ft') = VERS(ft'ΓDom(ft')-1) и {(Dom(ft)-1, rAlso Γ^π)} und VERS(ft⁺) =
VERS(ft*) и {(Dom(ft)+1+Dom(ft')-1, rAlso Γ^π)}. Mit v') ergibt sich dann wie bei AF,
dass VERS(ft⁺) =  Dom(VERS(ft)) и {Dom(ft)}  и  {(Dom(ft)+1+l |  l  ∈

Dom(VERS(ft'))} und folglich (v) gilt.

Fur den Fall, dass  ft'   ∈ KEF(ft'ΓDom(ft')-1)   и  KBF(ft'ΓDom(ft')-1)   и

BEF(ft'ΓDom(ft')-1)    и    BBF(ft'ΓDom(ft')-1) и    AEF(ftTDom(ft')-1)    и

ABF(ft'ΓDom(ft')-1)    и    NBF(ft'ΓDom(ft')-1) и    UBF(ft'ΓDom(ft')-1)    и

PEF(ft'ΓDom(ft')-1) и IEF(ft'ΓDom(ft')-1) и IBF(ft'ΓDom(ft')-1), zeigt man analog, dass
dann auch ft⁺ ∈ KEF(ft*) и KBF(ft*) и BEF(ft*) и BBF(ft*) и AEF(ft*) и ABF(ft*)
и NBF(ft*) и UBF(ft*) и PEF(ft*) и IEF(ft*) и IBF(ft*) ⊆ RGS∖{0} und jeweils v)
gilt.

(UEF): Sei nun ft' ∈ UEF(ft'ΓDom(ft')-1). Dann gibt es nach Definition 3-12 β ∈ PAR,
ξ ∈ VAR und Δ ∈ FORM, wobei FV(Δ) ⊂ {ξ}, so dass [β, ξ, Δ] ∈ VER(ft'ΓDom(ft')-1),

<<   141   142   143   144   145   146   147   >>

More intriguing information