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*D0m(⅛)+2+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),