Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 179

TT(A(S*j)) und A(S*j) = [β*, β, A(Sj)] dann aber β ∈ TT(A(^_j∙)). Sodann ergibt sich mit
a) und b) aus j ∈ Dom(VANS(S*)), dass j ∈ Dom(VANS(STDom(S)-1)) und somit
A(Sj) ∈ VAN(STDom(S)-1). Damit ware aber β ∈ TTFM(VAN(STDom(S)-1)) und an-
dererseits nach Voraussetzung β = β⁺ ∉ TTFM(VAN(STDom(S)-1)). Widerspruch! Also
ist β* ∉ TTFM({Δ} ∪ VAN(S*)). Da sodann A(S*i) = [β*, ζ, Δ], i ∈ Dom(VERS(S*))
und K(S⁺) = ^rΛζΔ^^l ist damit dann insgesamt S⁺ ∈ UEF(S*).

Zweiter Fall: Sei nun β⁺ ≠ β. Dann lassen sich mit β⁺ ≠ β* und β⁺ = β* zwei Unterfalle
unterscheiden. Erster Unterfall: Sei β⁺ ≠ β*. Dann ist mit Theorem 1-25-(ii) und β⁺ ≠ β:
A(S*i) = [β*, β, [β⁺, ζ, Δ]] = [β⁺, ζ, [β*, β, Δ]]. Sodann ist K(S⁺) = ^rΛζ[β*, β, ΔΓ. Ange-
nommen β⁺ ∈ 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)). Da mit b) A(S*j) = [β*, β,
A(Sj)] und β⁺ ≠ β*, ware damit aber bereits β⁺ ∈ TT(A(Sj)). Mit a) und b) ergabe sich
sodann aus j ∈ Dom(VANS(S*)), dass j ∈ Dom(VANS(STDom(S)-I)) und somit A(Sj)
∈ VAN(STDom(S)-I)) und damit β⁺ ∈ TTFM(VAN(STDom(S)-1)) und andererseits
nach Voraussetzung β⁺ ∉ TTFM(VAN(STDom(S)-I)). Widerspruch! Also ist β⁺ ∉
TTFM({[β*, β, Δ]} ∪ VAN(S*)) und damit wiederum insgesamt S⁺ ∈ UEF(S*).

Zweiter Unterfall: Sei nun β⁺ = β*. Dann ist ζ ∉ FV(Δ), da sonst β* ∈ TT([β⁺, ζ, Δ]) ⊆
TTSEQ(S). Damit ist dann [β⁺, ζ, Δ] = Δ und damit A(S*i) = [β*, β, [β⁺, ζ, Δ]] = [β*, β,
Δ] und sodann ist K(S⁺) = ^rΛζ[β*, β, Δ]^^l. Sei nun в§ ∈ PAR∖TTSEQ(S*). Dann ist mit ζ
∉ FV(Δ) auch ζ ∉ FV([β*, β, Δ]) und damit A(S*i) = [β*, β, Δ] = [β^δ, ζ, [β*, β, Δ]] und
es gilt: в§ ∉ TTFM({[β*, β, Δ]} ∪ VAN(S*)) und damit wiederum insgesamt S⁺ ∈
UEF(S*). Damit gilt in beiden Unterfallen und somit insgesamt in beiden Fallen, dass S⁺
∈ UEF(S*) ⊆ RGS.

(UBF): Sei nun S ∈ UBF(STDom(S)-I). Dann gibt es nach Definition 3-13 θ ∈
GTERM, ζ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass ^rΛζΔ^π ∈
VER(STDom(S)-I), und S = STDom(S)-I ∪ {(Dom(S)-1, ^rAlso [θ, ζ, Δ]^π)}. Mit d) ist
dann S⁺ = S* ∪ {(Dom(S)-1, [β*, β, rAlso [θ, ζ, Δ]^π])} = S* ∪ {(Dom(S)-1, rAlso [β*,
β, [θ, ζ, Δ]]^^l)}. Sodann gibt es mit rΛζΔ^^l ∈ VER(STDom(S)-1) nach Definition 2-30 i ∈
Dom(VERS(STDom(S)-1)), so dass A(Si) = rΛζΔ^^l. Mit a) und b) ist dann i ∈
Dom(VERS(S*)) und A(S*i) = [β*, β, rΛζΔ^^l ] = rΛζ[β*, β, Δ]^^l. Sodann ist mit Theorem
1-26-(ii) K(S⁺) = [β*, β, [θ, ζ, Δ]] = [[β*, β, θ], ζ, [β*, β, Δ]], wobei mit θ ∈ GTERM

<<   152   153   154   155   156   157   158   >>

More intriguing information