Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

160  4 Theoreme zur deduktiven Konsequenzschaft

∣VANS(T)∣ gefuhrt. Sei ∣VANS(T)∣ = 0. Mit Theorem 2-77 folgt entgegen der Annahme
∣VAN(T)∣ = 0, womit die Behauptung trivial gilt.

Sei nun ∣VANS(T)∣ = k ≠ 0. Gelte die Behauptung fur alle T' ∈ RGS∖{0} mit
∣VANS(T')∣ < k. Dann gibt es mit Theorem 4-1 ein T¹ ∈ RGS∖{0}, so dass VAN(T¹) ⊂
VAN(T), K(T¹) = K(T) und ∣VANS(T¹)∣ = ∣VAN(T¹)∣ ≤ ∣VAN(T)∣ ≤ ∣VANS(T)∣. Sodann
gilt mit ∣VANS(T¹)∣ = ∣VAN(T¹)∣ fur alle Β ∈ VAN(T¹): Es gibt genau ein i ∈
Dom(VANS(T¹)), so dass Β = A(T_i). Angenommen, fur alle i ∈ Dom(VANS(T¹)): Wenn
A(T¹_i) = Γ, dann i = max(Dom(VANS(T¹))). Dann ist T¹ das gesuchte Element von
RGS\{0}.

Gelte nun nicht fur alle i ∈ Dom(VANS(T¹)): Wenn A(T¹_i) = Γ, dann i =
max(Dom(VANS(T¹))). Dann gibt es ein i ∈ Dom(VANS(T¹)), so dass A(T¹_i) = Γ und i
≠ max(Dom(VANS(T¹))). Dann ist VANS(T¹) ≠ 0 und Γ ∈ VAN(T¹) und es gilt fur alle
j ∈ Dom(VANS(T¹)): Wenn A(Tj) = Γ, dann j = i und damit auch j ≠
max(Dom(VANS(T¹))). Damit ist A(T¹_max(_Dom(VANS(_T¹)))) ≠ Γ. Sodann gilt mit VANS(T¹)
≠ 0, Theorem 3-18 und K(T¹) = K(T): T² = T¹ ^{(0, ^rAlso Α(T¹max(Dom(VANS(T¹)))) →
K(T)^π)} ∈ SEF(T¹). Dann gilt mit Theorem 3-22, dass VAN(T²) ⊆
VAN(T¹)∖{Α(T¹max(Dom(VΛNS(T⅝)} ⊆ VAN(T). Mit Theorem 3-19-(iv) und (v) gilt so-
dann ∣VANS(T²)∣ < ∣VANS(T¹)∣ ≤ ∣VANS(T)∣ und es gilt: ∣VANS(T²)∣ = ∣VAN(T²)∣.
Letzteres ergibt sich wie folgt:

Ware ∣VANS(T²)∣ > ∣VAN(T²)∣. Dann gabe es i, j ∈ Dom(T²) mit i ≠ j und Α ∈
GFORM, so dass (i, rSei Α^^l) ∈ VANS(T²) und (j', rSei Α^^l) ∈ VANS(T²). Da mit
Theorem 3-19-(v) VANS(T²) ⊆ VANS(T1) gabe es damit i, j ∈ Dom(T1) mit i ≠ j und Α
∈ GFORM, so dass (i, rSei Α^^l) ∈ VANS(T1) und (j', rSei Α^^l) ∈ VANS(T1). Dann ware
jedoch auch ∣VANS(T1)∣ > ∣VAN(T1)∣. Also ist ∣VANS(T²)∣ ≤ ∣VAN(T²)∣ und damit mit
Theorem 2-76 insgesamt ∣VANS(T²)∣ = ∣VAN(T²)∣.

Nun ist ∣VANS(T²)∣ < ∣VANS(T¹)∣ ≤ ∣VANS(T)∣ = k. Damit gibt es nach I.V. ein T³ ∈
RGS∖{0}, so dass VAN(T³) ⊆ VAN(T²) und K(T³) = K(T²) und fur alle i ∈
Dom(VANS(T³)): Wenn A(T³_i) = Γ, dann i = max(Dom(VANS(T³))). Dann ist VAN(T³)
⊆ VAN(T²) ⊆ VAN(T¹) ⊆ VAN(T), Α(T¹max(Dom(VΛNS(T`)))) ∉ VAN(T³) und K(T³) =
rΑ(T¹max(Dom(vлNS(τ')))) → K(T)^^l. Dann lassen sich mit Γ ∈ VAN(T³) oder Γ ∉ VAN(T³)
zwei Falle unterscheiden:

Erster Fall: Γ ∈ VAN(T³). Dann ist Γ = A(T³_max(_Dom(v_ANS(_T³)))) und fur alle i ∈
Dom(VANS(T³)): Wenn Γ = A(T_i), dann i = max(Dom(VANS(T³))). Dann ist mit

<<   133   134   135   136   137   138   139   >>

More intriguing information