Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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

Theorem 3-16. VANS-Vermehrung nur bei AR

Wenn ft ∈ SEQ und ft' ∈ RGF(ft), dann:

(i)   Wenn VANS(ft) ⊂ VANS(ft'), dann ft' ∈ AF(ft), und

(ii)   Wenn VAN(ft) ⊂ VAN(ft'), dann ft' ∈ AF(ft).

Beweis: Sei ft ∈ SEQ und ft' ∈ RGF(ft). Zu (i): Sei VANS(ft) ⊂ VANS(ft'). Dann gibt
es (i, ft'_i) ∈ VANS(ft')∖VANS(ft). Dann ist (i, ft'_i) ∈ ANS(ft'). Sodann gilt mit Theorem
3-14-(ii): (i, ft'_i) = (Dom(ft), ftŋom(ft)) und somit (Dom(ft), ft'D>m(⅛)) ∈ ANS(ft'). Dann ist
mit Definition 3-1 ft' ∈ AF(ft). Zu (ii): Sei VAN(ft) ⊂ VAN(ft'). Dann ist mit Theorem
2-75 VANS(ft') £ VANS(ft) und somit gibt es (i, ft'_i) ∈ VANS(ft')∖VANS(ft). Damit
ergibt sich die Behauptung wie zu (i). ■

Theorem 3-17. VERS, VANS, VER und VAN bei Ubergangen ohne AR

Wenn ft ∈ SEQ und ft' ∈ RGF(ft)∖AF(ft), dann:

(i)   VERS(ft') ⊆ VERS(ft) ∪ {(Dom(ft), ft⅛_s))},

(ii)   VANS(ft') ⊆ VANS(ft),

(iii) VER(ft') ⊆ VER(ft) ∪ {K(ft')} und

(iv) VAN(ft') ⊆ VAN(ft).

Beweis: Sei ft' ∈ RGF(ft)∖AF(ft). (i) und (iii) folgen mit Theorem 3-14-(i) und -(iii). Zu
(ii): Mit ft' ∈ RGF(ft)∖AF(ft) und Definition 3-1 bis Definition 3-18 gilt, dass (Dom(ft),
ft'Dom(ft)) = (Dom(ft), ^rAlso A(ft'Dom(ft))^π) ∉ ANS(ft') und somit (Dom(ft), ft Dom(ft)) ∉
VANS(ft'). Damit ist mit Theorem 3-14-(ii) VANS(ft') ⊆ VANS(ft). Zu (iv): (iv) ergibt
sich mit Theorem 2-75 aus (ii). ■

Theorem 3-18. Nicht-Ieeres VANS ist hinreichend fur SE

Wenn ft ∈ SEQ und VANS(ft) ≠ 0, dann ist ft ∪ {(Dom(ft), rAlso A(ft₁max(Dom(VANS(ft)))) →
K(ft)"^l)} ∈ SEF(ft).

Beweis: Sei ft ∈ SEQ und VANS(ft) ≠ 0. Dann ist (max(Dom(VANS(ft))),
ftmax(Dom(VANS(ft)))) ∈ VANS(ft) und es ist A(ftDom(ft)-1) = K(ft) und es gibt kein l mit
max(Dom(VANS(ft))) < l ≤ Dom(ft)-1, so dass (l, ft_l) ∈ VANS(ft). Damit ist mit
Definition 3-2 ft ∪ {(Dom(ft), rAlso A(ftmax(Dom(VANS(⅛)))) → K(ft)^π)} ∈ SEF(ft). ■

<<   <   117   118   119   120   121   122   123   >   >>