Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

..., ξk-ι} = FV(^rΦ(θ'0, ., θ' ) ) ∪ {ξo, ., ξk-ι}. Sodann ist TT(^rΦ(θ⁺o, ., θ⁺r-ι)^π) ∩
{θo, ., Θk-1} = ∪{TT(θ⁺i) | i < r} ∩ {θo, ., θk-ι} = ∪{TT(θ⁺i) ∩ {θo, ., Θk-1} | i < r} = 0.

Gelte die Behauptung nun fur Δ₀, Δ₁ ∈ FORM und sei Δ = ^r—Δ₀^^l ∈ JFORM. Sei nun k
∈ N∖{0}, {θo, ., θk-ι} ⊆ GTERM und {ξo, ., ξ_w} ⊆ VARTTA  Δ ), wobei ξ ≠ ξj

fur alle i, j < k mit i ≠ j. Mit TT(Δ₀) = TT(^r—Δ₀^^l) gilt dann {ξ₀, ., ξ_k-1} ⊆ VAR∖TT(Δ₀).
Dann gibt es nach I.V. fur Δ₀ ein Δ⁺₀ ∈ FORM, so dass Δ₀ = [<θ₀, ., θ_k-1), <ξ₀, ., ξ_k-1),
Δ⁺0] und FV(Δ⁺0) ⊆ FV(Δ0) ∪ {ξ0, ., ξk-1} und TT(Δ⁺0) ∩ {θ0, ., θk-1} = 0. Dann ist
Γ-Δ(√ = r-[<θ₀, ., Θk-1), (ξ₀, ., ξk-i), Δ⁺αΓ = [<θo, ., θk-1), <ξ1, ., ξk-1), ^r-Δ⁺0^π]. So-
dann ist FV(^r-.Δ+A) = FV(Δ⁺₀) und daher FV(^r-Δ'Δ) ⊆ FV(Δ₀) ∪ {ξ₀, ., ξ_k-1} =
FV(^r- Δ ) ∪ {ξ0, ., ξk-ι}. Sodann ist TTΔ Δ ) ∩ {θ0, ., θk-1} = TT(Δ⁺0) ∩ {θ0, .,
θk-1} = 0.

Sei nun Δ = ^r(Δ₀ ψ Δ₁)^^l ∈ JFORM. Sei nun k ∈ N∖{0}, {θ₀, ., θ_k-1} ⊆ GTERM und
{ξ₀, ., ξ_k-1} ⊆ VAR∖TT(^r(Δ₀ ψ Δ₁)^^l), wobei ξ_i ≠ ξj fur alle i, j < k mit i ≠ j. Mit TT(Δ₀)
∪ TT(Δ1) = TT(^r(Δ0 ψ Δι)^π) gilt dann {ξ0, ., ξk-ι} ⊆ VAR∖(TT(Δ0) ∪ TT(Δι)). Dann
gibt es nach I.V. fur Δ0, Δ1 jeweils ein Δ⁺0, Δ⁺1 ∈ FORM, so dass fur l < 2: Δl = [<θ0, .,
θk-1), <ξ0, ., ξk-1), Δ⁺1] und FV(Δ⁺1) ⊆ {ξ0, ., ξk-1} ∪ FV(Δ1) und TT(Δ⁺ι) ∩ {θ0, ., θk-1}
= 0. Dann ist ^r(Δ0 ψ Δ1)" = ^r([<θ0, ., θk-1), <ξ0, ., ξk-1), Δ⁺0] ψ [<θ0, ., θk-1), <ξ1, ., ξk-1),
Δ⁺1])^π = [<θ0, ., θk-1), <ξ0, ., ξk-1), ^r(Δ⁺0 ψ Δ⁺1)^π]. Sodann ist FV(^r(Δ% ψ Δ∖)^π) =
FV(Δ⁺0) ∪ FV(Δ⁺1) und daher FV(^r(Δ⁺0 ψ Δ⁺1)^π) ⊆ FV(Δ0) ∪ FV(Δ1) ∪ {ξ0, ., ξk-1} =
FV(^r(Δ0 ψ Δ1)") ∪ {ξ0, ., ξk-1}. Sodann ist TT(^r(Δ⁺0 ψ Δ∖)") ∩ {θ0, ., θk-1} = (TT(Δ⁺0)
∩ {θ0, ., θk-1}) ∪ (TT(Δ⁺1) ∩ {θ0, ., θk-1}) = 0.

Sei nun Δ = ^rΠζΔ₀^^l ∈ QFORM und weiter k ∈ N∖{0}, {θ₀, ., θ_k-1} ⊆ GTERM und
{ξ₀, ., ξ_k-1} ⊆ VAR∖TT(^rΠζΔ₀^^l), wobei ξi ≠ ξj fur alle i, j < k mit i ≠ j. Damit gilt ins-
besondere ζ ∉ {ξ0, ., ξk-1}. Sodann gilt mit TT(Δ0) ⊆ TT(^rΠζΔ0^¹), dass {ξ0, ., ξk-1} ⊆
VAR∖TT(Δ₀). Damit gibt es nach I.V. fur Δ₀ ein Δ⁺₀ ∈ FORM, so dass Δ₀ = [<θ₀, ., θ_k-1),
<ξ0, ., ξk-1), Δ⁺0] und FV(Δ⁺0) ⊆ {ξ0, ., ξk-1} ∪ FV(Δ0) und TT(Δ⁺0) ∩ {θ0, ., θk-1} = 0.
Da ζ ∉ {ξ0, ., ξk-1} ist dann 'ID = ^rΠζ[‰ ., θ_w>, <ξ0, ., ξk-1), Δ%Γ = [<θ0, .,
θk-1), <ξ0, ., ξk-1), ^r∏ζ∆V]∙ Sodann ist FV(^rΠζΔ%^π) = FV(Δ⁺0)∖{ζ} ⊆ (FV(Δ0)∖{ζ}) ∪
{ξ₀, ., ξ_k-1} = FV(^rΠζΔ₀^^l) ∪ {ξ₀, ., ξ_k-1}. Sodann ist mit VAR ∩ GTERM = 0 schlieβ-
lich TT(^rΠζΔ⁺0^π) ∩ {θ0, ., θk-1} = (TT(Δ⁺0) ∪ {ζ}) ∩ {θ0, ., θk-1} = 0. ■

<<   <   33   34   35   36   37   38   39   >   >>