Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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

(v)  VAN(S') ⊆ VAN(S) und

(vi) Wenn VAN(S') ⊂ VAN(S), dann ist S' ∈ PBF(S).

Beweis: Sei S ∈ SEQ und S' ∈ KEF(S) ∪ BEF(S) ∪ AEF(S) ∪ UEF(S) ∪ PEF(S) ∪
IEF(S). Dann gilt mit Definition 3-18 S' ∈ RGF(S). Sodann gilt mit Definition 3-4,
Definition 3-6, Definition 3-8, Definition 3-12, Definition 3-14 und Definition 3-16: Es
gibt Α, Β ∈ GFORM und θ ∈ GTERM und β ∈ PAR und ξ ∈ VAR und Δ ∈ FORM, wo-
bei FV(Δ) ⊆ {ξ}, so dass S' = S ∪ {(Dom(S), ^rAlso Α ∧ Β^^l)} oder S' = S ∪
{(Dom(S), rAlso Α → Β^^l)} oder S' = S ∪ {(Dom(S), rAlso Α ∨ Β^^l)} oder S' = S ∪
{(Dom(S), rAlso ΛξΔ^-l)} oder S' = S ∪ {(Dom(S), rAlso VξΔ^-l)} oder S' = S ∪
{(Dom(S), rAlso θ = θ^^l)}. Dann ist mit eindeutiger Lesbarkeit (Theorem 1-10, Theorem
1-11 und Theorem 1-12) (Dom(S), -⅜'D_om(⅛)) ∉ ANS(S') und damit nach Definition 3-1 S'
∉ AF(S). Dann ergeben sich (i), (ii), (iv) und (v) mit Theorem 3-17-(i), -(ii), -(iii) and
-(iv). Sodann ergibt sich mit Theorem 3-19-(x), Theorem 3-20-(x) und eindeutiger Les-
barkeit, dass S' ∉ SEF(S) ∪ NEF(S). Damit gilt mit Theorem 3-23: Wenn VANS(S') ⊂
VANS(S), dann S' ∈ PBF(S) und somit (iii). Sei nun fur (vi): VAN(S') ⊂ VAN(S).
Dann gilt VAN(S) £ VAN(S') und damit mit Theorem 2-75 VANS(S) £ VANS(S').
Damit gilt mit (ii): VANS(S') ⊂ VANS(S) und damit mit (iii), dass S' ∈ PBF(S). ■

Theorem 3-27. VERS, VANS, VER und VAN bei SB, KB, BB, AB, NB, UB, IB

Wenn S ∈ SEQ und S' ∈ SBF(S) ∪ KBF(S) ∪ BBF(S) ∪ ABF(S) ∪ NBF(S) ∪ UBF(S) ∪
IBF(S), dann:

(i)   VERS(S') ⊆ VERS(S) ∪ {(Dom(S), ‰ms))},

(ii) VANS(S') ⊆ VANS(S),

(iii) Wenn VANS(S') ⊂ VANS(S), dann ist S' ∈ SEF(S) ∪ NEF(S) ∪ PBF(S),

(iv) VER(S') ⊆ VER(S) ∪ {K(S')},

(v)  VAN(S') ⊆ VAN(S) und

(vi) Wenn VAN(S') ⊂ VAN(S), dann ist S' ∈ SEF(S) ∪ NEF(S) ∪ PBF(S).

Beweis: Sei S ∈ SEQ und S' ∈ SBF(S) ∪ KBF(S) ∪ BBF(S) ∪ ABF(S) ∪ NBF(S) ∪
UBF(S) ∪ IBF(S). Dann gilt mit Definition 3-18 S' ∈ RGF(S). Sodann gilt mit
Definition 3-3, Definition 3-5, Definition 3-7, Definition 3-9, Definition 3-11, Definition
3-13 und Definition 3-17: S' = S ∪ {(Dom(S), rAlso A(S'_Dom(_S))ⁿ)}. Dann ist (Dom(S),
S'Dom(S)) ∉ ANS(S') und damit S' ∉ AF(S). Dann ergeben sich (i), (ii), (iv) und (v) mit
Theorem 3-17-(i), -(ii), -(iii) and -(iv). Sodann ergibt sich (iii) mit Theorem 3-23. Sei nun

<<   125   126   127   128   129   130   131   >>

More intriguing information