Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

258   6 Korrektheit und Vollstandigkeit des Redehandlungskalkuls

BelegungsvariantenH von bX fur DX sind: DX, IX, b' ⅛ [β, ξ, Δ]. Nach Theorem 5-8H-(i)
gilt somit DX, IX, bX =h ^rΛξΔ^^l = Γ.

Siebtens: Sei Γ = ^rVξΔ^^l. Dann gibt es mit Definition 6-2-(xiii) ein θ ∈ GTERMH, so
dass [θ, ξ, Δ] ∈ X. Nach Theorem 1-13H ist dann FGRADH([θ, ξ, Δ]) < FGRADH(Γ) und
damit gilt nach I.V. DX, IX, bX ⅛ [θ, ξ, Δ]. Sei nun β ∉ TTH(Δ). Sei nun b' = (bX∖{(β,
b_X(β))} ∪ {(β, [θ]_A)}. Dann ist b' in β eine BelegungsvarianteH von b_X fur D_X mit b'(β) =
[θ]_A. Sodann ist TDH(θ, DX, IX, bX) = [θ]_A und somit b'(β) = TDH(θ, DX, IX, bX). Wegen DX,
IX, bX ⅛ [θ, ξ, Δ] folgt dann mit Theorem 5-9H-(ii): DX, IX, b` ⅛ [β, ξ, Δ]. Also gibt es
ein b', das in β BelegungsvarianteH von bX fur DX ist, so dass DX, IX, b` =n [β, ξ, Δ]. Nach
Theorem 5-8H-(ii) gilt somit DX, IX, bX ⅛ ^rVξΔ^^l = Γ.

Nun wird gezeigt: Wenn ^r—Γ^^l ∈ X, dann DX, IX, bX ≠∣∣ Γ. Sei nun ^r—Γ ∈ X. Nach
Annahme ist 0 < FGRADH(Γ). Damit konnen sieben Falle unterschieden werden. Erstens:
Sei Γ = ^r—B^^l. Dann ist mit Definition 6-2-(ii) Β ∈ X und weil FGRADH(B) <
FGRADH(Γ) gilt nach I.V. DX, IX, bX =n B. Mit Theorem 5-4H-(ii) folgt DX, IX, bX ≠n
^r—B^^l = Γ. Zweitens: Sei Γ = ^rΑ ∧ B^^l. Dann ist mit Definition 6-2-(iv) ^r—Α^^l ∈ X oder
^r-B^π ∈ X und weil FGRADH(A) < FGRADH(Γ) und FGRADH(B) < FGRADH(Γ) gilt
nach I.V. DX, IX, bX ≠n A oder DX, IX, bX ≠n B. Mit Theorem 5-4H-(iii) folgt DX, IX, bX ≠n
^rA ∧ B^^l = Γ. Der dritte bis funfte Fall verlaufen analog.

Sechstens: Sei Γ = r-ΛξΔ^^l. Dann gilt mit Definition 6-2-(xii): Es gibt ein θ ∈
GTERMH, so dass —[θ, ξ, Δ] ∈ X. Nach Theorem 1-13H gilt dann FGRADH([θ, ξ, Δ]) <
FGRADH(Γ). Damit gilt nach I.V.: DX, IX, bX ≠n [θ, ξ, Δ]. Sei nun β ∉ TTH(Δ). Sei nun b'
in β die BelegungsvarianteH von b_X fur D_X mit b'(β) = [θ]_A. Dann ist TDH(θ, D_X, I_X, b_X) =
[θ]A und somit b^,(β) = TDH(θ, DX, IX, bX). Wegen DX, IX, bX ≠∏ [θ, ξ, Δ] folgt dann mit
Theorem 5-9H-(ii): DX, IX, b' ≠n [β, ξ, Δ]. Also gibt es ein b^l, das in β BelegungsvarianteH
von bX fur DX ist, so dass DX, IX, b' ≠∣∣ [β, ξ, Δ]. Somit gilt mit Theorem 5-8H-(i) DX, IX, bX
^H " - \ .

Siebtens: Sei Γ = r-VξΔ^^l. Dann gilt mit Definition 6-2-(xiv) fur alle θ ∈ GTERMH
r—[θ, ξ, Δ]^^l ∈ X. Da fur alle θ ∈ GTERMH nach Theorem 1-13H FGRADH([θ, ξ, Δ]) <
FGRADH(Γ), gilt damit nach I.V. fur alle θ ∈ GTERMH: DX, IX, bX ≠∏ [θ, ξ, Δ]. Sei nun β

<<   228   229   230   231   232   233   234   >>

More intriguing information