Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

2.3 VERS, VANS, VER und VAN 115

Theorem 2-87. Beim Ubergang von Af Dom(A)-1 zu A verringert sich die Anzahl der verfug-
baren Annahmesatze maximal um eins

Wenn A ∈ SEQ, dann ∣VANS(AfDom(A)-1)∖VANS(A)∣ ≤ 1.

Beweis: Sei A ∈ SEQ. Dann ist VANS(AfDom(A)-Q)WANS(A) = 0 oder
VANS(AfDom(A)-1)∖VANS(A) ≠ 0. Im ersten Fall ist ∣(VANS(AfDom(A)-1)∖VANS(A)∣
= 0. Sei nun VANS(AfDom(A)-Q)WANS(A) ≠ 0. Dann gibt es mit Theorem 2-85 einen
geschlossenen Abschnitt ® in A, so dass VANS(AfDom(A)-Q)WANS(A) =
{(min(Dom(Φ)), Amin(Dom(<B)))}. Dann ist ∣VANS(Af Dom(A)-QWANS(A)I = 1. ■

Theorem 2-88. Beim Ubergang von AfDom(A)-1 zu A impliziert echte VAN-Inklusion echte
VANS-Inklusion

Wenn A ∈ SEQ und VAN(A) ⊂ VAN(AfDom(A)-I), dann VANS(A) ⊂
VANS(AfDom(A)-I).

Beweis: Sei A ∈ SEQ und sei VAN(A) ⊂ VAN(AfDom(A)-I). Dann gibt es ein Γ ∈
GFORM, so dass Γ ∈ VAN(AfDom(A)-I)WAN(A). Dann gibt es ein i ∈
Dom(VANS(Af Dom(A)-I)), so dass Γ = A(Ai). Dann ist i ∉ Dom(VANS(A)), denn sonst
ware Γ ∈ VAN(A). Damit ist VANS(AfDom(A)-I)WANS(A) ≠ 0 und mit Theorem 2-85
gibt es einen geschlossenen Abschnitt ® in A, so dass max(Dom(Φ)) = Dom(A)-I. Dann
ist ® ein SE- oder NE- oder EA-artiger Abschnitt in A. Dann ergibt sich mit Theorem
2-29, dass (Dom(A)-1, ADom(A)-1) ∉ ANS(A) und damit (Dom(A)-1, ADom(A)-1) ∉
VANS(A). Mit Theorem 2-81 gilt nun: VANS(A) ⊆ VANS(AfDom(A)-1) ∪
{(Dom(A)-1, A_Dom(_A)-i)}, so dass sich zunachst einmal VANS(A)   ⊆

VANS(AfDom(A)-1) ergibt und mit (i, Ai) ∈ VANS(AfDom(A)-1)∖VANS(A) ergibt
sich: VANS(A) ⊂ VANS(AfDom(A)-1). ■

Theorem 2-89. Vorbereitungstheorem (a) fur Theorem 2-91, Theorem 2-92 und Theorem 2-93
Wenn 21. ein Abschnitt in A ist und l ∈ Dom(Af max(Dom(2l.))), dann:

(l, Al) ∈ VERS(Afmax(Dom(^)))
gdw

Fur alle geschlossenen Abschnitte C in Afmax(Dom(^)) gilt: l < min(Dom(C)) oder
max(Dom(C)) ≤ l.

Beweis: Sei 21 ein Abschnitt in A und l ∈ Dom(Afmax(Dom(^))). (L-R): Sei nun zu-
nachst (l, A_l) ∈ VERS(Afmax(Dom(^))). Sei nun C ein geschlossener Abschnitt in

<<   90   91   92   93   94   95   96   >>

More intriguing information