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 θ0, ., θr-1 ∈ TERM und sei θ = rφ(θ0, ... θ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φ(θ*0, . θ*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