178 4 Theoreme zur deduktiven Konsequenzschaft
VERS(ft) = VERS(ftΓDom(ft)-1) и {(Dom(ft)-1, K(ft))} und dass VERS(ft+) =
VERS(ft*) и {(Dom(ft)-1, K(ft+))}. Mit Dom(VERS(ft*)) = Dom(VERS(ftΓDom(ft)-1))
ergibt sich dann Dom(VERS(ft+)) = Dom(VERS(ft)) fur alle verbleibenden Falle.
(AF): Sei nun ft ∈ AF(ftΓDom(ft)-1). Dann ist nach Definition 3-1 ft = ftΓDom(ft)-1 и
{(Dom(ft)-1, rSei A(ftDom(ft)-ι)π). Dann ist mit d) ft+ = ft* и {(Dom(ft)-1, rSei [β*, β,
A(ftDom(ft)-ι)]π)} ∈ AF(ft*) und damit ft+ ∈ RGS.
(SBF, KEF, KBF, BEF, BBF, AEF, ABF, NBF): Sei nun ft ∈ SBF(ftfDom(ft)-1). Dann
gibt es mit Definition 3-3 Α, Β ∈ GFORM, so dass Α, rΑ → IE ∈ VER(ftΓDom(ft)-1)
und ft = ftΓDom(ft)-1 и {(Dom(ft)-1, rAlso Β^l)}. Mit d) gilt dann: ft+ = ft* и
{(Dom(ft)-1, rAlso [β*, β, Β]^l)}. Sodann gibt es mit Α, rΑ → IE ∈ VER(ftΓDom(ft)-1)
und Definition 2-30 i, j ∈ Dom(VERS(ftΓDom(ft)-1)), so dass A(fti) = Α und A(ftj) = rΑ
→ IE. Mit a) und b) ergibt sich dann, dass i, j ∈ Dom(VERS(ft*)) und A(ft*i) = [β*, β,
Α] und A(ft*j) = r[β*, β, Α] → [β*, β, Β]π. Damit gilt dann mit d), dass ft+ = ft* и
{(Dom(ft)-1, rAlso [β*, β, Β]π)} ∈ SBF(ft*) und damit ft+ ∈ RGS. Fur KEF, KBF, BEF,
BBF, AEF, ABF und NBF ist analog vorzugehen.
(UEF): Sei nun ft ∈ UEF(ftΓDom(ft)-1). Dann gibt es nach Definition 3-12 β+ ∈ PAR,
ζ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass [β+, ζ, Δ] ∈ VER(ftΓDom(ft)-1), β+
∉ TTFM({Δ} и VAN(ftΓDom(ft)-1)) und ft = ftΓDom(ft)-1 и {(Dom(ft)-1, rAlso
ΛζΔ^l)}. Dann gilt mit d): ft+ = ft* и {(Dom(ft)-1, [β*, β, rAlso ΛζΔ^l])} = ft* и
{(Dom(ft)-1, rAlso Λζ[β*, β, Δ]π)}. Sodann gibt es mit [β+, ζ, Δ] ∈ VER(ftΓDom(ft)-1)
und Definition 2-30 i ∈ Dom(VERS(ftΓDom(ft)-1), so dass [β+, ζ, Δ] = A(fti). Mit a) und
b) gilt dann, dass i ∈ Dom(VERS(ft*)) und A(ft*j) = [β*, β, A(fti)] = [β*, β, [β+, ζ, Δ]].
Sodann lassen sich mit β+ = β und β+ ≠ β zwei Falle unterscheiden.
Erster Fall: Sei β+ = β. Dann ist A(ft*i) = [β*, β, [β+, ζ, Δ]] = [β*, β, [β, ζ, Δ]] und mit
β+ ∉ TT(Δ) auch β ∉ TT(Δ) und somit mit Theorem 1-24-(ii) A(ft*i) = [β*, β, [β, ζ, Δ]] =
[β*, ζ, Δ]. Mit β ∉ TT(Δ) ist sodann [β*, β, Δ] = Δ und damit K(ft+) = rΛζ[β*, β, Δ]π =
rΛζΔπ. Sodann gilt mit β+ = β und β* ∉ TTSEQ(ft): β, β* ∉ TTFM({Δ} и
VAN(ftΓDom(ft)-1)) und damit mit a) und b) auch β* ∉ TTFM({Δ} и VAN(ft*)). Ware
namlich β* ∈ TTFM({Δ} и VAN(ft*)). Dann ist β* ∉ TT(Δ), da sonst β* ∈ TT(Δ) ⊂
TT(rΛζΔ^l) = TT(K(ft)) ⊂ TTSEQ(ft), was wegen β* ∉ TTSEQ(ft) ausgeschlossen ist.
Also gabe es dann Β ∈ VAN(ft*), so dass β* ∈ TT(Β). Damit gabe es mit Definition
2-31 j ∈ Dom(VANS(ft*)), so dass β* ∈ TT(A(ft*j)). Dann ist mit b) A(ft*j) = [β*, β,
A(ftj)]. Sodann ist mit β* ∉ TTSEQ(ft) auch β* ∉ TT(A(ftj)). Damit gilt mit β* ∈