Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 165

Damit gilt dann auch:

viii') Dom(W) ∈ Dom(V ANS(W⁺)), Dom(W) ∈ Dom(VANS(W*)) und Dom(W) ≤
max(Dom(VANS(W*)))∙

Um Sonderbetrachtungen bei SBF, KEF, KBF, BEF, BBF, AEF, ABF, NBF, UEF, UBF,
PEF, IEF und IBF zu vereinfachen wird nun noch vorbereitend gezeigt:

ix') Wenn W⁺ ∈ SEF(W*) и NEF(W*) и PBF(W*), dann W' ∈ SEF(WfDom(W)-I) ∪
NEF(WfDom(W)-I) ∪ PBF(WfDom(W)-I).

Vorbereitungsteil: Sei zunachst W⁺ ∈ SEF(W*)∙ Dann gilt mit Definition 3-2, Theorem
3-19-(i) und vii') und viii'), dass es Dom(W)+1+i ∈ Dom(VANS(W*)) gibt, so dass mit i')
und iv') A(^*Dom(⅛)+1+i) = A(Wi) und K(W*) = A((W*Dom(W)+1+Dom(W')-2) = A(W∏om(⅞∙)-2) =
K(W'fDom(W')-1) und es kein l mit Dom(W)+1+i < l ≤ Dom(W)+1+Dom(W')-2 gibt, so
dass l ∈ Dom(VANS(W*)) und W⁺ = W* ∪ {(Dom(W)+1+Dom(W')-1, ^rAlso
A(W*Dom(W)+1+i) → K(W*)^^l} = W* и {(Dom(W)+1+Dom(W')-1, rAlso A(Wi) →
K(WfDom(W)-1)^π }. Dann gilt mit i'), iv') und v'): i ∈ Dom(VANS(W'fDom(W')-1)) und
es gibt kein l mit i < l ≤ Dom(W')-2, so dass l ∈ Dom(VANS(W'fDom(W')-1))∙ Ferner gilt
dann mit vi'), dass W' = WfDom(W)-1 и {(Dom(W')-1, rAlso A(Wi) →
K(WfDom(W)-1)^^l} und damit ist dann insgesamt W' ∈ SEF(W'fDom(W')-1)∙ Fur den Fall,
dass W⁺ ∈ NEF(W*), zeigt man analog, dass dann auch W' ∈ NEF(W'fDom(W')-1)∙

Sei nun W⁺ ∈ PBF(W*)∙ Dann gilt mit Definition 3-15, Theorem 3-21-(i), A(W*_Dom(_W)) =
rα = α^^l und vii') und viii'), dass es β ∈ PAR, ξ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊂ {ξ},
und Dom(W)+1+i ∈ Dom(VERS(W*)) gibt, so dass mit i') und iv') r√ξΔ^π =
A(W*Dom(W)+1+i) = A(W'i) und [β, ξ, Δ] = A(W*Dom(W)+2+i) = A(W'i+1), wobei Dom(W)+2+i ∈
Dom(VANS(W*)) und K(W*) = A(W*Dom(W)÷1÷Dom(W')-2) = Λ(W^,Dom<W>2) = K(W'fDom(W')-1)
und W⁺ = W* и {(Dom(W)+1+Dom(W')-1, rAlso K(W*)^^l} = W* и
{(Dom(W)+1+Dom(W')-1, rAlso K(W'fDom(W')-1)^π } und β ∉ TTFM({Δ, K(W*)}) und es
kein j ≤ Dom(W)+1+i gibt, so dass β ∈ TT(W*_j) und es kein l mit Dom(W)+2+i < l ≤
Dom(W)+1+Dom(W')-2 gibt, so dass l ∈ Dom(VANS(W*))∙ Dann gilt mit i'), iv') und v'): i
∈ Dom(VERS(W'fDom(W')-1)) und i+1 ∈ Dom(VANS(W'fDom(W')-1)) und β ∉
TTFM({Δ, K(W'fDom(W')-1)}) und es gibt kein j ≤ i, so dass β ∈ TT(W'_j), und es gibt
kein l mit i+1 < l ≤ Dom(W')-2, so dass l ∈ Dom(VANS(W'fDom(W')-1)∙ Ferner gilt dann
mit vi'), dass W' = W'fDom(W')-1 и {(Dom(W')-1, rAlso K(W'fDom(W')-1)^π } und damit ist
dann insgesamt W' ∈ PBF(W'fDom(W')-1)∙

<<   138   139   140   141   142   143   144   >>

More intriguing information