Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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

Dom(ft) oder ft_j∙ ≠ Σ oder Α(Σ) ist in ft bei j nicht verfugbar. Da ftti+1 eine Beschran-
kung von ft ist und j ∈ Dom(ftΓi+1), kann nur letzteres zutreffen. Es gilt also j ∈
Dom(ft) und ftj = Σ und Α(Σ) ist in ft bei j nicht verfugbar. Damit gibt es nach Definition
2-26 einen geschlossenen Abschnitt 'd in ft, so dass min(Dom(^)) ≤ j < max(Dom(^)).
Nach Theorem 2-64-(viii) ist 'd auch ein geschlossener Abschnitt in ftΓmax(Dom(^))+1.
Ware nun i < max(Dom(^)), so ware wegen j ∈ Dom(ftΓi+1) und damit j ≤ i auch
mιn(Dom('d)) ≤ i < max(Dom(^)). Damit ware entgegen der Annahme A(ft_i) = Γ nicht in
ft bei i verfugbar. Also max(Dom(^)) ≤ i und damit max(Dom(^))+1 ≤ i+1. Also
ftΓmax(Dom(W))+1 ⊂ ftΓi+1. Mit Theorem 2-62-(viii) ist 'd dann auch ein geschlossener
Abschnitt in ftΓi+1. Also gibt es einen geschlossenen Abschnitt 'd in ftΓi+1, so dass
min(Dom(W)) ≤ j < max(Dom(^)). Widerspruch! Also (j, Σ) ∈ VERS(ft).

Zu (ii), (iii) und (iv): Mit Theorem 2-72 ergibt sich (ii) aus (i). Mit Theorem 2-74 ergibt
sich (iii) aus (i). Mit Theorem 2-75 ergibt sich (iv) aus (ii). ■

Theorem 3-30. VERS, VANS, VER und VAN in Ableitungen

Wenn ft ∈ SEQ, dann:

ft ∈ RGS

gdw

Fur alle i ∈ Dom(ft):

(i) ft[7+1 ∈ AF(ft[7) und

a) VERS(ftfi+1)∖VERS(ftfi) = {(i, ft.,)},

b) VERS(ft[7+1) = VERS(ft[7) и {(i, ft.,)},

c) VANS(fti+1)∖VANS(ftN) = {(i, ft,i)},

d) VANS(ft[7+1) = VANS(ft[7) и {(i, ft.,)},

e) VER(ft[7+1)∖VER(ft[7) ⊂ {A(fti)},

f) VER(ft[7+1) = VER(ftN) и {A(fti)},