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. Neural Network Modelling of Constrained Spatial Interaction Flows
2. The name is absent
3. The Challenge of Urban Regeneration in Deprived European Neighbourhoods - a Partnership Approach
4. The English Examining Boards: Their route from independence to government outsourcing agencies
5. Moffett and rhetoric
6. Meat Slaughter and Processing Plants’ Traceability Levels Evidence From Iowa
7. Telecommuting and environmental policy - lessons from the Ecommute program
8. Globalization and the benefits of trade
9. What Lessons for Economic Development Can We Draw from the Champagne Fairs?
10. From Aurora Borealis to Carpathians. Searching the Road to Regional and Rural Development