176 4 Theoreme zur deduktiven Konsequenzschaft
Damit ist dann ebenfalls insgesamt auch ft ∈ PBF(ftΓDom(ft)-1). Also gilt in beiden
Unterfallen und damit insgesamt in beiden Fallen, dass ft ∈ PBF(ftΓDom(ft)-1).
Hauptteil: Nun zum Nachweis, dass sich fur die einzelnen Falle AF ... IBF jeweils
ergibt, dass ft+ ∈ RGS und Dom(VERS(ft+)) = Dom(VERS(ft)). Zunachst werden SEF,
NEF und PBF behandelt. Nach einer Ausschlussannahme fur alle anderen Falle kann
dann fur diese mit a), e) und Theorem 3-25 sofort Dom(VERS(ft+)) bestimmt werden.
(SEF, NEF): Sei nun ft ∈ SEF(ftΓDom(ft)-1). Dann gibt es nach Definition 3-2 i ∈
Dom(VANS(ftΓDom(ft)-1)), so dass es kein l ∈ Dom(VANS(ftΓDom(ft)-1)) mit i < l ≤
Dom(ft)-2 gibt und ft = ftΓDom(ft)-1 и {(Dom(ft)-1, rAlso A(fti) →
K(ftΓDom(ft)-1)^l)}. Dann gilt mit a), b) und d): i ∈ Dom(VANS(ft*)) und es gibt kein l
mit i < l ≤ Dom(ft)-2, so dass l ∈ Dom(VANS(ft*)), und A(ft*i) = [β*, β, A(fti)] und
K(ft*) = [β*, β, K(ftΓDom(ft)-1)] und ft+ = ft* и {(Dom(ft)-1, [β*, β, rAlso A(fti) →
K(ftΓDom(ft)-1)^l ])}= ft* и {(Dom(ft)-1, rAlso A(ft*i) → K(ft*)^l)}. Damit ist dann ft+
∈ SEF(ft*) und damit ft+ ∈ RGS.
Sodann ergibt sich mit Theorem 3-19-(iii), dass VERS(ft) = VERS(ftΓDom(ft)-1)∖{(j,
ftj) | i ≤ j < Dom(ft)-1} и {(Dom(ft)-1, rAlso A(fti) → K(ftΓDom(ft)-1)^l)} und dass
VERS(ft+) = VERS(ft*)∖{(j, ft+j) | i ≤ j < Dom(ft)-1} и {(Dom(ft)-1, rAlso [β*, β,
A(fti)] → [β*, β, K(ftΓDom(ft)-1)]π)}. Mit Dom(VERS(ft*)) =
Dom(VERS(ftΓDom(ft)-1)) ergibt sich dann auch Dom(VERS(ft+)) = Dom(VERS(ft)).
Fur den Fall, dass ft ∈ NEF(ftΓDom(ft)-1), zeigt man analog, dass dann auch ft+ ∈
NEF(ft*) ⊆ RGS und Dom(VERS(ft+)) = Dom(VERS(ft)).
(PBF): Sei nun ft ∈ PBF(ftΓDom(ft)-1). Dann gibt es nach Definition 3-15 β+ ∈ PAR, ζ
∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊂ {ζ}, und i ∈ Dom(VERS(ftΓDom(ft)-1)), so dass
A(fti) = r√ζΔπ, A(fti+1) = [β+, ζ, Δ], wobei i+1 ∈ Dom(VANS(ftΓDom(ft)-1)), β+ ∉
TTFM({Δ, A(ftDom(ft)-2)}), es kein j ≤ i gibt, so dass β+ ∈ TT(ftj), es kein l mit i+1 < l ≤
Dom(ft)-2 gibt, so dass l ∈ Dom(VANS(ftΓDom(ft)-1)) und ft = ftΓDom(ft)-1 и
{(Dom(ft)-1, rAlso A(ft∏om(ft)-2)π)}.
Damit ergibt sich dann mit a), b) und d) zunachst: i ∈ Dom(VERS(ft*)) und A(ft*i) =
[β*, β, A(ft,;)] = [β*, β, r√ζΔπ] = r√ζ[β*, β, Δ]π, i+1 ∈ Dom(VANS(ft*)) und A(ft*+1) =
[β*, β, A(fti+1)] = [β*, β, [β+, ζ, Δ]], K(ft*) = A(ft*Dom(ft)-2) = [β*, β, A(ftDom(ft)-2)] und ft +
= ft* и {(Dom(ft)-1, [β*, β, rAlso K(ftΓDom(ft)-1)^l])} = ft* и {(Dom(ft)-1, rAlso
K(ft*)]^l)} und es gibt kein l mit i+1 < l ≤ Dom(ft)-2, so dass l ∈ Dom(VANS(ft*)). So-
dann lassen sich mit β+ = β und β+ ≠ β zwei Falle unterscheiden.