162 4 Theoreme zur deduktiven Konsequenzschaft
{Α(⅛1maχ(Dom(VANsω⅛))} ⊆ VAN(⅛). Ferner ist mit Theorem 3-15-(vi)
{A(^ max(Dom(VANS(⅛1)))), A(^1max(Dom(VANS(⅛1)))) → K(-AΓ} ⊆ VER(⅛8). Sodann gilt mit Γ
∉ VAN(>Y) und Α(A 1max(Dom(VANS(^i)))) ≠ Γ auch Γ ∉ VAN(A8) und damit fur alle i ∈
Dom(VA∖S(.A8): A(⅛8i) ≠ Γ. Dann gilt trivialerweise fur alle i ∈ Dom(VANS(A8)):
Wenn A(⅛8i) = Γ, dann i = max(Dom(VANS(⅛8))). Dann ist .A9 = .A8"~"{(0, rAlso K(.AΓ)}
∈ SBF(⅛8) und mit Theorem 3-27-(v) gilt VAN(⅛9) ⊆ VAN(⅛8) ⊆ VAN(W). Ferner gilt
fur alle i ∈ Dom(VANS(W9)) wiederum trivialerweise: Wenn A(W9i) = Γ, dann i =
max(Dom(VA∖S(.A9))). Damit ist W’ das gesuchte Element von RGS∖{0}. ■
Theorem 4-3. Blockierende Annahmen
Wenn 21. ein geschlossener Abschnitt in W ist, i ∈ Dom(2l.) ∩ Dom(ANS(W)), Δ = A(Wi) und
PAR ∩ TT(Δ) = 0, dann gibt es ein j ∈ Dom(W), so dass i ≠ j und Δ ∈ TA(Wj).
Beweis: Sei 21 ein geschlossener Abschnitt in W, i ∈ Dom(W) ∩ Dom(ANS(W)), Δ =
A(Wi) und PAR ∩ TT(Δ) = 0. Mit Theorem 2-47 gilt dann, dass es einen geschlossenen
Abschnitt Y in W mit Y ⊆ W gibt, so dass i = min(Dom(Φ)). Mit Theorem 2-42 ist ®
dann ein SE- oder ein NE- oder ein EA-artiger Abschnitt in W. Sei ® ein SE- oder ein
NE-artiger Abschnitt in W. Dann gilt mit Definition 2-11 und Definition 2-12, dass
max(Dom(Y)) ∈ Dom(W), ma∖(Dom(Y)) ≠ i und Δ ∈ TA(Wmax(Dom(S))). Sei nun Y ein
EA-artiger Abschnitt in W. Dann gilt mit Definition 2-13: min(Dom(®))-1 ∈ Dom(W)
und min(Dom(®))-1 ≠ i. Sodann gibt es ξ ∈ VAR, Δ+ ∈ FORM, wobei FV(Δ+) ⊆ {ξ}
und β ∈ PAR, so dass A(Wmin(Dom(<B))-1) = r∀ξΔ+^, und Δ = A(Wmin(Dom(<B))) = [β, ξ, Δ+]. Da
nun nach Annahme PAR ∩ TT(Δ) = 0, ist dann β ∉ TT([β, ξ, Δ+]) und mit Theorem
1-14-(ii) Δ = [β, ξ, Δ+] = Δ+. Damit ist dann A(Wmin(Dom(S))-1) = r√ξΔπ und somit Δ ∈
TA(⅛min(Dom(S))-1) und die Behauptung gilt. ■
Theorem 4-4. Verkettung parameterfremder RGS-Elemente mit eingeschobener blockierender
Annahme
Wenn W, ⅛' ∈ RGS, PAR ∩ TTSEQ(W) ∩ TTSEQ(W) = 0 und α ∈ KONST∖(TTSEQ(W) ∪
TTSEQ(W)), dann gibt es ein W* ∈ RGS∖{0}, so dass
(i) Dom(W*) = Dom(W)+1+Dom(W'),
(ii) W*t^Dom(W) = W,
(iii) ⅛*Dom(f>) = rSei α = α1,
(iv) Fur alle i ∈ Dom(W) ist W i ⅛ * Dom(W)+1+i,