Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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(⅛'D_om(⅛')_-1)^π)} und mit vi') N = ⅛* и {(Dom(⅛)+1+Dom(⅛')-1,
^rSei A(⅛'D_om(⅛')_-ι)^π)} ∈ AF(⅛*) ⊂ RGS∖{0}. Sodann ergibt sich mit Theorem 3-15-(ii),
dass VERS(⅛') = VERS(⅛'ΓDom(⅛')-1) и {(Dom(⅛')-1, rSei A(^'_Dom(^')_-1)ⁿ)} und
VERS(⅛⁺) = VERS(⅛*) и {(Dom(⅛)+1+Dom(⅛')-1, rSei A(⅛'D_om(⅛')_-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, ⅛'₇) | 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, ⅛'D_om(⅛')_-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}

<<   139   140   141   142   143   144   145   >>

More intriguing information