246 6 Korrektheit und Vollstandigkeit des Redehandlungskalkuls
tigen sind, werden die Beweise ausgefuhrt. Zum Beispiel wird der angefuhrte Zusam-
menhang RGS = RGSH ∩ SEQ in Theorem 6-6 mit gezeigt. In Theorem 6-3-(i) wird ge-
zeigt, dass sich ModelleH zu Modellen transformieren lassen, indem die jeweilige
InterpretationsfunktionH auf EAUS (bzw. in diesem Fall genauer: KONST ∪ FUNK ∪
PRA) beschrankt wird. Bei der Substitutionsoperation ist die Aquivalenz fur L-
Argumente trivial. Um Indexhaufungen hinter eckigen Klammern zu vermeiden (vgl. den
Beweis zu Theorem 6-10), wird daher auf den H-Index bei den Substitutionsklammern
verzichtet.
Die folgenden Theoreme sichern zunachst den Zusammenhang zwischen der Erfullbar-
keit in L und LH (Theorem 6-3 bis Theorem 6-5) sowie der Konsistenz in L und LH
(Theorem 6-6 bis Theorem 6-8). Daran schlieβt sich dann die Hintikka-Mengen-
Definition (Definition 6-2) an. Sodann wird gezeigt, dass alle konsistenten L-
Aussagenmengen eine Hintikka-Obermenge haben (Theorem 6-9) und dass jede
Hintikka-Menge erfullbarH ist (Theorem 6-10). Daraus ergibt sich dann die Vollstandig-
keit des Redehandlungskalkuls (Theorem 6-11).
Theorem 6-3. Beschrankungen von LH-Modellen auf L sind L-Modelle
(i) Wenn (D, I) ein ModellH ist, dann ist (D, 1((KONST ∪ FUNK ∪ PRA)) ein Modell,
(ii) b ist eine BelegungH fur D gdw b ist eine Belegung fur D, und
(iii) b' ist in β eine BelegungsvarianteH von b fur D gdw b' ist in β eine Belegungsvariante
von b fur D.
Beweis: Zu (i): Sei (D, I) ein ModellH. Dann ist nach Definition 5-2H I eine
InterpretationsfunktionH fur D. Dann ist nach Definition 5-1H Dom(I) = KONSTERW ∪
FUNK ∪ PRA. Mit KONST ⊆ KONSTERW, ist dann Dom( I ((KONST ∪ FUNK ∪
PRA)) = KONST ∪ FUNK ∪ PRA und es ist fur alle μ ∈ KONST ∪ FUNK ∪ PRA:
I ((KONST ∪ FUNK ∪ PRA)(μ) = I (μ) und damit ergibt sich mit Definition 5-1h und
Definition 5-1, dass I((KONST ∪ FUNK ∪ PRA) eine Interpretationsfunktion fur D und
damit (D, I ((KONST ∪ FUNK ∪ PRA)) ein Modell ist.
Zu (ii): Mit Definition 5-3H und Definition 5-3 gilt:
b ist eine BelegungH fur D
gdw
b ist eine Funktion mit Dom(b) = PAR, so dass fur alle β ∈ PAR : b(β) ∈ D