Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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(SD_om(_S)_-1)ⁿ). Dann ist mit f) S⁺ = S* ∪ {(Dom(S), ^rSei [β, α,
A(S_Dom(_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₊₁) =
[β, α, Α] und A(S*j₊₁) = 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+₁) = [β, α, A(Si)] = [β, α, [β*, ζ,
Δ]]. Sodann lassen sich mit β* ≠ β und β* = β zwei Falle unterscheiden.

Erster Fall: Sei β* ≠ β. Dann ist mit Theorem 1-25-(ii): A(S*i+₁) = [β, α, [β*, ζ, Δ]] =
[β*, ζ, [β, α, Δ]]. 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*₀ ∈ 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

<<   159   160   161   162   163   164   165   >>

More intriguing information