Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

252   6 Korrektheit und Vollstandigkeit des Redehandlungskalkuls

Man beachte, dass G wohldefiniert ist, da kein α ∈ KONSTNEU Teilterm eines Γ ∈ X
⊆ GFORM ist und da fur jedes k ∈ N beim Schritt von G(k) zu G(k+1) hochstens ein
Element von KONSTNEU zu den Teiltermen von Elementen von G(k) hinzukommen
kann: Fur alle k ∈ N ist KONSTNEU∖TTFMH( G (k)) abzahlbar unendlich.

Nach Konstruktion von G gilt nun zunachst:

a) X = G (0) ⊆ URan( G),

b) Fur alle k ∈ N ist G(k) konsistentH,

c) Wenn l ≤ k, dann G(l) ⊆ G(k),

d) Wenn Y ⊆ URan(G) und |Y| ∈ N, dann gibt es ein k ∈ N, so dass Y ⊆ G(k),

e) URan( G) ist konsistentH.

a) ergibt sich direkt aus der Definition von G. Nun zu b): G(0) = X ⊆ GFORM ist nach
Voraussetzung konsistent und damit mit Theorem 6-8 konsistentH. Gelte nun fur k: G(k)
ist konsistentH. Ware nun G(k+1) inkonsistentH. Dann gilt nicht fur alle Γ ∈ G(k+1), dass
G(k) H Γ, da sonst mit Theorem 4-19_h auch G(k) inkonsistentH ware. Damit ist der Fall
G(k+1) ⊆ G(k) ∪ {^rθ = θ^^l} fur θ ∈ GTERM ausgeschlossen. Also ist F(k) ∈ G(k). Fur
diesen Fall sind aus demselben Grund die Falle (i*)-(iv*), (vii*), (ix*), (xii*) und (xv*)
ausgeschlossen (was sich leicht mit den LH-Versionen der Theoreme aus Kap. 4.2 ergibt).
Also ist F(k) ∈ G(k) und F(k) = ^r-(Α ∧ Β)^π oder F(k) = ^rΑ ∨ Β^π oder F(k) = ^rΑ → Β^π
oder F(k) = ^rΑ → Β^π oder F(k) = ^r-(Α → Β)^π oder F(k) = ^r-ΛξΔ^π oder F(k) = ^rVξΔ^π.
Angenommen F(k) = ^r— (Α ∧ Β)^^l. Dann ist nach (v*) G(k+1) = G(k) ∪ {^r-Α^^l}, falls
G(k) ∪ {^r-Α^^l} konsistentH, G(k+1) = G(k) ∪ { ^r∙lΓ } sonst. Dann ist G(k) ∪ {^r-Α^^l}
inkonsistentH und G(k+1) = G(k) ∪ {^r-Β^^l} ebenfalls. Dann gilt mit Theorem 4-22H:
G (k) HH Α und G (k) HH Β und somit G (k) HH ^rΑ ∧ Β^^l. Damit ware dann auch G (k)
inkonsistentH. Widerspruch! Die anderen junktoralen Falle zeigt man analog. Sei nun
F(k) = ^r-ΛξΔ^^l. Dann ist nach (xiii*) G(k+1) = G(k) ∪ {^r-[α, ξ, Δ]^^l} fur das α ∈
KONSTNEU mit dem kleinsten Index, fur welches gilt α ∉ TTFMH(G(k)). Dann ist G(k)
∪ {^r-[α, ξ, Δ]^π} inkonsistentH. Dann gilt G(k) HH [α, ξ, Δ]. Dann gilt aber wegen α ∉
TTFMH(G(k)) und ^r—ΛξΔ^^l ∈ G(k), dass α ∉ TTFMH(G(k) ∪ {Δ}) und damit mit

<<   222   223   224   225   226   227   228   >>

More intriguing information