Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 159

Α ∈ GFORM, so dass (i, ^rSei Α^π) ∈ VANS(A2) und (j, ^rSei Α^^l) ∈ VANS(A²). Dann
ware jedoch auch IVANS(A²)I > IVAN(A²)I. Also ist IVANS(A³)I ≤ IVAN(A³)I und damit
mit Theorem 2-76 insgesamt IVANS(A³)I = IVAN(A³)I∙

Sei A(Amax(Dom(VANS(A)))) ∉ VAN(A2)∙ Sei nun A4 = A'D(0, rSei A(Amax(Dom(VANS(A))))D.
Dann ist A⁴ ∈ AF(A²)∙ Dann ist mit Theorem 3-15-(viii) VAN(A⁴) = VAN(A²) и
{A(Amax(Dom(VANS(A))))} ⊆ VAN(A) und es ist K(A⁴) = A(Amax(Dom(VANS(A)))) und
∣VANS(A⁴)∣ = ∣VAN(A⁴)∣∙ Letzteres ergibt sich wie folgt:

Zunachst ist ∣VAN(A²)∣ = ∣VANS(A²)∣ und I{A(Amax(Dom(VANS(A))))}I = I{(Dom(A²), rSei
A( Amax(Dom(VANS(A)))DR Femer ist VANS(A²) ∩ {(Dom(A²), rSei A(Amax(Dom(VANS(A))))D
= 0 und VAN(A²) ∩ {A(A_max(_Dom(v_ANs(_A))))} = 0. Damit ist dann mit Theorem 3-15-(iv)
und -(viii):

IVANS(A⁴)I = ∣VANS(A²) U {(Dom(A²), rSei A(Amax(Dom(VANS(A))))DI

= ∣VANS(A²)∣+∣{(Dom(A²), rSei A(Am    m . )■)}

= |VAN(A²⁾|⁺|^{A(Amax(Dom(VANS(A)))^)}I

= ∣VAN(A2) ^{u {A(A}max(Dom(VANS(A)))^)}I

= IVAN(A⁴)I.

Sodann gilt mit Theorem 3-15-(vi), dass {A(Amax(Dom(VANS(A)))), ^rA(Amax(IDom(VANS(A)))) →
K(A)^^l} ⊆ VER(A⁴)∙ Damit ist A⁵ = A'^l"~" {(0, rAlso K(A)D ∈ SBF(A⁴) und mit
Theorem 3-27-(v) VAN(A⁵) ⊆ VAN(A⁴) ⊆ VAN(A) und K(A⁵) = K(A) und IVANS(A⁵)I
= IVAN(A⁵)I. Letzteres ergibt sich wie oben fur IVANS(A³)I = IVAN(A³)I unter Ruckgriff
auf IVANS(A⁴)I = IVAN(A⁴)I. ■

Das folgende Theorem dient insbesondere der Vorbereitung der Abgeschlossenheit unter
SE (Theorem 4-18-(i)).

Theorem 4-2. SE-Vorbereitungstheorem

Wenn A ∈ RGS∖{0} und Γ ∈ GFORM, dann gibt es ein A* ∈ RGS∖{0}, so dass

(i)   VAN(A*) ⊆ VAN(A),

(ii)   K(A*) = K(A) und

(iii) Fur alle i ∈ Dom(VANS(A*)): Wenn A(A*_i) = Γ, dann i = max(Dom(VANS(A*)))∙

Beweis: Sei A ∈ RGS∖{0} und Γ ∈ GFORM. Dann ist Γ ∉ VAN(A) oder Γ ∈ VAN(A).
Sei Γ ∉ VAN(A). Dann ist A selbst ein solches A* ∈ RGS∖{0}, so dass (i), (ii) und trivi-
alerweise (iii) gelten. Sei nun Γ ∈ VAN(A). Der Beweis wird mittels Induktion uber

<<   132   133   134   135   136   137   138   >>

More intriguing information