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. SOCIOECONOMIC TRENDS CHANGING RURAL AMERICA
2. Industrial Cores and Peripheries in Brazil
3. WP 92 - An overview of women's work and employment in Azerbaijan
4. The name is absent
5. Land Police in Mozambique: Future Perspectives
6. Stillbirth in a Tertiary Care Referral Hospital in North Bengal - A Review of Causes, Risk Factors and Prevention Strategies
7. ROBUST CLASSIFICATION WITH CONTEXT-SENSITIVE FEATURES
8. An Efficient Circulant MIMO Equalizer for CDMA Downlink: Algorithm and VLSI Architecture
9. Housing Market in Malaga: An Application of the Hedonic Methodology
10. The name is absent