Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

6.2 Vollstandigkeit des Redehandlungskalkuls 257

gdw

<TDH(θo, Dx, Iχ, bχ), ..., TDH(θr-ι, Dχ, Iχ, bχ)) ∈ Iχ(Φ)

gdw

<[θ]o, ., [θ]r-ɪ) ∈ Iχ(Φ)

gdw

^rΦ(θo, ., θr-ɪr ∈ X

gdw

Α ∈ X.

Nun wird durch Induktion uber FGRADH(Γ) gezeigt: Wenn Γ ∈ X, dann D_x, I_x, b_χ =∣∣ Γ
und wenn ^r∙Γ ∈ X, dann D_x, I_x, b_χ ≠n Γ. Daraus ergibt sich unmittelbar D_x, I_x, b_χ =H
x und damit, dass x erfullbarH ist.

Gelte die Behauptung fur alle k < FGRADH(Γ). Sei nun FGRADH(Γ) = 0. Dann ist Γ ∈
AFORMH. Sei nun Γ ∈ X. Dann gilt: D_x, I_x, b_χ =_h Γ. Sei nun ^r—Γ ∈ X. Dann gilt mit
Definition 6-2-(i), Γ ∉ X und damit: D_x, I_x, b_χ ≠n Γ.

Sei nun FGRADH(Γ) > 0. Dann ist Γ ∈ JFORMH ∪ QFORMH. Zunachst wird nun ge-
zeigt: Wenn Γ ∈ X, dann D_x, I_x, b_χ =H Γ. Sei dazu Γ ∈ X. Es konnen sieben Falle unter-
schieden werden. Erstens: Sei Γ = ^r∙lΓ. Dann ist FGRADH(B) < FGRADH(Γ) und damit
nach I.V. D_x, I_x, b_χ ≠n B und somit D_x, I_x, b_χ =_η ^r—B^^l = Γ. Zweitens: Sei Γ = ^rΑ ∧ 1Γ.
Dann gilt mit Definition 6-2-(iii): Α, l ∈ x. Da sodann FGRADH(Α) < FGRADH(Γ) und
FGRADH(B) < FGRADH(Γ), gilt damit nach I.V.: D_x, I_χ, b_χ =∣∣ Α und D_x, I_x, b_χ =∣∣ B
und damit D_x, I_x, b_χ =H ^rΑ ∧ B^^l = Γ. Der dritte bis funfte Fall verlaufen analog.

Sechstens: Sei Γ = ^rΛξΔ^^l. Dann gilt mit Definition 6-2-(xi) [θ, ξ, Δ] ∈ X fur alle θ ∈
GTERMH. Da fur alle θ ∈ GTERMH nach Theorem 1-13H FGRADH([θ, ξ, Δ]) <
FGRADH(Γ), gilt damit nach I.V. fur alle θ ∈ GTERMH: D_x, I_χ, b_χ =_η [θ, ξ, Δ]. Sei nun β
∈ PAR∖TTH(Δ) und sei b' in β eine BelegungsvarianteH von b_χ fur D_x. Dann ist b'(β) ∈
D_x und somit gibt es ein θ ∈ GTERMH, so dass b'(β) = [θ]_A. Dann ist TDH(θ, D_x, I_x, b_x) =
[θ]A und somit b'(β) = TDH(θ, Dχ, Iχ, bχ). Wegen Dχ, Iχ, bχ =H [θ, ξ, Δ] folgt dann mit

Theorem 5-9H-(ii): D_x, I_χ, b' I=H  [β,  ξ, Δ]. Also  gilt fur  alle  b', die in β

<<   227   228   229   230   231   232   233   >>

More intriguing information