Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

180   4 Theoreme zur deduktiven Konsequenzschaft

auch [β*, β, θ] ∈ GTERM und mit FV(Δ) ⊆ {ζ} auch FV([β*, β, Δ]) ⊆ {ζ}. Damit ist
dann insgesamt ft⁺ ∈ UBF(ft*) ⊆ RGS.

(PEF): Sei nun ft ∈ PEF(ftΓDom(ft)-1). Dann gibt es nach Definition 3-14 θ ∈
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 d) ist dann
ft⁺ = ft* ∪ {(Dom(ft)-1, [β*, β, rAlso VζΔ^^l])} = ft* ∪ {(Dom(ft)-1, rAlso Vζ[β*, β,
Δ]^^l)}. Sodann gibt es mit [θ, ζ, Δ] ∈ VER(ftΓDom(ft)-1) nach Definition 2-30 i ∈
Dom(VERS(ftΓDom(ft)-1)), so dass A(ft_i) = [θ, ζ, Δ]. Mit a) und b) ist dann i ∈
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
insgesamt ft⁺ ∈ PEF(ft*) ⊆ RGS.

(IEF): Sei nun ft ∈ IEF(ftΓDom(ft)-1). Mit Definition 3-16 gibt es dann θ ∈ GTERM,
so dass ft = ftΓDom(ft)-1 ∪ {(Dom(ft)-1, rAlso θ = θ^^l)}. Dann ist mit d) ft⁺ = ft* ∪
{(Dom(ft)-1, [β*, β, rAlso θ = θ^π])} = ft* ∪ {(Dom(ft)-1, rAlso [β*, β, θ] = [β*, β,
θ]^^l)}, wobei mit θ ∈ GTERM auch [β*, β, θ] ∈ GTERM. Damit ist dann ft⁺ ∈ IEF(ft*)
⊆ RGS.

(IBF): Sei nun ft ∈ IBF(ftΓDom(ft)-1). Dann gibt es mit Definition 3-17 θ₀, θ₁ ∈
GTERM, ζ ∈ VAR und Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass rθ₀ = θ₁^^l, [θ₀, ζ, Δ] ∈
VER(ftΓDom(ft)-1), und ft = ftΓDom(ft)-1 ∪ {(Dom(ft)-1, rAlso [θ₁, ζ, Δ]^^l)}. Dann ist
mit d) ft⁺ = ft* ∪ {(Dom(ft)-1, [β*, β, rAlso [θ₁, ζ, Δ]^^l])} = ft* ∪ {(Dom(ft)-1, rAlso
[β*, β, [θ1, ζ, Δ]]^π)}. Sodann gibt es mit ^γΘo = θΓ, [Θo, ζ, Δ] ∈ VER(ftΓDom(ft)-1) und
Definition 2-30 i, j ∈ Dom(VERS(ftΓDom(ft)-1)), so dass A(ft_i) = rθ₀ = θ₁^^l und A(ft_j) =
[θ₀, ζ, Δ]. Dann gilt mit a) und b): i, j ∈ Dom(VERS(ft*)) und A(ft*_i) = [β*, β, A(ft_i)] =
[β*, β, Γθo = θ14 = r[β*, β, Θo] = [β*, β, θɪ]ɔ und A(ft*j) = [β*, β, A(ftj)]. Dann ist mit
Theorem 1-26-(ii) A(ft*j) = [β*, β, A(ftj)] = [β*, β, [Θo, ζ, Δ]] = [[β*, β, Θo], ζ, [β*, β, Δ]]
und K(ft⁺) = [β*, β, [Θi, ζ, Δ]] = [[β*, β, Θi], ζ, [β*, β, Δ]], wobei mit Θo, Θi ∈ GTERM
auch [β*, β, θo], [β*, β, θ1] ∈ GTERM und mit FV(Δ) ⊆ {ζ} auch FV([β*, β, Δ]) ⊆ {ζ}.
Damit gilt dann insgesamt ft⁺ ∈ IBF(ft*) ⊆ RGS. ■

Das folgende Theorem dient der Vorbereitung des Generalisierungstheorems (Theorem
4-24). Der Beweis ahnelt stark dem Beweis zu Theorem 4-8.

<<   <   153   154   155   156   157   158   159   >   >>