206 4 Theoreme zur deduktiven Konsequenzschaft
gilt mit VAN(⅛) ⊆ Y, dass fur alle Γ ∈ VAN(⅛) gilt: X H Γ und damit X Mh VAN(⅛).
Damit gilt dann X H Β. ■
Theorem 4-20. Cut
Wenn X ∪ {Β} H Α und Y H Β, dann X ∪ Y H Α.
Beweis: Gelte X ∪ {Β} H Α und Y H Β. Dann gilt mit Theorem 4-18-(i): X∖{Β} H rΒ →
Α^l und damit mit Theorem 4-16, dass X H rΒ → Α^l. Damit gilt mit Theorem 4-18-(ii):
X ∪ Y H Α. ■
Theorem 4-21. Deduktionstheorem und Umkehrung
X ∪ {Α} H Β gdw X H rΑ → Β1.
Beweis: Gelte zunachst X ∪ {Α} H Β. Dann gilt mit Theorem 4-18-(i): X\{Α} H rΑ →
If und damit mit Theorem 4-16, dass X H rΑ → Β^l. Gelte nun umgekehrt X H rΑ →
Β^l. Dann ist nach Definition 3-21 und Theorem 3-9 rΑ → Β^l ∈ GFORM und damit auch
Α ∈ GFORM. Damit gilt mit Theorem 4-15: {Α} H Α und somit mit Theorem 4-18-(ii):
X ∪ {Α} H Β. ■
Theorem 4-22. Inkonsistenz und Ableitbarkeit
X H Α gdw X ∪ {r—Α^l} ist inkonsistent.
Beweis: (L-R): Gelte zunachst X H Α. Dann ist mit Definition 3-21 und Theorem 3-9 X
⊆ GFORM und Α ∈ GFORM. Dann ist r—Α^l ∈ GFORM und damit gilt mit Theorem
4-16, dass X ∪ {r—Α^l} H Α, und mit Theorem 4-15: X ∪ {r—Α^l} H r—Α^l. Damit gilt
nach Definition 3-24, dass X ∪ {r—Α^l} inkonsistent ist.
(R-L): Sei nun X ∪ {r—Α^l} inkonsistent. Dann gilt nach Definition 3-24, dass X ∪
{r—Α^l} ⊆ GFORM und dass es ein Γ ∈ GFORM gibt, so dass X ∪ {r—Α^l} H Γ und X
∪ {r—Α^l} H r—Γ^l. Dann gilt mit Theorem 4-18-(xi): X\{r—Α^l} H r——Α^l und damit
mit Theorem 4-16: X H r——Α^l. Daraus folgt mit Theorem 4-18-(xii), dass X H Α. ■