Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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(ftD_om(_ft)_-ι)^π). Dann ist mit d) ft⁺ = ft* и {(Dom(ft)-1, ^rSei [β*, β,
A(ftD_om(_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(ft_i) = Α 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(ft_i). Mit a) und
b) gilt dann, dass i ∈ Dom(VERS(ft*)) und A(ft*_j) = [β*, β, A(ft_i)] = [β*, β, [β⁺, ζ, Δ]].
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(ft_j)). Damit gilt mit β* ∈

<<   151   152   153   154   155   156   157   >>

More intriguing information