184 4 Theoreme zur deduktiven Konsequenzschaft
damit mit Theorem 1-20 A(⅛i) = [β*, ζ, Δ+]. Ware nun β* ∈ TTFM({Δ+, A(‰om(⅛)-2)})
oder gabe es ein j ≤ i-1, so dass β* ∈ TT(.<ι ). Dann ware wegen β* ≠ α mit d) auch β* ∈
TTFM({[β, α, Δ+], [β, α, A(‰m(⅛>2)]}) oder es gabe j ≤ i, so dass β* ∈ TT(⅛*j). Wider-
spruch! Also ist im ersten Fall die Parameterbedingung fur β* auch in .ħfDom(<ι)-1 er-
fullt und damit wiederum insgesamt ⅛ ∈ PBF(⅛ΓDom(⅛)-1).
Zweiter Fall: Sei nun β* ∉ TT([β, α, A(⅛i)]). Mit [β, α, A(⅛i)] = [β*, ζ, [β, α, Δ+]], gilt
dann ζ ∉ FV([β, α, Δ+]). Dann ist [β, α, A(⅛i)] = [β*, ζ, [β, α, Δ+]] = [β, α, Δ+] und damit
mit β ∉ TT(Λ(<y)) ∪ TT(Δ+) wiederum mit Theorem 1-20 A(⅛i) = Δ+, wobei mit ζ ∉
FV([β, α, Δ+]) auch ζ ∉ FV(Δ+). Sei nun β+ ∈ PAR∖TTSEQ(⅛ΓDom(⅛)-1). Mit ζ ∉
FV(Δ+), gilt dann Λ(^i) = Δ+ = [β+, ζ, Δ+] und es gilt: β+ ∉ TTFM({Δ+, A‰m^2)}) und
es gibt kein j ≤ i, so dass β+ ∈ TT(⅛j). Damit ist dann ebenfalls insgesamt auch .ħ ∈
PBF(⅛ΓDom(⅛)-1). Also gilt in beiden Fallen .ħ ∈ PBF(⅛ΓDom(⅛)-1).
Hauptteil: Nun zum Nachweis, dass sich fur die einzelnen Falle AF ... IBF jeweils
ergibt, dass .ħ' ∈ RGS und Dom(VERS(⅛+)) = {(l+1 | l ∈ Dom(VERS(⅛))} ∪ {0}. Zu-
nachst werden SEF, NEF und PBF behandelt. Nach einer Ausschlussannahme fur alle an-
deren Falle kann fur diese Dom(VERS(⅛+)) allein mit c), g) und Theorem 3-25 bestimmt
werden.
(SEF, NEF): Sei nun .ħ ∈ SEF(⅛ΓDom(⅛)-1). Nach Definition 3-2 gibt es dann ein i ∈
Dom(VANS(⅛ΓDom(⅛)-1)), so dass es kein l ∈ Dom(VANS(⅛ΓDom(⅛)-1)) mit i < l ≤
Dom(⅛)-2 gibt und .ħ = ⅛ΓDom(⅛)-1 ∪ {(Dom(⅛)-1, rAlso A(⅛i) →
K(⅛ΓDom(⅛)-1)^l)}. Dann gilt mit a), d) und f): i+1 ∈ Dom(VANS(⅛*)) und es gibt kein
l mit i+1 < l ≤ Dom(⅛)-1 = Dom(⅛*)-1, so dass l ∈ Dom(VANS(⅛*)), und A(⅛*i+1) = [β,
α, A(⅛i)] und K(⅛*) = [β, α, K(⅛ΓDom(⅛)-1)] und .ħ' = ⅛* ∪ {(Dom(⅛), [β, α, rAlso
A(⅛) → K(^Dom(^)-1)π])} =⅞* ∪ {(Dom(M rAlso [β, α, A(⅛)] → [β, α,
K(⅛ΓDom(⅛)-1)]^l)} = ft* ∪ {(Dom(⅛), rAlso A(⅛*i+ι) → K(⅛*)^l)}. Damit ist dann .ħ'
∈ SEF(⅛*) und damit .ħ' ∈ RGS.
Sodann ergibt sich mit Theorem 3-19-(iii), dass VERS(⅛) = VERS(⅛ΓDom(⅛)-1)∖{(j,
ftj) | i ≤ j < Dom(⅛)-1} ∪ {(Dom(⅛)-1, rAlso A(⅛i) → K(⅛ΓDom(⅛)-1)^l)} und dass
VERS(⅛+) = VERS(⅛*)∖{(j, ,ħ +) | i+1 ≤ j < Dom(⅛)} ∪ {(Dom(⅛), rAlso [β, α, A(⅛i)]
→ [β, α, K(⅛ΓDom(⅛)-1)]π)}. Mit Dom(VERS(⅛*)) = {(l+1 | l ∈
Dom(VERS(⅛ΓDom(⅛)-1))} ∪ {0} ergibt sich dann auch Dom(VERS(⅛+)) = {(l+1 | l ∈
Dom(VERS(⅛))} ∪ {0}. Fur den Fall, dass ft ∈ NEF(⅛ΓDom(⅛)-1), zeigt man analog,