Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

Zu (ii): Sei Δ ∈ FORM. Der Beweis wird mittels Induktion uber den Formelaufbau von
Δ gefuhrt. Sei Δ = ^rΦ(θ₀, ., θ_r-1)^^l ∈ AFORM. Der Fall verlauft analog zum FTERM-
Fall unter Verwendung von (i).

Gelte die Behauptung nun fur Δ₀, Δ₁ ∈ FORM und sei Δ = ^r—Δ₀^^l ∈ JFORM. Dann ist
[θ, θ', Δ] = [θ, θ', ^r-Δo^π ] = ^r-[θ, θ', ΔoΓ fur alle θ ∈ GTERM. Nun gilt nach I.V. θ ∈
TT([θ, θ', Δ0]) fur alle θ ∈ GTERM oder [θ, θ', Δ0] = Δ0 fur alle θ ∈ GTERM. Im ersten
Fall gilt auch θ ∈ TT(^r-[θ, θ', Δo]^π) = TT([θ, θ', Δ]) fur alle θ ∈ GTERM. Im zweiten
Fall gilt [θ, θ', Δ] = ^r-[θ, θ', ΔoΓ = ^r-Δo^π = Δ fur alle θ ∈ GTERM. Sei Δ = ^r(Δo ψ Δι)^π.
Der Fall verlauft analog zum Negatorfall.

Sei Δ = ^rΠξΔo^π. Sei zunachst ξ = θ'. Dann ist [θ, θ', Δ] = [θ, θ', ^rΠξΔo^π ] = ^rΠξΔo^π = Δ
fur alle θ ∈ GTERM. Sei sodann ξ ≠ θ'. Dann ist [θ, θ', Δ] = [θ, θ', ^rΠξΔo^π] = ^rΠξ[θ, θ',
Δ₀]^^l fur alle θ ∈ GTERM. Nun gilt nach I.V. θ ∈ TT([θ, θ', Δ₀]) fur alle θ ∈ GTERM
oder [θ, θ', Δo] = Δo fur alle θ ∈ GTERM. Im ersten Fall gilt auch θ ∈ TT(^rΠξ[θ, θ', Δo]^π)
= TT([θ, θ', Δ]) fur alle θ ∈ GTERM. Im zweiten Fall gilt [θ, θ', Δ] = ^rΠξ[θ, θ', Δo]^π =
^rΠξΔ₀^^l = Δ fur alle θ ∈ GTERM. ■

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

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

Beweis: Durch Induktion uber den Termaufbau von θ. Sei θ ∈ ATERM. Sei nun k ∈
N∖{0}, {θo, ., θ_fc-ι} ⊆ GTERM und {ξo, ., ξ_t-₁} ⊆ VAR∖TT(θ), wobei ξ ≠ ξj fur alle i,
j < k mit i ≠ j. Dann ist θ ∈ KONST ∪ PAR ∪ VAR. Sei zunachst θ ∈ PAR ∪ KONST.
Dann gibt es kein i < k, so dass θ = θi, oder es gibt ein i < k, so dass θ = θi. Im ersten Fall
ergibt sich θ = [<θo, ., θk-1>, <ξo, ., ξk-1>, θ] sowie FV(θ) ⊆ {ξo, ., ξk-1} ∪ FV(θ) und
TT(θ) ∩ {θo, ., θk-1} = 0. Im zweiten Fall ist dann fur ein i < k θ = [<θo, ., θi>, <ξo, .,
ξi>, ξi]. Wegen ξi ≠ ξj fur alle i, j < k mit i ≠ j, gilt damit aber auch θ = [<θo, ., θi>, <ξo, .,
ξi>, ξi] = [<θo, ., θk-1>, <ξo, ., ξk-1>, ξi] und es ist FV(ξi) ⊆ {ξo, ., ξk-1} ∪ FV(θ) und
TT(ξi) ∩ {θo, ., θk-1} = 0. Sei nun θ ∈ VAR. Dann ist wegen {ξo, ., ξk-1} ⊆
VAR∖TT(θ) ebenfalls θ = [<θo, ., θ_fc-ι>, <ξo, ., ξ_fc-ι>, θ] und FV(θ) ⊆ {ξo, ., ξ_fc-ι} ∪
FV(θ) und wegen TT(θ) ∩ {θo, ., θk-1} ⊆ VAR ∩ GTERM = 0 auch TT(θ) ∩ {θo, .,
θk-1} = 0.

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