Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

34    1 Zum grammatischen Rahmen

Theorem 1-19. Eindeutige Substitutionsorte (a) fur Terme

Wenn θ, θ⁺ ∈ TERM, θ* ∈ GTERM∖(TT(θ) ∪ TT(θ⁺)) und θ§ ∈ ATERM und wenn [θ*, θ§, θ]
= [θ*, θ^δ, θ⁺], dann θ = θ⁺.

Beweis: Durch Induktion uber den Termaufbau von θ. Sei θ ∈ ATERM. Sei nun θ⁺ ∈
TERM, θ* ∈ GTERM∖(TT(θ) ∪ TT(θ⁺)) und θ^δ ∈ ATERM und sei [θ*, θ^δ, θ] = [θ*, θ^δ,
θ⁺]. Sei nun θ^δ = θ. Dann ist [θ*, θ^δ, θ] = θ*. Dann ist θ* = [θ*, θ, θ⁺]. Da nach Vorausset-
zung θ* ∉ TT(θ⁺) und mithin θ⁺ ≠ θ*, ist dann θ = θ⁺. Sei nun θ^δ ≠ θ. Dann ist [θ*, θ^δ, θ]
= θ. Dann ist θ = [θ*, θ^δ, θ⁺], womit sich wegen θ* ∉ TT(θ) mit Theorem 1-14-(i) eben-
falls ergibt, dass θ = θ⁺.

Gelte die Behauptung nun fur {θ₀, ..., θ_r-ι} ⊆ TERM und sei ^rφ(θ₀, ... θ_r-1)^^l ∈
FTERM. Sei nun θ⁺ ∈ TERM, θ* ∈ GTERM∖(TT( ^rφ(θo, . θr-ʃ) ∪ TT(θ⁺)) und θ^δ ∈
ATERM und sei [θ*, θ^δ, ^rφ(θo, ., θr-ι)^π] = [θ*, θ^δ, θ⁺]. Also [θ*, θ^δ, θ⁺] = ^rφ([θ*, θ^δ, θɑ],
., [θ*, θ^δ, θ_r-ι])^^l ∈ FTERM. Ware θ⁺ ∈ ATERM. Dann ware θ^δ ≠ θ⁺ oder θ^δ = θ⁺. An-
genommen θ^δ ≠ θ⁺. Dann ist θ⁺ = [θ*, θ^δ, θ⁺] = ^rφ([θ*, θ^δ, θ₀], ., [θ*, θ^δ, θ_r-1])^^l ∈
FTERM. Widerspruch! Angenommen θ^δ = θ⁺. Dann ist θ* = [θ*, θ^δ, θ⁺] = ^rφ([θ*, θ^δ, θ₀],
., [θ*, θ^δ, θ_r-1])^π. 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φ([θ*, θ^δ, θ₀], ., [θ*, θ^δ, θ_r-ι])^^l = ^rφ(θ₀, ., θ_r-ι)^^l und damit entgegen der Vorausset-
zung θ* ∈ 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 Teil-
term von sich selbst. Widerspruch 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, ., ‰)^π] = [θ*, θ^s,
θ⁺] = ^rφ([θ*, θ^δ, θ₀], ., [θ*, θ^δ, θ_r-1])^^l. Mit Theorem 1-11-(ii) gilt dann k = r und φ' = φ
und [θ*, θ^δ, θi] = [θ*, θ^δ, θ'i] fur alle i < r. Mit I.V. ergibt sich, dass θi = θ'i fur alle i < r.
Damit ist dann ^rφ(θ₀, ., θ_r-1)^^l = ^rφ'(θ'₀, ., θ'_k-1)^^l = θ⁺. ■

Theorem 1-20. Eindeutige Substitutionsorte (a) fur Formeln

Wenn Δ, Δ⁺ ∈ FORM, θ* ∈ GTERM∖(TT(Δ) ∪ TT(Δ⁺)) und θ§ ∈ ATERM und wenn [θ*, θ^δ,
Δ] = [θ*, θ^δ, Δ⁺], dann Δ = Δ⁺.

Beweis: Seien Δ, Δ⁺ ∈ FORM, θ* ∈ GTERM∖(TT(Δ) ∪ TT(Δ⁺)) und θ^δ ∈ ATERM und
[θ*, θ^δ, Δ] = [θ*, θ^δ, Δ⁺]. Wie im Induktionsschritt des vorangehenden Beweises fur funk-

<<   <   36   37   38   39   40   41   42   >   >>