Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

3.3 VERS, VANS, VER und VAN in Ableitungen und bei einzelnen Ubergangen 155

i)   VAN(W) = VAN(W+1) и {A(W_ax(Dom(VANS(⅛o)))} ^un

j)   A(⅛) = ∖U )'

oder

(v) W+1 ∈ KEF(W) U BEF(W) и AEF(W) и UEF(W) и PEF(W) и IEF(W) und
a) VERS(φ[^i+1) ⊂ VERS(W) и {(i, ⅛)},
b) VANS(W+1) ⊂ VANS(W),
c) Wenn VANS(W+1) ⊂ VANS(W), dann ist .W+1 ∈ PBF(W),
d) VER(W+1) ⊂ VER(W) и {A(⅛)},
e) VAN(W+1) ⊂ VAN(W) und
f)  Wenn VAN(W+1) ⊂ VAN(W), dann ist .W+1 ∈ PBF(W)

oder

(vi) W+1 ∈ SBF(W) и KBF(W) и BBF(W) и ABF(W) и NBF(W) и UBF(W) и
IBF(W) und

a) VERS(W+1) ⊂ VERS(W) и {(i, ⅛)},

b) VANS(W+1) ⊂ VANS(W),

c) Wenn VANS(W+1) ⊂ VANS(W), dann ist .W+1 ∈ SEF(W) и NEF(W)
и PBF(W),

d) VER(W+1) ⊂ VER(W) и {A(⅛)},

e) VAN(W+1) ⊂ VAN(W) und

f) Wenn VAN(W+1) ⊂ VAN(W), dann ist ⅛f(i+1) ∈ SEF(W) и NEF(W)
и PBF(W).

Beweis: Sei ⅛ ∈ SEQ. (L-R): Sei nun ⅛ ∈ RGS. Dann gilt mit Definition 3-19 fur alle i ∈
Dom(W W+1 ∈ RGF(W). Dann gilt mit Definition 3-18 fur alle i ∈ Dom(W W+1 ∈
AF(W) и SEF(W) и NEF(W) и PBF(W) и KEF(W) и BEF(W) и AEF(W) и

UEF(W) и PEF(W) и IEF(W) и SBF(W) и KBF(W) и BBF(W) и ABF(W) и

NBF(W) и UBF(W) и IBF(W). Dann ergibt sich fur W+1 ∈ AF(W) mit Theorem
3-15, dass (i) gilt, fur W+1 ∈ SEF(W) mit Theorem 3-19, dass (ii) gilt, fur W+1 ∈
NEF(W) mit Theorem 3-20, dass (iii) gilt, fur W+1 ∈ PBF(W) mit Theorem 3-21,
dass (iv) gilt, fur W+1 ∈ KEF(W) и BEF(W) и AEF(W) и UEF(W) и PEF(W) и
IEF(W) mit Theorem 3-26, dass (v) gilt und zuletzt fur W+1 ∈ SBF(W) и KBF(W)
и BBF(W) и ABF(⅛Γi) и NBF(⅛Γi) и UBF(⅛Γi) и IBF(⅛Γi) mit Theorem 3-27, dass
(v) gilt.

(R-L): Gelte nun fur alle i ∈ Dom(⅛) einer der Falle (i) bis (vi). Dann gilt mit
Definition 3-18 fur alle i ∈ Dom(⅛): ⅛ti+1 ∈ RGF(W). Mit Definition 3-19 ist ⅛ ∈
RGS. ■

<<   129   130   131   132   133   134   135   >>

More intriguing information