Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie



28    1 Zum grammatischen Rahmen

Gelte die Behauptung nun fur ¼ ʌɪ FORM. Also FGRAD(Δ0) = FGRAD([θ, θ', Δo])
und FGRAD(Δ
1) = FGRAD([θ, θ', Δ1]).

Zu JFORM: Sei nun Δ = r√Δ0Γ. Dann ist FGRAD(Δ) = FGRAD(rΔl√) =
FGRAD(Δ
o)+1 = FGRAD([θ, θ', Δ])+1 = FGRAD(r-[θ, θ', Δ]π) = FGRAD([θ, θ',
rΔ0^l ]) = FGRAD([θ, θ', Δ]). Sei nun Δ = r0 ψ Δ1)~l fur ein ψ JUNK{ r-^l}. Dann
ist FGRAD(Δ) = FGRAD(
ro ψ Δι)π) = max({FGRAD(Δ0), FGRAD(Δi)})+1 =
max({FGRAD([θ, θ', Δ
]), FGRAD([θ, θ', Δi])})+1 = FGRAD(r([θ, θ', Δ] ψ [θ, θ', Δι])π)
= FGRAD([θ, θ',
ro ψ Δι)^l ]) = FGRAD([θ, θ', Δ]).

Zu QFORM: Sei nun Δ = rΠξΔ0^l. Sei zunachst ξ θ'. Dann ist FGRAD(Δ) =
FGRAD(
rΠξΔoπ) = FGRAD(Δ0)+l = FGRAD([θ, θ', Δ0])+l = FGRAD(rΠξ[θ, θ', Δ0]π) =
FGRAD([θ, θ',
rΠξΔ0π ]) = FGRAD([θ, θ', Δ]). Sei sodann ξ = θ'. Dann ist FGRAD(Δ) =
FGRAD(
rΠξΔ0π) = FGRAD([θ, θ', rΠξΔ0π ]) = FGRAD([θ, θ', Δ]). ■

Theorem 1-14. Fur alle Substituenda und Substitutionsorte gilt, dass entweder alle geschlos-
senen Terme Teilterme des jeweiligen Substitutionsergebnisses sind oder fur alle geschlosse-
nen Terme das jeweilige Substitutionsergebnis mit dem Substitutionsort identisch ist
Wenn θ' ATERM, θ* TERM, Δ FORM, dann:

(i)   θ TT([θ, θ', θ*]) fur alle θ GTERM oder [θ, θ', θ*] = θ* fur alle θ GTERM und

(ii)   θ TT([θ, θ', Δ]) fur alle θ GTERM oder [θ, θ', Δ] = Δ fur alle θ GTERM.

Beweis: Seien θ' ATERM, θ* TERM, Δ FORM. Zu (i): Der Beweis wird mittels
Induktion uber den Termaufbau von θ* gefuhrt. Sei θ*
ATERM. Falls θ' = θ*, dann ist
[θ, θ', θ*] = θ und mithin θ
TT([θ, θ', θ*]) fur alle θ GTERM. Falls θ' θ*, dann ist
[θ, θ', θ*] = θ* fur alle θ
GTERM. Gelte die Behauptung nun fur θ*0, ., θ*r-1
TERM und sei θ* = rφ(θ*0, ., θ*r)π FTERM. Dann ist [θ, θ', θ*] = [θ, θ', rφ(θ*0, .,
θ*
r)π ] = rφ([θ, θ', θ*0], ., [θ, θ', θ*r])π fur alle θ GTERM. Nun gilt nach I.V. fur al-
le
i r: θ TT([θ, θ', θ*i]) fur alle θ GTERM oder [θ, θ', θ*i] = θ*i fur alle θ
GTERM. Angenommen es gibt ein i r, so dass θ TT([θ, θ', θ*i]) fur alle θ GTERM.
Dann ist auch θ
TΓ(rφ([θ, θ', θ*0], ., [θ, θ', θ*r])π) = TT([θ, θ', θ*]) fur alle θ
GTERM. Angenommen es gibt kein i r, so dass θ TT([θ, θ', θ*i]) fur alle θ
GTERM. Dann gilt nach I.V. [θ, θ', θ*i] = θ*i fur alle θ GTERM und alle i r. Also [θ,
θ', θ*] =
rφ([θ, θ', θ*0], ., [θ, θ', θ*r])π = rφ(θ*0, ., θ*r)π = θ* fur alle θ GTERM.



More intriguing information

1. Banking Supervision in Integrated Financial Markets: Implications for the EU
2. Gender and headship in the twenty-first century
3. Evidence on the Determinants of Foreign Direct Investment: The Case of Three European Regions
4. WP RR 17 - Industrial relations in the transport sector in the Netherlands
5. Peer Reviewed, Open Access, Free
6. Evaluating Consumer Usage of Nutritional Labeling: The Influence of Socio-Economic Characteristics
7. Database Search Strategies for Proteomic Data Sets Generated by Electron Capture Dissociation Mass Spectrometry
8. Publication of Foreign Exchange Statistics by the Central Bank of Chile
9. The name is absent
10. The value-added of primary schools: what is it really measuring?