186 4 Theoreme zur deduktiven Konsequenzschaft
Ausschlussannahme: Fur die verbleibenden Schritte sei S ∉ SEF(SΓDom(S)-1) ∪
NEF(SPDom(S)-1) ∪ PBF(SfDom(S)-1). Mit g) ist dann S+ ∉ SEF(S*) ∪ NEF(S*) ∪
PBF(S*). Damit ergibt sich fur die folgenden Falle dann jeweils mit Theorem 3-25, dass
VERS(S) = VERS(SPDom(S)-I) ∪ {(Dom(S)-1, K(S))} und dass VERS(S+) =
VERS(S*) ∪ {(Dom(S), K(S*))}. Mit Dom(VERS(S*)) = {(l+1 | l ∈
Dom(VERS(SΓDom(S)-1))} ∪ {0} ergibt sich dann Dom(VERS(S+)) = {(l+1 | l ∈
Dom(VERS(S))} ∪ {0} fur alle verbleibenden Falle.
(AF): Sei nun S ∈ AF(SPDom(S)-1). Nach Definition 3-1 ist dann S = SΓDom(S)-1 ∪
{(Dom(S)-1, rSei A(SDom(S)-1)n). Dann ist mit f) S+ = S* ∪ {(Dom(S), rSei [β, α,
A(SDom(S)-1)]-1)} ∈ AF(S*) und damit S+ ∈ RGS.
(SBF, KEF, KBF, BEF, BBF, AEF, ABF, NBF): Sei nun S ∈ SBF(SPDom(S)-1). Nach
Definition 3-3 gibt es dann Α, Β ∈ GFORM, so dass Α, rΑ → 1Γ ∈ VER(SΓDom(S)-1)
und S = SΓDom(S)-1 ∪ {(Dom(S)-1, rAlso Β^l)}. Mit f) gilt dann: S+ = S* ∪
{(Dom(S), rAlso [β, α, Β]^l)}. Sodann gibt es mit Α, rΑ → 1Γ ∈ VER(SΓDom(S)-1)
und Definition 2-30 i, j ∈ Dom(VERS(SΓDom(S)-1)), so dass A(Si) = Α und A(Sj) = rΑ
→ 1Γ. Mit c) und d) ergibt sich dann, dass i+1, j+1 ∈ Dom(VERS(S*)) und A(S*i+1) =
[β, α, Α] und A(S*j+1) = r[β, α, Α] → [β, α, Β]^l. Damit gilt dann S+ = S* ∪ {(Dom(S),
rAlso [β, α, Β]π)} ∈ SBF(S*) und damit S+ ∈ RGS. Fur KEF, KBF, BEF, BBF, AEF,
ABF und NBF ist analog vorzugehen.
(UEF): Sei nun S ∈ UEF(SΓDom(S)-1). Nach Definition 3-12 gibt es dann β* ∈ PAR,
ζ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass [β*, ζ, Δ] ∈ VER(SΓDom(S)-1), β*
∉ TTFM({Δ} ∪ VAN(SΓDom(S)-1)) und S = SΓDom(S)-1 ∪ {(Dom(S)-1, rAlso
ΛζΔ^l)}. Dann gilt mit f): S+ = S* ∪ {(Dom(S), [β, α, rAlso ΛζΔ^l])} = S* ∪
{(Dom(S)-1, rAlso Λζ[β, α, Δ]^l)}. Sodann gibt es mit [β*, ζ, Δ] ∈ VER(SΓDom(S)-1)
und Definition 2-30 ein i ∈ Dom(VERS(SΓDom(S)-1)), so dass [β*, ζ, Δ] = A(Si). Mit c)
und d) gilt dann, dass i+1 ∈ Dom(VERS(S*)) und A(S*i+1) = [β, α, A(Si)] = [β, α, [β*, ζ,
Δ]]. Sodann lassen sich mit β* ≠ β und β* = β zwei Falle unterscheiden.
Erster Fall: Sei β* ≠ β. Dann ist mit Theorem 1-25-(ii): A(S*i+1) = [β, α, [β*, ζ, Δ]] =
[β*, ζ, [β, α, Δ]]. Sodann ist K(S+) = rΛζ[β, α, Δ]π. Ware β* ∈ TTFM({[β, α, Δ]} ∪
VAN(S*)). Da β* ≠ β und β* ∉ TT(Δ) ist zunachst β* ∉ TT([β, α, Δ]). Also ware β* ∈
TTFM(VAN(S*)) und somit gabe es mit Definition 2-31 ein j ∈ Dom(VANS(S*)), so
dass β* ∈ TT(A(S*j)). Mit S*0 ∈ FSATZ ist j ≠ 0. Da mit d) dann A(S*j) = [β, α,
A(Sj-1)] und β* ≠ β ware damit aber bereits β* ∈ TT(A(Sj-1)). Mit c) und d) ergabe sich