Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

Gelte die Behauptung fur Δ₀, Δ₁ ∈ FORM und sei Δ = ^r—Δ₀^^l ∈ JFORM. Dann ist [θ',
θ⁺, [θ*, ζ, Δ]] = [θ', θ⁺, [θ*, ζ, ` Δ ]] = ^r-[θ', θ⁺, [θ*, ζ, Δo]Γ. Mit I.V. gilt [θ', θ⁺, [θ*,
ζ, Δo]] = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, Δo]]. Also [θ', θ⁺, [θ*, ζ, Δ]] = ^r-[[θ', θ⁺, θ*], ζ, [θ', θ⁺,
Δo]Γ = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, ^r- Δ ]] = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, Δ]]. Sei Δ = ^γ(Δo ψ Δ1)- ∈
JFORM. Der Fall verlauft analog zum Negatorfall.

Sei Δ = r∏ξΔo^π ∈ QFORM. Angenommen ξ = ζ. Dann ist [θ', θ⁺, [θ*, ζ, Δ]] = [θ', θ⁺,
[θ*, ζ, r∏ξΔo^π]] = [θ', θ⁺, r∏ξΔo^π] = r∏ξ[θ', θ⁺, ΔoΓ = [[θ', θ⁺, θ*], ζ, r∏ξ[θ', θ⁺, Δ I ] =
[[θ', θ⁺, θ*], ζ, [θ', θ⁺, r∏ξΔo^π ]] = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, Δ]]. Angenommen ξ ≠ ζ. Der Fall
verlauft analog zum Negatorfall. ■

Theorem 1-27. Mehrfache Substitution von neuen und paarweise verschiedenen Parametern
furpaarweise verschiedene Parameter in Termen, Formeln, Satzen und Sequenzen

Wenn θ ∈ TERM, Δ ∈ FORM, Σ ∈ SATZ, S ∈ SEQ, k ∈ N∖{0} und {β*o, ., β*k} ⊆
PAR∖(TT(θ) ∪ TT(Δ) ∪ TT(Σ) ∪ TTSEQ(S)) und {βo, ., β⅛} ⊆ PAR∖{β*o, ., β*_k}, wobei
β*_i ≠ β*j und β_i ≠ β_j∙ fur alle i, j < k+1 mit i ≠ j, dann:

(i)    [β*k, βk, [(β*o, ., β*k-i>, (βo, ., β_fc-ι>, θ]] = [(β*o, ., β*_ft>, (βo, ., βk>, θ],

(ii)   [β*k, βk, [(β*0, ., β*k-i>, (βo, ., βk-i>, Δ]] = [(β*0, ., β*k>, (βo, ., βk>, Δ],

(iii)   [β*k, βk, [(β*0, ., β*k-i>, (βo, ., βk-i>, Σ]] = [(β*0, ., β*k>, (βo, ., βk>, Σ] und

(iv)   [β*k, βk, [<β*0, ., β*k-1>, <βo, ., βk-1>, S]] = [<β*o, ., β*k>, <βo, ., βk>, S].

Beweis: Seien θ ∈ TERM, Δ ∈ FORM, Σ ∈ SATZ, S ∈ SEQ, k ∈ N∖{0} und {β*o, .,
β*k} ⊆ PAR∖(TT(θ) ∪ TT(Δ)) und {βo, ., β_fc} ⊆ PAR∖{β*o, ., β*k}, wobei β*i ≠ β*j
und βi ≠ βj fur alle i, j < k+1 mit i ≠ j. Zu (i): Der Beweis wird mittels Induktion uber den
Termaufbau von θ gefuhrt. Sei θ ∈ ATERM. Dann ist θ ∈ KONST ∪ PAR ∪ VAR. Sei
nun θ ∈ KONST ∪ VAR ∪ (PAR∖{βo, ., β_fc}). Dann ist θ = [(β*o, ., β*k-ι>, (βo, .,
βk-ι>, θ] und es ist θ = [<β*o, ., β*k>, (βo, ., βk>, θ] und damit [β*k, βk, [(β*o, ., β*k-ι>,
<βo, ., βk-1>, θ]] = [β*k, βk, θ] = θ = [<β*o, ., β*k>, <βo, ., βk>, θ].

Sei nun θ ∈ {βo, ., βk}. Dann ist θ = βi fur ein i < k+1. Dann ist nach Voraussetzung
fur alle j < k+1 mit j ≠ i gilt auch θ ≠ βj. Damit ist zunachst [(β*₀, ., β*_k>, (β₀, ., β_k>, θ]
= β*i. Sei nun i < k. Dann ist [(β*o, ., β*k-ι>, (βo, ., βk-ι>, θ] = β*i und damit [β*k, β_k,
[<β*o, ., β*k-ι>, <βo, ., βk-ι>, θ]] = [β*k, βk, β*i]. Aus der Voraussetzung ergibt sich nun,
dass βk ≠ β*i und damit, dass [β*k, βk, β*i] = β*i. Sei nun i = k. Dann ist [<β*o, ., β*k-ι>,
<βo, ., βk-ι>, θ] = θ = βk und somit [β*k, βk, [(β*o, ., β*k-ι>, (βo, ., βk-ι>, θ]] = [β*k, βk,
βk] = β*k = β*i.

<<   <   43   44   45   46   47   48   49   >   >>