Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

30    1 Zum grammatischen Rahmen

Gelte die Behauptung nun fur θ'₀, ., θ'_r-1 ∈ TERM und sei θ = ^rφ(θ'₀, ... θ'_r-1)^^l ∈
FTERM. Sei nun k ∈ N∖{0}, {θo, ., θ_w} ⊆ GTERM und {ξo, ., ξk-ι} ⊆ VAR∖TT(θ),
wobei ξi ≠ ξj fur alle i, j < k mit i ≠ j. Mit U {TT(θ'_i) | i < r} ⊆ TT(θ), gilt dann fur alle i <
r, dass {ξ₀, ., ξ_k-1} ⊆ VAR∖TT(θ'i). Damit gibt es nach I.V. fur jedes θ'i (i < r) ein θ⁺i ∈
TERM, so dass θ'i = [<θo, ., θk-ι>, <ξ₁, ., ξ_w>, θ⁺i] und FV(θ⁺i) ⊆ {ξo, ., ξk-ι} ∪ FV(θ'i)
und TT(θ⁺i) ∩ {θ₀, ., θ_k-1} = 0. Dann gibt es kein i < k, so dass ^rφ(θ'₀, . θ'_r-1)^^l = θi,
oder es gibt ein i < k, so dass ^rφ(θ'₀, . θ'_r-1)^^l = θi. Im ersten Fall ist ^rφ(θ'₀, . θ'_r-1)^^l =
^rφ([<θo, ., θk-ι>, <ξ0, ., ξk-ι>, θ⁺0], ., [<θ0, ., θk-ι>, <ξ0, ., ξk-ι>, θ⁺r-ι])^π = [<θ0, ., θk-ι>,
<ξ0, ., ξk-ι>, ^rφ(θ⁺0, ., θ⁺r-ι)^π]. Sodann ist FV(^rφ(θ⁺0, ., θ⁺r-ι>^π) = U JFV(O) | i < r}
und somit mit I.V. FV(^rφ(θ⁺0, ., θ⁺r-ι)^π) ⊆ U{FV(θ'i) | i < r} ∪ {ξ0, ., ξk-ι} =
FV(^rφ(θ'₀, ., θ'_r-1)^^l) ∪ {ξ₀, ., ξ_k-1}. Sodann ist nach Fallannahme und I.V. TT(^rφ(θ⁺₀,
., θ⁺r-ι)^π) ∩ {θ0, ., θk-ι} = ({^rφ(θ⁺0, ., θ⁺r-ι)^π} ∪ U{TT(θ⁺i) | i < r}) ∩ {θ0, ., θk-ι} =
({^rφ(θ⁺0, ., θ⁺r-ι)^π} ∩ {θ0, ., θk-ι}) ∪ (U{TT(θ⁺i) | i < r} ∩ {θ0, ., θk-ι}) = 0 ∪
U{TT(θ⁺i) ∩ {θ₀, ., θ_k-1} | i < r} = 0. Im zweiten Fall ist dann fur ein i < k ^rφ(θ'₀, .
θ'r-ι)^^, = [<θ0, ., θi>, <ξ0, ., ξi>, ξi]. Wegen ξi ≠ ξj fur alle i, j < k mit i ≠ j, gilt aber auch
^rφ(θ'0, . θ'r-ι)^π = [<θ0, ., θi>, <ξ0, ., ξi>, ξi] = [<θ0, ., θk-ι>, <ξ0, ., ξk-1>, ξi] und FV(ξi)
⊆ {ξ0, ., ξk-ι} ∪ FV(^rφ(θ'0, . θ'r-ι)^π) und wegen ξi ∉ GTERM auch TT(ξi) ∩ {θ0, .,
θk-1} = 0. ■

Theorem 1-16. Basen fur die Substitution von geschlossenen Termen in Formeln

Wenn Δ ∈ FORM, k ∈ N∖{0},{θ0, ., θk-ι} ⊆ GTERM und {ξ0, ., ξk-ι} ⊆ VAR∖TT(Δ), wo-
bei ξi ≠ ξj fur alle i, j < k mit i ≠ j, dann gibt es ein Δ⁺ ∈ FORM, wobei FV(Δ⁺) ⊆ {ξ0, ., ξk-1}
∪ FV(Δ) und TT(Δ⁺) ∩ {θ0, ., θk-ι} = 0, so dass Δ = [<θ0, ., θk-ι>, <ξ0, ., ξk-ι>, Δ⁺].

Beweis: Durch Induktion uber den Formelaufbau von Δ. Sei Δ = ^rΦ(θ'₀, . θ'_r-1)^^l ∈
AFORM. Sei nun k ∈ N\{0}, {θ0, ., θk-1} ⊆ GTERM und {ξ0, ., ξk-1} ⊆
VARVΓT(^rΦ(θ'₀, . θ'_r-1)^^l), wobei ξ_i ≠ ξj fur alle i, j < k mit i ≠ j. Mit U {TT(θ'i) | i < r} =
TT(^rΦ(θ'₀, . θ'_r-1)^π), gilt dann fur alle i < r, dass {ξ₀, ., ξ_k-1} ⊆ VAR∖TT(θ'i). Dann
gibt es nach Theorem 1-15 fur jedes θ'i (i < r) ein θ⁺i ∈ TERM, so dass θ'i = [<θ0, ., θk-1>,
<ξ0, ., ξk-1>, θ⁺i] und FV(θ⁺i) ⊆ {ξ0, ., ξk-1} ∪ FV(θ'i) und TT(θ⁺i) ∩ {θ0, ., θk-1} = 0.
Dann ist ^rΦ(θ'0, . θ'r-ι)^π = ^rΦ([(θ0, ., θk-ι>, <ξ0, ., ξk-ι>, θ⁺0], ., [<θ0, ., θk-ι>, <ξ0, .,
ξk-ι>, θ⁺r-ι])^π = [<θ0, ., θk-ι>, <ξ0, ., ξk-ι>, ^rΦ(θ⁺0, ., θ⁺r-ι)^π]. Sodann ist FV(^rΦ(θ⁺0, .,
θ⁺r-ι)^π) = U{FV(θ⁺i) | i < r} und daher FV(^rΦ(θ⁺0, ., θ⁺r-ι)^π) ⊆ U{FV(θ'i) | i < r} ∪ {ξ0,

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