Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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Α → Β¹.

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 Α. ■

<<   179   180   181   182   183   184   185   >>

More intriguing information