Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

36    1 Zum grammatischen Rahmen

Theorem 1-22. Eindeutige Substitutionsorte (b) fur Terme

Wenn θ, θ⁺ ∈ TERM, θ* ∈ GTERM∖(TT(θ) ∪ TT(θ⁺)), ξ ∈ VAR, β ∈ PAR und [θ*, ξ, θ] =
[θ*, β, θ⁺], dann θ⁺ = [β, ξ, θ].

Beweis: Durch Induktion uber den Termaufbau von θ. Sei θ ∈ ATERM. Sei nun θ⁺ ∈
TERM, θ* ∈ GTERM∖(TT(θ) ∪ TT(θ⁺)), ξ ∈ VAR, β ∈ PAR und [θ*, ξ, θ] = [θ*, β, θ⁺].
Dann ist θ ∈ KONST ∪ PAR ∪ VAR. Sei nun θ ∈ KONST. Dann ist [θ*, ξ, θ] = θ. Dann
ist θ = [θ*, β, θ⁺], womit sich wegen θ* ∉ TT(θ) und Theorem 1-14-(i) ergibt, dass θ = θ⁺
und wegen θ ≠ ξ: θ⁺ = θ = [β, ξ, θ]. Sei nun θ ∈ PAR. Dann ist [θ*, ξ, θ] = θ. Dann ist θ =
[θ*, β, θ⁺], womit sich wegen θ* ∉ TT(θ) und Theorem 1-14-(i) ergibt, dass auch θ = θ⁺
und wegen ξ ≠ θ: θ⁺ = θ = [β, ξ, θ]. Sei nun θ ∈ VAR. Angenommen θ = ξ. Dann ist [θ*,
ξ, θ] = θ*. Dann ist θ* = [θ*, β, θ⁺]. Dann ist wegen θ* ≠ θ⁺ β ∈ TT(θ⁺). Damit ist θ* ∈
TT([θ*, β, θ⁺]). Ware nun θ⁺ ≠ β ergabe sich dann mit θ* = [θ*, β, θ⁺], dass θ* im Wider-
spruch zu Theorem 1-8 echter Teilterm von sich selbst ware. Also gilt θ⁺ = β = [β, ξ, θ].
Sei nun θ ≠ ξ. Dann ist θ = [θ*, ξ, θ]. Dann ist θ = [θ*, β, θ⁺]. Dann ist wegen θ* ∉ TT(θ)
und Theorem 1-14-(i) θ = θ⁺ und wegen θ ≠ ξ: θ⁺ = θ = [β, ξ, θ].

Gelte die Behauptung nun fur {θ₀, ..., θ_r-ι} ⊆ TERM und sei ^rφ(θ₀, ..., θ_r-1)^^l ∈
FTERM. Sei nun θ⁺ ∈ TERM, θ* ∈ TERM∖(TT( ^rφ(θo, ., θr-ʃ) ∪ TT(θ⁺)), ξ ∈ VAR, β
∈ PAR und [θ*, ξ, ^rφ(θo, .,        = [θ*, β, θ⁺]. Also [θ*, β, θ⁺] = ^rφ([θ*, ξ, θo], ., [θ*,

ξ, θ_r-ι])^^l ∈ FTERM. Ware θ⁺ ∈ ATERM. Dann ware β ≠ θ⁺ oder β = θ⁺. Angenommen β
≠ θ⁺. Dann ist θ⁺ = [θ*, β, θ⁺] = ^rφ([θ*, ξ, θo], ., [θ*, ξ, θr-ι])^π ∈ FTERM. Widerspruch!
Angenommen β = θ⁺. Dann ist θ* = [θ*, β, θ⁺] = ^rφ([θ*, ξ, θ₀], ., [θ*, ξ, θ_r-1])^^l. Mit
Theorem 1-14-(i) gilt dann fur alle i < r: [θ*, ξ, θi] = θi oder es gibt ein i < r, so dass θ* ∈
TT([θ*, ξ, θi]). Wenn [θ*, ξ, θi] = θi fur alle i < r, dann θ* = ^rφ([θ*, ξ, θo], ., [θ*, ξ,
θ_r-1])^^l = ^rφ(θ₀, ., θ_r-ι)^^l und damit entgegen der Voraussetzung θ* ∈ TT(^rφ(θ₀, .
θ_r-1)^^l). Wenn es andererseits ein i < r gibt, so dass θ* ∈ TT([θ*, ξ, θi]), dann ist θ* echter
Teilterm von ^rφ([θ*, ξ, θ₀], ., [θ*, ξ, θ_r-1])^^l, also echter Teilterm von sich selbst. Wider-
spruch zu Theorem 1-8. Also θ⁺ ∉ ATERM, sondern θ⁺ ∈ FTERM. Also gibt es {θ'o, .,
θ'k-ι} ⊆ TERM und φ' ∈ FUNK, so dass θ⁺ = ^rφ'(θ'o, ., θ'k-ι)^π. Damit ist ^rφ'([θ*, β, θ'o],
., [θ*, β, θ'k-ι])^π = [θ*, β, ^rφ'(θ'o, ., θ'k-ʃ] = [θ*, β, θ⁺] = ^rφ([θ*, ξ, θo], ., [θ*, ξ,
θ_r-ι])^^l. Mit Theorem 1-11-(ii) gilt dann k = r und φ' = φ und [θ*, β, θ'i] = [θ*, ξ, θi] fur al-
le i < r. Mit I.V. ergibt sich, dass θ'_i = [β, ξ, θi] fur alle i < r. Damit ist dann θ⁺ = ^rφ'(θ'₀,
., θ'k-ι)^π = ^rφ([β, ξ, θo], ., [β, ξ, θr-₁])^π = [β, ξ, ^rφ(θo, ., θr-ʃ]. ■

<<   38   39   40   41   42   43   44   >>

More intriguing information