Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie



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 ir: [θ*, θδ, θi] = θi oder es
gibt ein
ir, so dass θ* TT([θ*, θδ, θi]). Wenn [θ*, θδ, θi] = θi fur alle ir, 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 absent
2. 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