Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

Theorem 1-23. Eindeutige Substitutionsorte (b) fur Formeln

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

Beweis: Seien Δ, Δ⁺ ∈ FORM, θ* ∈ GTERM∖(TT(Δ) ∪ TT(Δ⁺)) und ξ ∈ VAR, β ∈ PAR
und [θ*, ξ, Δ] = [θ*, β, Δ⁺]. Wie im Induktionsschritt des vorangehenden Beweises fur
funktorale 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 Beweis
wird nun mittels Induktion uber den Formelaufbau von Δ gefuhrt. Sei Δ = ^rΦ(θ₀, ... θ_r-1)^^l
∈ AFORM. Dann ist auch [θ*, ξ, Δ] = ^rΦ([θ*, ξ, θo], ., [θ*, ξ, θr₄])^π ∈ AFORM und es
gibt {θ'o, ., θ'r-ι} ⊆ TERM mit ^rΦ(θ'o, ., θVι)^π = Δ⁺. Also auch ^rΦ([θ*, ξ, θo], ., [θ*,
ξ, θr-ι])^π = [θ*, ξ, Δ] = [θ*, β, Δ⁺] = [θ*, β, ^rΦ(θ'o, ., θ'r-ι∏ = ^rΦ([θ*, β, θ'o], ., [θ*, β,
θ'_r-1])^^l ∈ AFORM. Mit Theorem 1-11-(iv) gilt dann [θ*, ξ, θ_i] = [θ*, β, θ'_i] fur alle i < r.
Mit Theorem 1-22 ergibt sich, dass θ'_i = [β, ξ, θ_i] fur alle i < r. Damit ist dann Δ⁺ = ^rΦ(θ'_o,
. θ'r-1Γ = ^rΦ([β, ξ, θo], ., [β, ξ, θr-1]Γ = [β, ξ, ^rΦ(θo, ., θr-ʃ] = [β, ξ, Δ].

Gelte die Behauptung nun fur Δ_o, Δ₁ ∈ FORM und sei Δ = ^r—Δ_o^^l ∈ JFORM. Dann ist
auch [θ*, ξ, Δ] = ^r-[θ*, ξ, Δo]^π ∈ JFORM und es gibt Δ'o ∈ FORM mit ^r√W = Δ⁺. Al-
so auch ^r-[θ*, ξ, Δo]^π = [θ*, β, Δ⁺] = [θ*, β, ^r-Δ'o^π ] = ^r-[θ*, β, Δ'o]^π ∈ JFORM. Mit
Theorem 1-11-(v) gilt dann [θ*, ξ, Δo] = [θ*, β, Δ'o]. Mit I.V. ergibt sich, dass Δ'o = [β, ξ,
Δo] und damit Δ⁺ = 'V = ^r-[β, ξ, Δ<,Γ = [β, ξ, ` Δ ] = [β, ξ, Δ]. Sei Δ = ^r(Δo ψ Δ1)"
∈ JFORM. Dann ist auch [θ*, ξ, Δ] = ^r([θ*, ξ, Δ_o] ψ [θ*, ξ, Δ₁])^^l ∈ JFORM und es gibt
Δ'o, Δ'1 ∈ FORM mit ^r(Δ'o ψ Δ'1)^π = Δ⁺. Also auch ^r([θ*, ξ, Δo] ψ [θ*, ξ, Δ1])^π = [θ*, β,
Δ⁺] = [θ*, β, ^r(Δ'o ψ Δ'1)^π] = ^r([θ*, β, Δ'o] ψ [θ*, β, Δ'1])^π ∈ JFORM. Mit Theorem
1-11-(vi) gilt dann [θ*, ξ, Δo] = [θ*, β, Δ'o] und [θ*, ξ, Δ1] = [θ*, β, Δ'1]. Mit I.V. ergibt
sich, dass Δ'o = [β, ξ, Δo] und Δ'1 = [β, ξ, Δ1] und damit Δ⁺ = ^r(Δ'o ψ Δ'1)^π = ^r([β, ξ, Δo] ψ
[β, ξ, Δ1]>- = [β, ξ, ^r(Δo ψ ʌɪ)ɔ] = [β, ξ, Δ].

Sei Δ = ^rΠξ'Δ_o^^l ∈ QFORM. Angenommen ξ' = ξ. Dann ist Δ = ^rΠξ'Δ_o^^l = [θ*, ξ,
^rΠξ'Δo^π] = [θ*, ξ, Δ] = [θ*, β, Δ⁺]. Mit Theorem 1-14-(ii) ist θ* ∈ TT([θ*, β, Δ⁺]) =
TT(Δ) oder [θ*, β, Δ⁺] = Δ⁺. Der erste Fall kann nach Voraussetzung nicht eintreten. Im
zweiten Fall ist Δ⁺ = ^rΠξ'Δ_o^^l = [β, ξ, ^rΠξ'Δ_o^^l ] = [β, ξ, Δ]. Angenommen ξ' ≠ ξ. Dann ist
auch [θ*, ξ, Δ] = ^rΠξ'[θ*, ξ, Δo]^π ∈ QFORM und es gibt Δ'o ∈ FORM mit ^rΠξ'Δ√ = Δ⁺.
Also auch ^rΠξ'[θ*, ξ, Δo]^π = [θ*, β, Δ⁺] = [θ*, β, ^rΠξ'Δ√] = ^rΠξ'[θ*, β, Δ'o]^π ∈
QFORM. Mit Theorem 1-11-(vii) gilt dann [θ*, ξ, Δo] = [θ*, β, Δ'o]. Mit I.V. ergibt sich,

<<   39   40   41   42   43   44   45   >>

More intriguing information