200 4 Theoreme zur deduktiven Konsequenzschaft
mit Theorem 3-27-(v) ist VAN(ft+) ⊆ VAN(ft*) ⊆ X ∪ Y und es ist K(ft+) = Β. Also
gilt mit Theorem 3-12: X ∪ Y H Β.
Zu (iv) (KB), (viii) (AE), (xii) (NB), (xiii) (UE), (xiv) (UB), (xv) (PE): (iv) wird exempla-
risch gezeigt. Klauseln (viii), (xii), (xiii), (xiv) und (xv) ergeben sich analog. Sei fur (iv)
X H rΑ ∧ Β^l oder X H rΒ ∧ Α^l. Sei nun X H rΑ ∧ Β^l. Dann gibt es nach Theorem
3-12 ft ∈ RGS∖{0}, so dass VAN(ft) ⊆ X und K(ft) = rΑ ∧ 1Γ. Dann ist mit Theorem
2-82 rΑ ∧ 1Γ ∈ VER(ft) und daher nach Definition 3-5 ft' = ft~{(0, rAlso Α^l)} ∈
KBF(ft) ⊆ RGS∖{0} und mit Theorem 3-27-(v) ist VAN(ft') ⊆ VAN(ft) ⊆ X und es ist
K(ft') = Α. Also gilt wiederum nach Theorem 3-12: X H Α. Fur den Fall, dass X H rΒ ∧
.Α zeigt man analog, dass dann ebenfalls X H Α gilt.
Zu (vi:)(BE*): Sei X H Β und Α ∈ X und Y H Α und Β ∈ Y. Dann gilt mit (i): X\{Α}
H rΑ → Βπ und Y∖{Β} H rΒ → Α^l. Dann gilt mit (v): (X\{Α}) ∪ (Y∖{Β}) H rΑ → Βπ.
Zu (ix) (AB): Sei X H rΑ ∨ Β^l und Y H rΑ → Γ^l und Z H rΒ → Γ^l. Dann ergibt sich
mit zweifacher Anwendung von (iii): X ∪ Y ∪ Z H r(Α ∨ Β) ∧ ((Α → Γ) ∧ (Β → Γ))^l.
Dann gibt es mit Theorem 3-12 ft ∈ RGS∖{0}, so dass VAN(ft) ⊆ X ∪ Y ∪ Z und K(ft)
= r(Α ∨ Β) ∧ ((Α → Γ) ∧ (Β → Γ))^l. Nun gibt es ein α ∈ KONST∖TTSEQ(ft). Damit
lasst sich ft wie folgt zu einem ft6 ∈ SEQ mit ft6ΓDom(ft) = ft fortsetzen:
ft1 = ft ∪ {(Dom (ft),
rSei α = απ)}
rAlso Α V Βπ)}
rAlso (Α → Γ) ∧ (Β → Γ)1)}
rAlso Α → Γ^l)}
rAlso Β → Γ1)}
rAlso Γ1)}.
ft2 = ft1 ∪ {(Dom(ft1),
ft3 = ft2 ∪ {(Dom(ft2),
ft4 = ft3 ∪ {(Dom(ft3),
ft5 = ft4 ∪ {(Dom(ft4),
ft6 = ft5 ∪ {(Dom(ft5),
Zunachst ist ft6Dom(ft) ∈ ASATZ. Sodann gilt mit α ∈ KONST∖TTSEQ(ft) auch α ∉
TTFM({Α, Β, Γ}) und damit insgesamt, dass fur alle k mit 1 ≤ k ≤ 6 gilt: Wenn i ∈
Dom(ftk), dann: α ∈ TT(ftki) gdw i = Dom(ft). Sodann gilt fur alle k mit 1 ≤ k ≤ 6, dass
Dom(ft) ∈ Dom(ANS(ftk)). Mit Theorem 4-3 gilt damit, dass fur alle k mit 1 ≤ k ≤ 6 gilt:
Es gibt keinen geschlossenen Abschnitt ʌl in ftk fur den min(Dom(^)) ≤ Dom(ft) ≤
max(Dom(^)). Damit ergibt sich auch, dass fur alle k mit 1 ≤ k ≤ 6 gilt, dass Dom(ft) =
max(Dom(VANS(ftk))). Mit Theorem 3-19-(i), Theorem 3-20-(i), Theorem 3-21-(i) und