Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

42    1 Zum grammatischen Rahmen

Gelte die Behauptung nun fur {θ₀, ., θ_r-1} ⊆ TERM und sei θ = ^rφ(θ₀, ., θ_r-1)^π ∈
FTERM. Dann ist [β*_fc, β_fc, [<β*o, ., β*k-ι>, <βo, ., βk-ι>, θ]] = [β*k, βk, [<β*o, ., β*k-ι>,
<βo, ., β_fc4>, ^rφ(θo, ., θ -I Il = ^rφ([β*⅛, βk, [<β*o, ., β*_fc-ι>, (βo, ., β_fc-ι>, θo]], ., [β*_fc,
βk, [<β*o, ., β*_fc-ι>, (βo, ., β_fc-ι>, θ ∣∏) . Mit I.V. gilt [β*k, βk, [(β*o, ., β*k-ι), (βo, .,
βk-ι>, θi]] = [<β*o, ., β*k>, <βo, ., βk>, θi] fur alle i < r. Also [β*k, βk, [<β*o, ., β*k-ι>, <βo,
., β_fc-ι>, θ]] = ^rφ([(β*o, ., β*_fc>, (βo, ., β_fc>, θo], ., [<β*o, ., β*_fc>, (βo, ., β_fc>, θ -]) =
[<β*o, ., β*k>, (βo, ., βk>, ^rφ(θo, ., θ -) ] = [<β*o, ., β*_fc>, (βo, ., β_fc>, θ].

Zu (ii): Der Beweis wird mittels Induktion uber den Formelaufbau von Δ gefuhrt. Sei Δ
= ^rΦ(θ_o, . θ_r-1)^^l ∈ AFORM. Der Fall verlauft analog zum FTERM-Fall unter Verwen-
dung von (i).

Gelte die Behauptung nun fur Δ_o, Δ₁ ∈ FORM und sei Δ = ^r—Δ_o^^l ∈ JFORM. Dann ist
[β*k, βk, [(β*o, ., β*_fc-1>, (βo, ., β_fc-1>, Δ]] = [β*k, βk, [<β*o, ., β*k-1>, (βo, ., βk-1>,
Γ-Δoη] = ■-[β*k, βk, [<β*₀, ., β*k-ι), (βo, ., βk-ι), Δo]Γ. Mit I.V. gilt [β*k, βk, [<β*o, .,
β*k-ι>, (βo, ., βk-ι), Δo]] = [(β*o, ., β*k>, (βo, ., βk>, Δo]. Also [β*k, βk, [(β*o, ., β*k-ι),
(βo, ., β_fc-1>, Δ]] = ^r-[(β*o, ., β*_fc>, (βo, ., β_fc>, Δ ] = [<β*o, ., β*_fc>, (βo, ., β_fc>,
■ Δ ] = [<β*o, ., β*_fc>, (βo, ., β_fc>, Δ]. Sei Δ = ^r(Δo ψ Δ_l)' ∈ JFORM. Der Fall verlauft
analog zum Negatorfall. Sei Δ = ^rΠξΔ_o^^l ∈ QFORM. Der Fall verlauft analog zum Nega-
torfall.

Zu (iii) und (iv): (iii) ergibt sich analog zum Negatorfall unter Verwendung von (ii). (iv)
ergibt sich analog zum FTERM-Fall unter Verwendung von (iii). ■

Hinweis: Ein zu Theorem --27 analoges Theorem lasst sich fur Formelmengen zeigen.

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

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

(i) Wenn θ ∈ TERM, dann

[θ*k, ξk, [(θ*o, ., θ*k-ι>, (ξo, ., ξk-ι>, θ]] = [(θ*o, ., θ*k), (ξo, ., ξk>, θ], und

(ii) Wenn Δ ∈ FORM, dann

[θ*k, ξk, [(θ*o, ., θ*k-1>, (ξo, ., ξk-1>, Δ]] = [(θ*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 den Termaufbau von θ gefuhrt. Sei θ ∈ ATERM. Angenommen ξi ≠ θ fur alle i <

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