166 4 Theoreme zur deduktiven Konsequenzschaft
Hauptteil: Nun zum Nachweis, dass sich fur die einzelnen Falle AF ... IBF jeweils
ergibt, dass .ħ' ∈ RGS∖{0} und v) gilt:
(AF): Sei ⅛, ∈ AF(⅛'ΓDom(⅛')-1). Dann ist nach Definition 3-1 ⅛, = ⅛'ΓDom(⅛')-1 и
{(Dom(⅛')-1, rSei A(⅛'Dom(⅛')-1)π)} und mit vi') N = ⅛* и {(Dom(⅛)+1+Dom(⅛')-1,
rSei A(⅛'Dom(⅛')-ι)π)} ∈ AF(⅛*) ⊂ RGS∖{0}. Sodann ergibt sich mit Theorem 3-15-(ii),
dass VERS(⅛') = VERS(⅛'ΓDom(⅛')-1) и {(Dom(⅛')-1, rSei A(^'Dom(^')-1)n)} und
VERS(⅛+) = VERS(⅛*) и {(Dom(⅛)+1+Dom(⅛')-1, rSei A(⅛'Dom(⅛')-1)π)}. Mit v') ergibt
sich dann:
i ∈ Dom(VERS(⅛+))
gdw
i ∈ Dom(VERS(⅛*)) и {Dom(⅛)+1+Dom(⅛')-1}
gdw
i ∈ Dom(VERS(⅛)) и {Dom(⅛)} и {(Dom(⅛)+1+l | l ∈ Dom(VERS(⅛'∣Dom(⅛')-1))}
и {Dom(⅛)+1+Dom(⅛')-1}
gdw
i ∈ Dom(VERS(⅛)) и {Dom(⅛)} и {(Dom(⅛)+1+l | l ∈ Dom(VERS(⅛'))}
und damit, dass Dom(VERS(⅛+)) = Dom(VERS(⅛)) и {Dom(A)} и {(Dom(⅛)+1+l | l ∈
Dom(VERS(⅛'))} und somit (v) gilt.
(SEF, NEF): Sei nun ⅛, ∈ SEF(⅛'ΓDom(⅛')-1). Dann gibt es nach Definition 3-2 i ∈
Dom(⅛')-1, so dass mit iv') A(⅛'i) = A(^*Dom(^)+i+i) und i ∈ Dom(VANS(⅛'ΓDom(⅛')-1))
und K(⅛'∣'Dom(⅛')-1) = A(⅛*Dom(⅛)+1+Dom(⅛')-2) = K(⅛*) und es kein l mit i < l ≤
Dom(⅛')-2 gibt, so dass l ∈ Dom(VANS(⅛'ΓDom(⅛')-1)) und ⅛, = ⅛'ΓDom(⅛')-1 и
{(Dom(⅛')-1, rAlso A(⅛i) → K(⅛*)^l)}. Mit vi') ergibt sich dann: A' = ⅛* и
{(Dom(⅛)+1+Dom(⅛')-1, rAlso A(⅛i) → K(⅛*)^l)}. Sodann gilt mit iv') und v'):
Dom(⅛)+1+i ∈ Dom(VANS(⅛*)) und es gibt kein l mit Dom(⅛)+1+i < l ≤
Dom(⅛)+1+Dom(⅛')-2, so dass l ∈ Dom(VANS(⅛*)). Damit ist dann auch A' ∈
SEF(⅛*) ⊂ RGS∖{0}. Sodann ergibt sich mit Theorem 3-19-(iii), dass VERS(⅛') =
(VERS(^Dom(^')-1)∖{(j, ⅛'7) | i ≤ j < Dom(⅛')-1}) и {(Dom(⅛')-1, ^ Dom(⅛')-1)} und
VERS(⅛+) = (VERS(⅛*)X{(r, A) | Dom(⅛)+1+i ≤ r < Dom(⅛)+1+Dom(⅛')-1}) и
{(Dom(⅛)+1+Dom(⅛')-1, ⅛'Dom(⅛')-1)}. Mit v') ergibt sich dann:
k ∈ Dom(VERS(⅛+))
gdw
k ∈ (Dom(VERS(⅛*))∖{r | Dom(⅛)+1+i ≤ r < Dom(⅛)+1+Dom(⅛')-1}) и
{Dom(⅛)+1+Dom(⅛')-1}