230 5 Modelltheorie
5.2 Abgeschlossenheit der modelltheoretischen Konse-
quenzschaft
Der folgende Abschnitt fuhrt zur Korrektheit hin. Es wird fur jede Regel des Redehand-
Iungskalkuls (vgl. Kap. 3.1) beziehungsweise fur jede Fortsetzungsoperation (vgl. Kap.
3.2) ein modelltheoretisches Theorem bewiesen, dass der jeweiligen Abschlussklausel in
Kap. 4.2 entspricht, also Theorem 4-15 (AR) oder einer der Klauseln von Theorem 4-18.
Zunachst wird jedoch die modelltheoretische Monotonie (vgl. dazu Theorem 4-16) vo-
rausgeschickt.
Theorem 5-13. Modelltheoretische Monotonie
Wenn X' ⊆ X ⊆ GFORM und X' к Γ, dann X к Γ.
Beweis: Sei X' ⊆ X ⊆ GFORM und X' к Γ. Dann gilt fur alle D, I, b: Wenn D, I, b к
X', dann D, I, b к Γ. Gelte nun D, I, b к X. Dann gilt mit X' ⊆ X nach Theorem 5-10,
dass D, I, b к X' und damit nach Annahme, dass D, I, b к Γ. Also gilt fur alle D, I, b:
Wenn D, I, b к X, dann D, I, b к Γ. Also X к Γ. ■
Theorem 5-14. Modelltheoretische Entsprechung zu AR
Wenn X ⊆ GFORM und Α ∈ X, dann X к Α.
Beweis: Sei X ⊆ GFORM und Α ∈ X. Dann gilt nach Definition 5-9 fur alle D, I, b:
Wenn D, I, b к X, dann D, I, b к Α und damit X к Α. ■
Theorem 5-15. Modelltheoretische Entsprechung zu SE
Wenn X к Β und Α ∈ X, dann X\{Α} к rΑ → Β^l.
Beweis: Sei X к Β und Α ∈ X. Sei nun D, I, b к X∖{Α}. Dann ist (D, I) ein Modell und
b eine Belegung fur D und fur alle Δ ∈ X\{Α} gilt: D, I, b к Δ. Dann gilt entweder D,
I, b к Α oder D, I, b к Α. Im ersten Fall gilt, dass D, I, b к Δ fur alle Δ ∈ X, und so-
mit gilt D, I, b к X. Nach Voraussetzung gilt dann auch D, I, b к Β. Mit Theorem
5-4-(v) gilt dann D, I, b к rΑ → Β^l. Das gilt aber auch, falls D, I, b к Α. Also gilt fur
alle D, I, b, fur die D, I, b к X\{Α} gilt, auch D, I, b к rΑ → Β^l. Also X\{Α} к rΑ
→ Βπ. ■