Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

32    1 Zum grammatischen Rahmen

Theorem 1-17. Alternative Basen fur die Substitution von geschlossenen Termen fur Variab-
len in Termen

Wenn {ξ, ζ} ∪ X ⊆ VAR, wobei {ξ, ζ} ∩ X = 0, und θ ∈ TERM, wobei FV(θ) ⊆ {ξ} ∪ X,
dann gibt es ein θ* ∈ TERM, wobei FV(θ*) ⊆ {ζ} ∪ X, so dass fur alle θ' ∈ GTERM gilt: [θ',
ξ, θ] = [θ', ζ, θ*].

Beweis: Seien {ξ, ζ} ∪ X ⊆ VAR, wobei {ξ, ζ} ∩ X = 0, und sei θ ∈ TERM, wobei
FV(θ) ⊆ {ξ} ∪ X. Falls ξ = ζ, dann ergibt sich mit θ* = θ sofort die Behauptung. Sei nun
ξ ≠ ζ. Der Beweis wird nun mittels Induktion uber den Termaufbau von θ gefuhrt. Sei θ
∈ KONST ∪ PAR. Dann gilt mit θ* = θ, dass FV(θ*) = 0 ⊆ {ζ} ∪ X und dass fur alle θ'
∈ GTERM gilt: [θ', ξ, θ] = [θ', ζ, θ*]. Sei nun θ ∈ VAR. Angenommen θ = ξ. Dann gilt
mit θ* = ζ, dass FV(θ*) ⊆ {ζ} ∪ X und fur alle θ' ∈ GTERM: [θ', ξ, θ] = θ' = [θ', ζ, θ*].
Angenommen θ ≠ ξ. Dann ist θ ∈ X und damit θ ∉ {ξ, ζ}. Dann gilt mit θ* = θ, dass
FV(θ*) = {θ} ⊆ {ζ} ∪ X und dass fur alle θ' ∈ GTERM gilt: [θ', ξ, θ] = θ = θ* = [θ', ζ,
θ*].

Gelte die Behauptung nun fur θ₀, ., θ_r-1 ∈ TERM und sei θ = ^rφ(θ₀, ... θ_r-1)^^l ∈
FTERM. Dann gilt fur alle i < r: FV(θi) ⊆ {ξ} ∪ X. Dann gibt es nach I.V. fur alle i < r
ein θ*i ∈ TERM, wobei FV(θ*i) ⊆ {ζ} ∪ X, so dass fur alle θ' ∈ GTERM gilt: [θ', ξ, θi]
= [θ', ζ, θ*_i]. Dann gilt mit θ* = ^rφ(θ*₀, . θ*_r-1)^^l, dass FV(θ*) ⊆ {ζ} ∪ X und dass fur
alle θ' ∈ GTERM gilt: [θ', ξ, θ] = [θ', ξ, ^rφ(θo, . θr-ι)^π] = ^rφ([θ', ξ, θo], . [θ', ξ, θr-ι])^π =
^rφ([θ', ζ, θ*o], . [θ', ζ, θ*r-ι])^π = [θ', ζ, ^rφ(θ*o, . θ*r-ι)^π ] = [θ', ζ, θ*]. ■

Theorem 1-18. Alternative Basen fur die Substitution von geschlossenen Termen fur Variab-
len in Formeln

Wenn {ξ, ζ} ∪ X ⊆ VAR, wobei {ξ, ζ} ∩ X = 0, und Δ ∈ FORM, wobei FV(Δ) ⊆ {ξ} ∪ X
und ζ ∉ TT(Δ), dann gibt es ein Δ* ∈ FORM, wobei FV(Δ*) ⊆ {ζ} ∪ X, so dass fur alle θ' ∈
GTERM gilt: [θ', ξ, Δ] = [θ', ζ, Δ*].

Beweis: Der Beweis wird mittels Induktion uber den Formelaufbau von Δ gefuhrt. Sei Δ =
^rΦ(θo, . θr-ι)^π ∈ AFORM. Seien {ξ, ζ} ∪ X ⊆ VAR, wobei {ξ, ζ} ∩ X = 0, und FV(Δ)
⊆ {ξ} ∪ X und ζ ∉ TT(Δ). Dann gilt fur alle i < r: FV(θi) ⊆ {ξ} ∪ X. Nach Theorem
1-17 gibt es dann fur alle i < r ein θ*i ∈ TERM, wobei FV(θ*i) ⊆ {ζ} ∪ X, so dass fur
alle θ' ∈ GTERM gilt: [θ', ξ, θ_i] = [θ', ζ, θ*]. Dann gilt mit Δ* = ^rΦ(θ*o, . O*,.-ιΓ, dass

<<   34   35   36   37   38   39   40   >>

More intriguing information