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√Δ₀Γ. Dann ist FGRAD(Δ) = FGRAD(^rΔ_l√) =
FGRAD(Δo)+1 = FGRAD([θ, θ', Δ∣])+1 = FGRAD(^r-[θ, θ', Δ∣]^π) = FGRAD([θ, θ',
^r—Δ₀^^l ]) = FGRAD([θ, θ', Δ]). Sei nun Δ = ^r(Δ₀ ψ Δ1)~^l fur ein ψ ∈ JUNK∖{ ^r-^^l}. Dann
ist FGRAD(Δ) = FGRAD(^r(Δo ψ Δι)^π) = max({FGRAD(Δ0), FGRAD(Δi)})+1 =
max({FGRAD([θ, θ', Δ∣]), FGRAD([θ, θ', Δi])})+1 = FGRAD(^r([θ, θ', Δ∣] ψ [θ, θ', Δι])^π)
= FGRAD([θ, θ', ^r(Δo ψ Δι)^^l ]) = FGRAD([θ, θ', Δ]).

Zu QFORM: Sei nun Δ = ^rΠξΔ₀^^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 θ*₀, ., θ*_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.

<<   <   30   31   32   33   34   35   36   >   >>