Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

38    1 Zum grammatischen Rahmen

dass Δ'o = [β, ξ, Δo] und damit Δ⁺ = ^rΠξ'Δ'o^π = ^r∏ξ'[β, ξ, Δ₀Γ = [β, ξ, ^r∏ξ'Δo^π ] = [β, ξ,
Δ]. ■

Theorem 1-24. Kurzung von Parametern bei der Substitution

Wenn θ ∈ TERM, Δ ∈ FORM, Σ ∈ SATZ, θ* ∈ GTERM, β ∈ PAR∖(TT(θ) ∪ TT(Δ) ∪
TT(Σ)) und θ⁺ ∈ ATERM, dann:

(i) [θ*, θ⁺, θ] = [θ*, β, [β, θ⁺, θ]],

(її) [θ*, θ⁺, Δ] = [θ*, β, [β, θ⁺, Δ]] und

(iii) [θ*, θ⁺, Σ] = [θ*, β, [β, θ⁺, Σ]].

Beweis: Seien θ ∈ TERM, Δ ∈ FORM, Σ ∈ SATZ, θ* ∈ GTERM, β ∈ PAR∖(TT(θ) ∪
TT(Δ) ∪ TT(Σ)) und θ⁺ ∈ ATERM. Zu (i): Der Beweis wird mittels Induktion uber den
Termaufbau von θ gefuhrt. Sei θ ∈ ATERM. Dann ist θ = θ⁺ oder θ ≠ θ⁺. Sei zunachst θ
= θ⁺. Dann ist [β, θ⁺, θ] = β und [θ*, θ⁺, θ] = θ*. Dann ist [θ*, θ⁺, θ] = θ* = [θ*, β, β] =
[θ*, β, [β, θ⁺, θ]]. Sei nun θ ≠ θ⁺. Dann ist [β, θ⁺, θ] = θ und [θ*, θ⁺, θ] = θ. Wegen β ∉
TT(θ) ist β ≠ θ und mithin θ = [θ*, β, θ]. Also [θ*, θ⁺, θ] = θ = [θ*, β, θ] = [θ*, β, [β, θ⁺,
θ]].

Gelte die Behauptung nun fur {θ₀, ., θ_r-1} ⊆ TERM und sei θ = ^rφ(θ₀, ... θ_r-1)^^l ∈
FTERM. Wegen β ∉ TT(θ) gilt auch β ∉ TT(θi) fur alle i < r. Dann gilt mit I.V. [θ*, θ⁺,
θi] = [θ*, β, [β, θ⁺, θi]] fur alle i < r. Dann ist [θ*, θ⁺, ^rφ(θo, . W] = W*, θ⁺, θo],
., [θ*, θ⁺, θr-ι])^π = ^rφ([θ*, β, [β, θ⁺, θo]], ., [θ*, β, [β, θ⁺, θr-ι]])^π = [θ*, β, ^rφ([β, θ⁺,
θo], ., [β, θ⁺, θr-ι])^π] = [θ*, β, [β, θ⁺, ^rφ(θo, . θr-ι)^π ]].

Zu (ii): Der Beweis wird mittels Induktion uber den Formelaufbau von Δ gefuhrt. Sei Δ
= ^rΦ(θo, . θr-ι)^π ∈ AFORM. Dann gilt β ∉ TT(θi) fur alle i < r und [θ*, θ⁺, Δ] = [θ*, θ⁺,
^rΦ(θo, . θr-ι)^π] = ^rΦ([θ*, θ⁺, θo], . [θ*, θ⁺, θr-ι])^π. Mit (i) gilt [θ*, θ⁺, θ_i] = [θ*, β, [β,
θ⁺, θi]] fur alle i < r. Also [θ*, θ⁺, Δ] = ^rΦ([θ*, β, [β, θ⁺, θo]], ., [θ*, β, [β, θ⁺, θr-ι]])^π =
[θ*, β, ^rΦ([β, θ⁺, θo], ., [β, θ⁺, θr-ι])^π = [θ*, β, [β, θ⁺, ^rΦ(θo, . θr-ι)^π ]] = [θ*, β, [β, θ⁺,
Δ]].

Gelte die Behauptung nun fur Δ_o, Δ₁ ∈ FORM. Sei zunachst Δ = ^r√∖_oΓ ∈ JFORM.
Dann gilt β ∉ TT(Δo) und [θ*, θ⁺, Δ] = [θ*, θ⁺, ^r-Δo^π ] = ^r-[θ*, θ⁺, Δo]^π. Mit I.V. gilt
[θ*, θ⁺, Δo] = [θ*, β, [β, θ⁺, Δo]]. Also [θ*, θ⁺, Δ] = ^r-[θ*, β, [β, θ⁺, Δo]]^π = [θ*, β, [β, θ⁺,
^r—Δ_o^^l ]] = [θ*, β, [β, θ⁺, Δ]]. Sei Δ = ^r(Δ_o ψ Δ₁)^^l ∈ JFORM. Der Fall verlauft analog zum
Negatorfall.

<<   <   40   41   42   43   44   45   46   >   >>