34 1 Zum grammatischen Rahmen
Theorem 1-19. Eindeutige Substitutionsorte (a) fur Terme
Wenn θ, θ+ ∈ TERM, θ* ∈ GTERM∖(TT(θ) ∪ TT(θ+)) und θ§ ∈ ATERM und wenn [θ*, θ§, θ]
= [θ*, θδ, θ+], dann θ = θ+.
Beweis: Durch Induktion uber den Termaufbau von θ. Sei θ ∈ ATERM. Sei nun θ+ ∈
TERM, θ* ∈ GTERM∖(TT(θ) ∪ TT(θ+)) und θδ ∈ ATERM und sei [θ*, θδ, θ] = [θ*, θδ,
θ+]. Sei nun θδ = θ. Dann ist [θ*, θδ, θ] = θ*. Dann ist θ* = [θ*, θ, θ+]. Da nach Vorausset-
zung θ* ∉ TT(θ+) und mithin θ+ ≠ θ*, ist dann θ = θ+. Sei nun θδ ≠ θ. Dann ist [θ*, θδ, θ]
= θ. Dann ist θ = [θ*, θδ, θ+], womit sich wegen θ* ∉ TT(θ) mit Theorem 1-14-(i) eben-
falls ergibt, dass θ = θ+.
Gelte die Behauptung nun fur {θ0, ..., θr-ι} ⊆ TERM und sei rφ(θ0, ... θr-1)^l ∈
FTERM. Sei nun θ+ ∈ TERM, θ* ∈ GTERM∖(TT( rφ(θo, . θr-ʃ) ∪ TT(θ+)) und θδ ∈
ATERM und sei [θ*, θδ, rφ(θo, ., θr-ι)π] = [θ*, θδ, θ+]. Also [θ*, θδ, θ+] = rφ([θ*, θδ, θɑ],
., [θ*, θδ, θr-ι])^l ∈ FTERM. Ware θ+ ∈ ATERM. Dann ware θδ ≠ θ+ oder θδ = θ+. An-
genommen θδ ≠ θ+. Dann ist θ+ = [θ*, θδ, θ+] = rφ([θ*, θδ, θ0], ., [θ*, θδ, θr-1])^l ∈
FTERM. Widerspruch! Angenommen θδ = θ+. Dann ist θ* = [θ*, θδ, θ+] = rφ([θ*, θδ, θ0],
., [θ*, θδ, θr-1])π. Mit Theorem 1-14-(i) gilt dann fur alle i < r: [θ*, θδ, θi] = θi oder es
gibt ein i < r, so dass θ* ∈ TT([θ*, θδ, θi]). Wenn [θ*, θδ, θi] = θi fur alle i < r, dann θ* =
rφ([θ*, θδ, θ0], ., [θ*, θδ, θr-ι])^l = rφ(θ0, ., θr-ι)^l und damit entgegen der Vorausset-
zung θ* ∈ TT(rφ(θ0, . θr-1)^l). Wenn es andererseits ein i < r gibt, so dass θ* ∈ TT([θ*,
θδ, θi]), dann ist θ* echter Teilterm von rφ([θ*, θδ, θ0], ., [θ*, θδ, θr-1])^l, also echter Teil-
term von sich selbst. Widerspruch zu Theorem 1-8. Also θ+ ∉ ATERM, sondern θ+ ∈
FTERM. Also gibt es {θ'o, ., θ'k-ι} ⊆ TERM und φ' ∈ FUNK, so dass θ+ = rφ'(θ'o, .,
θ'k-1)π. Damit ist rφ'([θ*, θδ, θ'o], ., [θ*, θδ, θ'k-1])π = [θ*, θδ, rφ'(θ'o, ., ‰)π] = [θ*, θs,
θ+] = rφ([θ*, θδ, θ0], ., [θ*, θδ, θr-1])^l. Mit Theorem 1-11-(ii) gilt dann k = r und φ' = φ
und [θ*, θδ, θi] = [θ*, θδ, θ'i] fur alle i < r. Mit I.V. ergibt sich, dass θi = θ'i fur alle i < r.
Damit ist dann rφ(θ0, ., θr-1)^l = rφ'(θ'0, ., θ'k-1)^l = θ+. ■
Theorem 1-20. Eindeutige Substitutionsorte (a) fur Formeln
Wenn Δ, Δ+ ∈ FORM, θ* ∈ GTERM∖(TT(Δ) ∪ TT(Δ+)) und θ§ ∈ ATERM und wenn [θ*, θδ,
Δ] = [θ*, θδ, Δ+], dann Δ = Δ+.
Beweis: Seien Δ, Δ+ ∈ FORM, θ* ∈ GTERM∖(TT(Δ) ∪ TT(Δ+)) und θδ ∈ ATERM und
[θ*, θδ, Δ] = [θ*, θδ, Δ+]. Wie im Induktionsschritt des vorangehenden Beweises fur funk-
More intriguing information
1. The name is absent2. Micro-strategies of Contextualization Cross-national Transfer of Socially Responsible Investment
3. Cross-Country Evidence on the Link between the Level of Infrastructure and Capital Inflows
4. The name is absent
5. The name is absent
6. The name is absent
7. National urban policy responses in the European Union: Towards a European urban policy?
8. EU Preferential Partners in Search of New Policy Strategies for Agriculture: The Case of Citrus Sector in Trinidad and Tobago
9. The name is absent
10. The name is absent