Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

torale Terme lasst sich fur alle Formeln zeigen, dass Substitutionsorte (Δ bzw. Δ⁺) der
gleichen Kategorie angehoren und denselben Hauptoperator (Pradikator, Junktor oder
Quantor) haben wie die Substitutionsergebnisse ([θ*, θ^δ, Δ] bzw. [θ*, θ^δ, Δ⁺]). Der Be-
weis wird nun mittels Induktion uber den Formelaufbau von Δ gefuhrt. Sei Δ = ^rΦ(θ₀, ...
θr.ι)^π ∈ AFORM. Dann ist auch [θ*, θ^δ, Δ] = ^rΦ([θ*, θ^δ, θo], ., [θ*, θ^δ, θr-ι])^π ∈
AFORM und es gibt {θ'₀, ., θ'_r-1} ⊆ TERM mit ^rΦ(θ'₀, . θ'∙∙_-∣Γ = Δ⁺. Also auch
^rΦ([θ*, θ^δ, θo], ., [θ*, θ^δ, θr-ι])^π = [θ*, θ^δ, Δ] = [θ*, θ^δ, Δ⁺] = [θ*, θ^δ, ^rΦ(θ'o, . θ'r-ι)^π] =
^rΦ([θ*, θ^δ, θ'o], ., [θ*, θ^δ, θ'r-ι])^π ∈ AFORM. Mit Theorem ɪ-ɪɪ-(iv) gilt dann [θ*, θ^δ,
θi] = [θ*, θ^δ, θ'i] fur alle i < r. Mit Theorem 1-19 ergibt sich, dass θi = θ'i fur alle i < r.
Damit ist dann ^rΦ(θ₀, . θ_r-1)^^l = ^rΦ(θ'₀, . θ'_r-1)^^l = Δ⁺.

Gelte die Behauptung nun fur Δ₀, Δ₁ ∈ FORM und sei Δ = ^r—Δ₀^^l ∈ JFORM. Dann ist
auch [θ*, θ^δ, Δ] = ^r—[θ*, θ^δ, Δ₀]^^l ∈ JFORM und es gibt Δ'₀ ∈ FORM mit ^r— Δ'₀^^l = Δ⁺.
Also auch ^r-[θ*, θ^δ, Δ0]^π = [θ*, θ^δ, Δ] = [θ*, θ^δ, Δ⁺] = [θ*, θ^δ, ^r-ΔA∣ = ^r-[θ*, θ^δ, Δ'0]^π
∈ JFORM. Mit Theorem 1-11-(v) gilt dann [θ*, θ^δ, Δ0] = [θ*, θ^δ, Δ'0]. Mit I.V. ergibt
sich, dass Δ₀ = Δ'₀ und damit Δ = ^r—Δ₀^^l = ^r— Δ'₀^^l = Δ⁺. Sei Δ = ^r(Δ₀ ψ Δ₁)^^l ∈ JFORM.
Dann ist auch [θ*, θ^δ, Δ] = ^r([θ*, θ^δ, Δ0] ψ [θ*, θ^δ, Δι])^π ∈ JFORM und es gibt Δ'0, ʌ'ɪ ∈
FORM mit ^r(Δ'0 ψ Δ'ι)^π = Δ⁺. Also auch ^r([θ*, θ^δ, Δ0] ψ [θ*, θ^δ, Δι])^π = [θ*, θ^δ, Δ] = [θ*,
θ^δ, Δ⁺] = [θ*, θ^δ, ^r(Δ'0 ψ Δ'ι)^π] = ^r([θ*, θ^δ, Δ'0] ψ [θ*, θ^δ, Δ'ι])^π ∈ JFORM. Mit Theorem
ɪ-ɪɪ-(vi) gilt dann [θ*, θ^δ, Δ0] = [θ*, θ^δ, Δ'0] und [θ*, θ^δ, Δι] = [θ*, θ^δ, Δ'ι]. Mit I.V.
ergibt sich, dass Δ₀ = Δ'₀ und Δ₁ = Δ'₁ und damit Δ = ^r(Δ₀ ψ Δ₁)^^l = ^r(Δ'₀ ψ Δ'₁)^^l = Δ⁺.

Sei Δ = ^rΠξΔ0^π ∈ QFORM. Dann ist auch [θ*, θ^δ, Δ] ∈ QFORM und es gibt Δ'0 ∈
FORM mit ^rΠξΔ'₀^^l = Δ⁺. Angenommen ξ = θ^δ. Dann ist Δ = ^rΠξΔ₀^^l = [θ*, θ^δ, ^rΠξΔ₀^^l ] =
[θ*, θ^δ, Δ] = [θ*, θ^δ, Δ⁺] = [θ*, θ^δ, ^rΠξΔ'0^π ] = ^r∏ξΔ'0^π = Δ⁺. Angenommen ξ ≠ θ^δ. Dann
ist ^rΠξ[θ*, θ^δ, Δ0]^π = [θ*, θ^δ, Δ] = [θ*, θ^δ, Δ⁺] = [θ*, θ^δ, ^rΠξΔ'0^π] = ^rΠξ[θ*, θ^δ, Δ'0]^π ∈
QFORM. Mit Theorem ɪ-ɪɪ-(vii) gilt dann [θ*, θ^δ, Δ0] = [θ*, θ^δ, Δ'0]. Mit I.V. ergibt sich,
dass Δ₀ = Δ'₀ und damit Δ = ^rΠξΔ₀^^l = ^rΠξΔ'₀^^l = Δ⁺. ■

Theorem 1-21. Eindeutige Substitutionsorte (a) fur Satze

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

Beweis: Analog zum Negatorfall im Beweis zu Theorem ɪ-20 unter Ruckgriff auf
Theorem 1-20 und Theorem 1-12. ■

<<   37   38   39   40   41   42   43   >>

More intriguing information