158 4 Theoreme zur deduktiven Konsequenzschaft
RGS-treu ist (Theorem 4-8). Der dazu gehorige Beweis dient als Vorlage fur den Beweis
des Folgetheorems (Theorem 4-9), das seinerseits das Generalisierungstheorem (Theorem
4-24) vorbereitet. Zudem wird gezeigt, dass die simultane Substitution mehrerer neuer
und paarweise verschiedener Parameter fur paarweise verschiedene Parameter RGS-treu
ist (Theorem 4-10). Sodann werden Eigenschaften von UE- und UB-Fortsetzungen von
Ableitungen etabliert, bis dann schlussendlich mit Theorem 4-14 gezeigt werden kann,
dass sich je zwei beliebige Ableitungen so verbinden lassen, dass einerseits die verfugba-
ren Annahmen insgesamt nicht mehr werden und andererseits die Konklusionen beider
Ableitungen noch verfugbar sind.
Theorem 4-1. Non-redundantes VANS
Wenn S ∈ RGS∖{0} dann gibt es ein S* ∈ RGS∖{0}, so dass
(i) VAN(S*) ⊆ VAN(S)
(ii) K(S*) = K(S) und
(iii) ∣VANS(S*)∣ = ∣VAN(S*)∣.
Beweis: Sei S ∈ RGS∖{0}. Der Beweis wird mittels Induktion uber ∣VANS(S)∣ gefuhrt.
Sei ∣VANS(S)∣ = 0. Offenbar gilt VAN(S) ⊆ VAN(S) und K(S) = K(S) und mit
Theorem 2-77 folgt auch ∣VAN(S)∣ = 0.
Sei nun ∣VANS(S)∣ = k ≠ 0. Gelte die Behauptung fur alle S' ∈ RGS∖{0} mit
∣VANS(S')∣ < k. Dann ist mit Theorem 2-76 ∣VAN(S)∣ ≤ ∣VANS(S)∣. Sei nun ∣VAN(S)∣ ≠
∣VANS(S)∣. Dann ist ∣VAN(S)∣ < ∣VANS(S)∣. Sodann ist VANS(S) ≠ 0. Damit ist mit
Theorem 3-18 S1 = S ∪ {(Dom(S), rAlso A(Smax(Dom(VANS(S)))) → K(S)π)} ∈ SEF(S).
Dann ist mit Theorem 3-19-(ix) VAN(S1) ⊆ VAN(S) und mit Theorem 3-19-(iv) und
-(v) ergibt sich ∣VANS(S1)∣ < k. Dann gibt es nach I.V. S2 ∈ RGS∖{0}, so dass VAN(S2)
⊆ VAN(S1), K(S2) = K(S1) und ∣VANS(S2)∣ = ∣VAN(S2)∣. Dann ist VAN(S2) ⊆
VAN(S1) ⊆ VAN(S) und K(S2) = K(S1) = rA(Smax(Dom(VANS(S)))) → K(S)'. Nun ist
A(Smax(Dom(VANS(S)))) ∈ VAN(S2) oder A(Smax(Dom(VANS(S)))) ∉ VAN(S2).
Sei A(Smax(Dom(VANS(S)))) ∈ VAN(S2). Dann ist S3 = S2^{(0, rAlso K(S)π)} ∈ SBF(S2)
und mit Theorem 3-27-(v) VAN(S3) ⊆ VAN(S2) ⊆ VAN(S1) ⊆ VAN(S) und es ist
K(S3) = K(S) und ∣VANS(S3)∣ = ∣VAN(S3)∣. Letzteres ergibt sich wie folgt:
Ware ∣VANS(S3)∣ > ∣VAN(S3)∣. Dann gabe es i, j ∈ Dom(S3) mit i ≠ j und Α ∈
GFORM, so dass (i, rSei Α^l) ∈ VANS(S3) und (j, rSei Α^l) ∈ VANS(S3). Da mit
Theorem 3-27-(ii) VANS(S3) ⊆ VANS(S2) gabe es damit i, j ∈ Dom(S2) mit i ≠ j und