Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

FV(Δ*) ⊆ {ζ} ∪ X und dass fur alle θ' ∈ GTERM gilt: [θ', ξ, ^rΦ(θo, ... θr-ι)^π] = ^rΦ([θ',
ξ, θo], . [θ', ξ, θr-i]Γ = ^rΦ([θ', ζ, θ*o], . [θ', ζ, θ*r-1])^π = [θ', ζ, ^rΦ(θ*0, . θ*r-1)^π] = [θ',
ζ, Δ*].

Gelte die Behauptung nun fur Δo, Δ1 ∈ FORM und sei Δ ∈ JFORM. Seien {ξ, ζ} ∪ X
⊆ VAR, wobei {ξ, ζ} ∩ X = 0, und FV(Δ) ⊆ {ξ} ∪ X und ζ ∉ TT(Δ). Sei zunachst Δ =
^r—Δ₀^^l. Dann gilt FV(Δ₀) = FV(Δ) ⊆ {ξ} ∪ X und ζ ∉ TT(Δ₀). Dann gibt es nach I.V.
Δ*o ∈ FORM, wobei FV(Δ*o) ⊆ {ζ} ∪ X, so dass fur alle θ' ∈ GTERM gilt: [θ', ξ, Δo] =
[θ', ζ, Δ*_o]. Dann gilt mit Δ* = ^r—Δ*₀^^l, dass FV(Δ*) ⊆ {ζ} ∪ X und dass fur alle θ' ∈
GTERM gilt: [θ', ξ, ` Δ ∣ = ^r-[θ', ξ, Δ0]^π = ^r-[θ', ζ, Δ%]^π = [θ', ζ, ^r-ΔV] = [θ', ζ,
Δ*].

Sei nun Δ = ^r(Δ₀ ψ Δ₁)^^l ∈ JFORM. Dann gilt FV(Δ₀) ⊆ FV(Δ) ⊆ {ξ} ∪ X und ζ ∉
TT(Δ0) und FV(Δ1) ⊆ FV(Δ) ⊆ {ξ} ∪ X und ζ ∉ TT(Δ1). Dann gibt es nach I.V. Δ*0,
Δ*1 ∈ FORM, wobei FV(Δ*0) ⊆ {ζ} ∪ X und FV(Δ*1) ⊆ {ζ} ∪ X, so dass fur alle θ' ∈
GTERM gilt: [θ', ξ, Δ0] = [θ', ζ, Δ*0] und [θ', ξ, Δ1] = [θ', ζ, Δ*1]. Dann gilt mit Δ* =
^r(Δ*0 ψ Δ*ι)^π, dass FV(Δ*) ⊆ {ζ} ∪ X und dass fur alle θ' ∈ GTERM gilt: [θ', ξ, ^r(Δ0 ψ
V) ] = ^r([θ', ξ, Δ0] ψ [θ', ξ, Δι]>- = ^r([θ', ζ, Δ*0] ψ [θ', ζ, Δ*₁]Γ = [θ', ζ, ^r(Δ*0 ψ Δ*₁Γ ] =
[θ', ζ, Δ*].

Sei nun Δ = ^rΠξ'Δ₀^^l ∈ QFORM. Seien {ξ, ζ} ∪ X ⊆ VAR, wobei {ξ, ζ} ∩ X = 0, und
FV(Δ) ⊆ {ξ} ∪ X und ζ ∉ TT(Δ). Dann gilt insbesondere ζ ≠ ξ'. Sei zunachst ξ = ξ'.
Dann ist [θ', ξ, ^rΠξ'Δ0^π ] = ^r∏ξ'Δ0^π fur alle θ' ∈ GTERM und FV(Δ) ⊆ X. Sei dann Δ* =
Δ = ^rΠξ'Δ0^π. Da ζ ∉ TT(Δ) gilt auch [θ', ζ, ^rΠξ⅝^π ] = ^r∏ξ'Δ0^π fur alle θ' ∈ GTERM und
FV(Δ*) = FV(Δ) ⊆ X ⊆ {ζ} ∪ X. Sei nun ξ ≠ ξ'. Dann gilt FV(Δ0) ⊆ FV(Δ) ∪ {ξ'} ⊆
{ξ} ∪ X ∪ {ξ'} und ζ ∉ TT(Δ0). Dann gibt es nach I.V. Δ*0 ∈ FORM, wobei FV(Δ*0) ⊆
{ζ} ∪ X ∪ {ξ'}, so dass fur alle θ' ∈ GTERM gilt: [θ', ξ, Δ0] = [θ', ζ, Δ*0]. Dann gilt mit
Δ* = ^rΠξ'ΔV, dass FV(Δ*) ⊆ {ζ} ∪ X und dass fur alle θ' ∈ GTERM gilt: [θ', ξ,
^rΠξ'Δ0^π] = ^rΠξ'[θ', ξ, Δ0]^π = ^r∏ξ'[θ', ζ, Δ%Γ = [θ', ζ, ^r∏ξ'ΔV] = [θ', ζ, Δ*]. ■

<<   35   36   37   38   39   40   41   >>

More intriguing information