Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie



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



More intriguing information

1. The name is absent
2. The name is absent
3. A Computational Model of Children's Semantic Memory
4. STIMULATING COOPERATION AMONG FARMERS IN A POST-SOCIALIST ECONOMY: LESSONS FROM A PUBLIC-PRIVATE MARKETING PARTNERSHIP IN POLAND
5. Financial Development and Sectoral Output Growth in 19th Century Germany
6. DETERMINANTS OF FOOD AWAY FROM HOME AMONG AFRICAN-AMERICANS
7. Visual Perception of Humanoid Movement
8. The name is absent
9. The name is absent
10. The name is absent