Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

44    1 Zum grammatischen Rahmen

., θ*k-ι>, <ξo, ., ξk-ι>, ^r∏ζΔo^π]] = [θ*k, ξk, ^r∏ζ[<θ*o, ., θ*k-ι>, <ξo, ., ξk-ι>, ʌo]ɔ] =
^r∏ζ[<θ*o, ., θ*k-ι>, <ξo, ., ξk-ι>, Δo,∣' = [<θ*o, ., θ*k}, <ξo, ., ξk>, ∙∏ζΔ I = [<θ*0, .,
θ*k}, <ξo, ., ξk>, Δ].

Angenommen ξ ≠ ζ fur alle i < k+1. Dann ist [θ*k, ξk, [<θ*o, ., θ*_k-ι), <ξo, ., ξk-ι>, Δ]]
= [θ*k, ξk, [<θ*o, ., θ*k-ι>, <ξo, ., ξk-1>, ^r∏ζΔo^π]] = [θ*k, ξk, ^r∏ζ[<θ*o, ., θ*k-ι>, <ξo, .,
ξk-ι>, Δ ] ] = ^r∏ζ[θ*k, ξk, [<θ*o, ., θ*k-ι>, <ξo, ., ξk-ι>, Δ H . Mit I.V. gilt [θ*k, ξk, [<θ*o,
., θ*k-ι>, <ξo, ., ξk-ι>, Δo]] = [<θ*o, ., θ*k>, <ξo, ., ξk>, Δo]. Also [θ*k, ξk, [<θ*o, .,
θ*k-1>, <ξo, ., ξk-1>, Δ]] = ^r∏ζ[<θ*o, ., θ*k>, <ξo, ., ξk>, Δ ] = [<θ*o, ., θ*k>, <ξo, ., ξk>,
^r∏ζΔo^π] = [<θ*o, ., θ*k>, <ξo, ., ξk>, Δ]. ■

Theorem 1-29. Mehrfache Substitution von geschlossenen Termen fur paarweise verschiedene
Variablen in Termen und Formeln (b)

Wenn k ∈ N∖{o}, {θ*o, ., θ*k} ⊆ GTERM und {ξo, ., ξ⅛} ⊆ VAR, wobei ξi ≠ ξ∙ fur alle i, j
< k+1 mit i ≠ j, dann:

(i) Wenn θ ∈ TERM, dann

[<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, [θ*k, ξk, θ]] = [<θ*o, ., θ*_ft>, <ξo, ., ξ_fc>, θ], und
(ii) Wenn Δ ∈ FORM, dann

[<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, [θ*k, ξk, Δ]] = [<θ*o, ., θ*k>, <ξo, ., ξk>, Δ].

Beweis: Seien k ∈ N\{o}, {θ*o, ., θ*k} ⊆ GTERM und {ξo, ., ξk} ⊆ VAR, wobei ξi ≠
ξj fur alle i, j < k+1 mit i ≠ j. Zu (i): Sei θ ∈ TERM. Der Beweis wird mittels Induktion
uber k gefuhrt. Sei k = 1. Dann ist mit Theorem 1-25-(i) und Theorem 1-28-(i) [θ*o, ξo,
[θ*1, ξ1, θ]] = [θ*1, ξ1, [θ*o, ξo, θ]] = [<θ*o, θ*1>, <ξo, ξ1>, θ]. Sei nun 1 < k. Durch Anwen-
dung von I.V., Theorem 1-25-(i), I.V., Theorem 1-28-(i), I.V. und Theorem 1-28-(i) in
dieser Reihenfolge ergibt sich: [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, [θ*k, ξk, θ]] = [<θ*o, ., θ*k-
2>, <ξo, ., ξk-2>, [θ*k-1, ξk-1, [θ*k, ξk, θ]]] = [<θ*o, ., θ*k-2>, <ξo, ., ξk-2>, [θ*k, ξk, [θ*k-1, ξk-1,
θ]]] = [<θ*o, ., θ*k-2, θ*k>, <ξo, ., ξk-2, ξk>, [θ*k-1, ξk-1, θ]] = [θ*k, ξk, [<θ*o, ., θ*k-2>, <ξo,
., ξk-2>, [θ*k-1, ξk-1, θ]]] = [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, θ]] = [<θ*o, ., θ*k>, <ξo,
., ξk>, θ].

(ii) folgt auf analogem Wege aus Theorem 1-25-(ii) und Theorem 1-28-(ii). ■

<<   <   46   47   48   49   50   51   52   >   >>