Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.2 Eigenschaften der deduktiven Konsequenzschaft 199

Β) und dass A(^3Dom_№')) = Α ≠ ^r-(Α ∧ Β) = ■ Аш .. ) . Damit gilt mit Theorem
2-42, Definition 2-11, Definition 2-12 und Definition 2-13, dass fur alle k mit 1 ≤ k ≤ 3
gilt: Es gibt keinen geschlossenen Abschnitt A in .^k fur den min(Dom(A)) = Dom(.').
Mit Theorem 2-47 gilt damit fur alle k mit 1 ≤ k ≤ 3: Es gibt keinen geschlossenen Ab-
schnitt A in .^k fur den min(Dom(A)) ≤ Dom(.') ≤ max(Dom(A)). Damit ergibt sich
auch, dass fur alle k mit 1 ≤ k ≤ 3 gilt, dass Dom(.') = max(Dom(VANS(.^k))). Mit
Theorem 3-19-(i), Theorem 3-20-(i), Theorem 3-21-(i) und Theorem 2-61 gilt dann, dass
fur alle k mit 2 ≤ k ≤ 3 gilt: .^k ∉ SEF(.^k-1) ∪ NEF(.^k-1) ∪ PBF(.^k-1).

Hingegen ist erstens nach Definition 3-1 .¹ ∈ AF(.') ⊆ RGS∖{0} und mit Theorem
3-15 VERS(.¹) = VERS(.') ∪ {(Dom(.'), ^rSei Α^π)} und (Dom(.'), ^rSei Α^π) ∈
VANS(.') ∪ {(Dom(.'), rSei Α^π)} = VANS(.¹) und Β ∈ VER(.') ⊆ VER(.¹) und Α
∈ VER(.¹). Also ist zweitens nach Definition 3-4 .² ∈ KEF(.¹) ⊆ RGS∖{0} und mit
Theorem 3-25 VERS(.²) = VERS(.¹) ∪ {(Dom(.¹), rAlso Α ∧ Β^^l)}. Damit gilt
(Dom(.'), rSei Α^π) ∈ VANS(.¹) = VANS(.²) und rΑ ∧ Β^π ∈ VER(.²). Also ist drit-
tens nach Definition 3-5 .³ ∈ KBF(.²) ⊆ RGS∖{0} und mit Theorem 3-25 VERS(.³) =
VERS(.²) ∪ {(Dom(.²), rAlso Β^^l)}. Damit gilt Dom(.') ∈ Dom(.³) und A(.³D_om(⅞')) =
Α und (Dom(.'), rSei Α^π) ∈ VANS(.²) = VANS(.³) und A(.³Dom(.3)-1) = Β und es gibt
kein l mit Dom(.') < l ≤ Dom(.³)-1, so dass (l, .³_l) ∈ VANS(.³). Damit ist nach
Definition 3-2 .⁴ ∈ SEF(.³) ⊆ RGS∖{0} und mit Theorem 3-19-(iv) und -(v) VANS(.⁴)
= VANS(.³)∖{(max(Dom(VANS(.³))), ш...... o... V . ... )} = VANS(.³)∖{(Dom(.'),
rSei Α^^l)} = VANS(.¹)∖{(Dom(.'), rSei Α^π)} = (VANS(.') ∪ {(Dom(.'), rSei
Α^π)})∖{(Dom(.'), rSei Α^^l)} = VANS(.')∖{(Dom(.'), rSei Α^π)} ⊆ VANS(.'). Mit
Theorem 2-75 ist dann VAN(.⁴) ⊆ VAN(.') und wegen Α ∉ VAN(.') und VAN(.') ⊆
VAN(.) ⊆ X dann auch VAN(.⁴) ⊆ VAN(.)∖{Α} ⊆ X∖{Α}. Da K(.⁴) = rΑ → Β^π,
gilt mit Theorem 3-12 X∖{Α} H га → Β^^l.

Zu (ii) (SB), (iii) (KE), (v) (BE), (vii) (BB), (xviii) (IB): (ii) wird exemplarisch gezeigt.
Klauseln (iii), (v), (vii) und (xviii) ergeben sich analog. Sei fur (ii) X H Α und Y H га →
Β^^l. Dann gibt es nach Theorem 3-12 ., .' ∈ RGS∖{0}, so dass VAN(.) ⊆ X und K(.)
= Α und VAN(.') ⊆ Y und K(.') = rΑ → 1Γ. Mit Theorem 4-14 gibt es dann ein .* ∈
RGS∖{0}, so dass Α, га → Β^π ∈ VER(.*) und VAN(.*) ⊆ VAN(.) ∪ VAN(.') ⊆ X
∪ Y. Nach Definition 3-3 ist dann .⁺ = ⅛*^{(0, rAlso Β^^l)} ∈ SBF(.*) ⊆ RGS∖{0} und

<<   <   172   173   174   175   176   177   178   >   >>