Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

6.2 Vollstandigkeit des Redehandlungskalkuls 259

∉ TTH(Δ) und sei b' in β eine BelegungsvarianteH von bX fur DX. Dann ist b'(β) ∈ DX und
somit gibt es ein θ ∈ GTERMH, so dass b'(β) = [θ]_A. Dann ist TDH(θ, D_X, I_X, b_X) = [θ]_A
und somit b'(β) = TDH(θ, DX, IX, bX). Wegen DX, IX, bX kH [θ, ξ, Δ] folgt dann mit
Theorem 5-9H-(ii): DX, IX, b' kH [β, ξ, Δ]. Also gilt fur alle b', die in β
BelegungsvariantenH von bX fur DX sind: DX, IX, b` ≠∏ [β, ξ, Δ]. Mit Theorem 5-8H-(ii)
gilt somit DX, IX, bX ≠∏ ^rVξΔ^^,.

Damit wurde gezeigt: Wenn Γ ∈ X, dann DX, IX, bX ⅛ Γ und wenn ^r—Γ ∈ X, dann
DX, IX, bX ≠n Γ. Allein aus dem ersten Teil ergibt sich bereits gemaβ Definition 5-17H und
Definition 5-9H, dass X erfullbarH ist. ■

Theorem 6-11. Modelltheoretische Konsequenzschaft impliziert Ableitbarkeit

Fur alle X, Γ: Wenn X к Γ, dann X — Γ.

Beweis: Sei X к Γ. Dann ist nach Definition 5-10 X ∪ {Γ} ⊆ GFORM und damit auch
X ∪ {^r—Γ} ⊆ GFORM. Sodann ist mit Theorem 5-12 X ∪ {^r—Γ^^l} nicht erfullbar. Wa-
re nun X ∪ {^r—Γ} konsistent. Dann gabe es mit Theorem 6-9 eine Hintikka-Menge Z,
so dass X ∪ {^r-Γ^ⁱ} ⊆ Z. Dann gilt mit Theorem 6-10, dass Z erfullbarH ist, und mit
Theorem 5-11H ware damit aber auch X ∪ {^r-1} erfullbarH. Damit ware dann mit
Theorem 6-5 aber X ∪ {^r—Γ^^l} erfullbar. Widerspruch! Also ist X ∪ {^r—Γ^^l} nicht kon-
sistent und damit inkonsistent. Damit gilt mit Theorem 4-22: X — Γ. ■

Theorem 6-12. Kompaktheitssatz

(i)   Wenn X к Γ, dann gibt es ein Y ⊆ X, so dass ∣ Y∣ ∈ N und Y к Γ,

(ii)   Wenn X ⊆ GFORM, dann: X ist erfullbar gdw fur alle Y ⊆ X mit ∣ Y∣ ∈ N gilt: Y ist

erfullbar.

Beweis: Zu (i): Sei Xk Γ. Mit Theorem 6-11 gilt dann X — Γ. Also gibt es nach
Definition 3-21 ein Д so dass ⅛ eine Ableitung von Γ aus VAN(⅛) ist und VAN(⅛) ⊆
X. Dann ist nach Theorem 3-9 ∣VAN(φ)∣ ∈ N. Auβerdem gilt nach Definition 3-20 f ∈
RGS∖{0} und damit Theorem 6-1 auch VAN(⅛) к Γ. Also (i).

<<   229   230   231   232   233   234   235   >>

More intriguing information