Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 187

sodann aus j ∈ Dom(VANS(ft*)), dass j-1 ∈ Dom(VANS(ftΓDom(ft)-1)) und somit
A(ft_j-ι) ∈ VAN(ftΓDom(ft)-1) und β* ∈ TTFM(VAN(ftΓDom(ft)-1)) und andererseits
nach Voraussetzung β* ∉ TTFM(VΛN(ftfDom(ft)-1)). Widerspruch! Also ist β* ∉
TTFM({[β, α, Δ]} ∪ VAN(ft*)) und damit ft⁺ ∈ UEF(ft*).

Zweiter Fall: Sei nun β* = β. Dann ist ζ ∉ FV(Δ), da sonst β ∈ TT([β*, ζ, Δ]) ⊆
TTSEQ(ft). Damit ist dann [β*, ζ, Δ] = Δ und damit A(ft*_i+ι) = [β, α, [β*, ζ, Δ]] = [β, α,
Δ] und sodann ist K(ft⁺) = ^rΛζ[β, α, Δ]^^l. Sei nun β⁺ ∈ PAR∖TTSEQ(ft*). Dann ist mit ζ
∉ FV(Δ) auch ζ ∉ FV([β, α, Δ]) und damit A(ft*i₊ι) = [β, α, Δ] = [β⁺, ζ, [β, α, Δ]] und es
gilt: β⁺ ∉ TTFM({[β, α, Δ]} ∪ VAN(ft*)) und damit wiederum ft⁺ ∈ UEF(ft*). Damit
gilt in beiden Fallen, dass ft⁺ ∈ UEF(ft*) ⊆ RGS.

(UBF): Sei nun ft ∈ UBF(ftΓDom(ft)-1). Nach Definition 3-13 gibt es dann θ ∈
GTERM, ζ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass ^rΛζΔ^π ∈
VER(ftΓDom(ft)-1) und ft = ftΓDom(ft)-1 ∪ {(Dom(ft)-1, ^rAlso [θ, ζ, Δ]^^l)}. Mit f) ist
dann ft⁺ = ft* ∪ {(Dom(ft), [β, α, rAlso [θ, ζ, Δ]^^l])} = ft* ∪ {(Dom(ft), rAlso [β, α, [θ,
ζ, Δ]]^^l)}. Sodann gibt es mit rΛζΔ^^l ∈ VER(ftΓDom(ft)-1) nach Definition 2-30 ein i ∈
Dom(VERS(ftΓDom(ft)-1)), so dass A(ft_i) = rΛζΔ^^l. Mit c) und d) ist dann i+1 ∈
Dom(VERS(ft*)) und A(ft*i₊ι) = [β, α, rΛζΔ^π] = rΛζ[β, α, Δ]^^l. Sodann ist mit Theorem
1-26-(ii) K(ft⁺) = [β, α, [θ, ζ, Δ]] = [[β, α, θ], ζ, [β, α, Δ]], wobei mit θ ∈ GTERM auch
[β, α, θ] ∈ GTERM und mit FV(Δ) ⊆ {ζ} auch FV([β, α, Δ]) ⊆ {ζ}. Damit ist dann ins-
gesamt ft⁺ ∈ UBF(ft*) ⊆ RGS.

(PEF): Sei nun ft ∈ PEF(ftΓDom(ft)-1). Nach Definition 3-14 gibt es dann θ ∈
GTERM, ζ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass [θ, ζ, Δ] ∈
VER(ftΓDom(ft)-1) und ft = ftΓDom(ft)-1 ∪ {(Dom(ft)-1, rAlso VζΔ^^l)}. Mit f) ist dann
ft⁺ = ft* ∪ {(Dom(ft), [β, α, rAlso VζΔ^^l])} = ft* ∪ {(Dom(ft), rAlso Vζ[β, α, Δ]^^l)}. So-
dann gibt es mit [θ, ζ, Δ] ∈ VER(ftΓDom(ft)-1) nach Definition 2-30 ein i ∈
Dom(VERS(ftΓDom(ft)-1)), so dass A(ft_i) = [θ, ζ, Δ]. Mit c) und d) ist dann i+1 ∈
Dom(VERS(ft*)) und A(ft*_i+ι) = [β, α, A(ft_i)]. Dann ist mit Theorem 1-26-(ii) A(ft*i₊ι)
= [β, α, A(fti)] = [β, α, [θ, ζ, Δ]] = [[β, α, θ], ζ, [β, α, Δ]], wobei mit θ ∈ GTERM auch [β,
α, θ] ∈ GTERM und mit FV(Δ) ⊆ {ζ} auch FV([β, α, Δ]) ⊆ {ζ}. Damit ist dann insge-
samt ft⁺ ∈ PEF(ft*) ⊆ RGS.

(IEF): Sei nun ft ∈ IEF(ftΓDom(ft)-1). Nach Definition 3-16 gibt es dann θ ∈ GTERM,
so dass ft = ftΓDom(ft)-1 ∪ {(Dom(ft)-1, rAlso θ = θ^^l)}. Dann ist mit f) ft⁺ = ft* ∪

<<   160   161   162   163   164   165   166   >>

More intriguing information