Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

Sei Δ = ^rΠξΔo^π ∈ QFORM. Angenommen ξ = θ⁺. Dann ist [θ*, θ⁺, Δ] = [θ*, θ⁺,
'HξΔ I = ^rΠξΔo^π = [β, θ⁺, ^rΠξΔo^π] = [β, θ⁺, Δ]. Dann ist β ∉ TT([β, θ⁺, Δ]) = TT(Δ).
Also [θ*, θ⁺, Δ] = [β, θ⁺, Δ] = [θ*, β, [β, θ⁺, Δ]]. Angenommen ξ ≠ θ⁺. Der Fall verlauft
analog zum Negatorfall.

Zu (iii): Der Fall verlauft analog zum Negatorfall. ■

Theorem 1-25. Eine hinreichende Bedingung fur die Kommutativitat einer Substitution in
Termen und Formeln

Wenn θ*o, θ*ι ∈ GTERM, θo, θι ∈ ATERM, θo ≠ θɪ, θɪ ∉ TT(θ*o) und θo ∉ TT(θ*ι), dann:
(i) Wenn θ⁺ ∈ TERM, dann [θ*₁, θ₁, [θ*_o, θ_o, θ⁺]] = [θ*_o, θ_o, [θ*₁, θ₁, θ⁺]], und
(ii) Wenn Δ ∈ FORM, dann [θ*ι, θ₁, [θ*o, θo, Δ]] = [θ*o, θo, [θ*ι, θι, Δ]].

Beweis: Seien θ*o, θ*1 ∈ GTERM, θo, θ1 ∈ ATERM, θo ≠ θ1, θ1 ∉ TT(θ*o) und θo ∉
TT(θ*₁). Zu (i): Sei θ⁺ ∈ TERM. Der Beweis wird mittels Induktion uber den Termaufbau
von θ⁺ gefuhrt. Sei θ⁺ ∈ ATERM. Angenommen θ⁺ = θ_o. Dann ist θ⁺ ≠ θ₁ und [θ*₁, θ₁,
[θ*o, θo, θ⁺]] = [θ*1, θ1, θ*o]. Weil θ1 ∉ TT(θ*o) gilt [θ*1, θ1, θ*o] = θ*o. Andererseits ist
[θ*o, θo, [θ*1, θ1, θ⁺]] = [θ*o, θo, θ⁺] = θ*o. Also [θ*1, θ1, [θ*o, θo, θ⁺]] = [θ*o, θo, [θ*1, θ1,
θ⁺]]. Sei nun θ⁺ ≠ θo. Angenommen θ⁺ = θ1. Dann ist [θ*1, θ1, [θ*o, θo, θ⁺]] = [θ*1, θ1, θ⁺]
= θ*1. Weil θo ∉ TT(θ*1) gilt [θ*o, θo, θ*1] = θ*1. Damit ist [θ*o, θo, [θ*1, θ1, θ⁺]] = [θ*o,
θo, θ*1] = θ*1. Also [θ*1, θ1, [θ*o, θo, θ⁺]] = [θ*o, θo, [θ*1, θ1, θ⁺]]. Angenommen θ⁺ ≠ θ1.
Dann ist [θ*1, θ1, [θ*o, θo, θ⁺]] = [θ*1, θ1, θ⁺] = θ⁺ und [θ*o, θo, [θ*1, θ1, θ⁺]] = [θ*o, θo, θ⁺]
= θ⁺. Also auch [θ*1, θ1, [θ*o, θo, θ⁺]] = [θ*o, θo, [θ*1, θ1, θ⁺]].

Gelte die Behauptung fur {θ'_o, ..., θ'_r-1} ⊆ TERM und sei θ⁺ = ^rφ(θ'_o, ..., θ'_r-1)^^l ∈
FTERM. Dann ist [θ*ι, θ₁, [θ*o, θo, θ⁺]] = [θ*ι, θι, [θ*o, θo, ^rφ(θ'o, ., θ'r-ι)^π]] = ^rφ([θ*ι,
θι, [θ*o, θo, θ'o]], ., [θ*ι, θι, [θ*o, θo, θ'r-ι]])^π. Mit I.V. gilt [θ*1, θι, [θ*o, θo, θ'i]] = [θ*o,
θo, [θ*ι, θι, θ'_i]] fur alle i < r. Also [θ*ι, θι, [θ*o, θo, θ⁺]] = ^rφ([θ*o, θo, [θ*ι, θι, θ'o]], .,
[θ*o, θo, [θ*ι, θι, θ'r-ι]])^π = [θ*o, θo, [θ*ι, θι, ^rφ(θ'o, . θ¼)^π]] = [θ*o, θo, [θ*ι, θι, θ⁺]].

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

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