240 6 Korrektheit und Vollstandigkeit des Redehandlungskalkuls
Falle entsprechen AF, SEF, NEF und PBF beziehungsweise AR, SE, NE und PB. Fur die
verbleibenden 13 Falle kann ausgeschlossen werden, dass die letzte Fortsetzung der be-
trachteten Ableitung zu einem der ersten vier Falle gehort. Die Korrektheit des Redehand-
lungskalkuls gegenuber der Modelltheorie wird dann am Ende des Abschnitts in Theorem
6-2 etabliert.
Theorem 6-1. Hauptbeweis der Korrektheit
Wenn ft ∈ RGS∖{0}, dann VAN(ft) к K(ft).
Beweis: Beweis per Induktion uber |ft|. Gelte dazu das Theorem fur alle l < |ft| und sei ft
∈ RGS∖{0}. Dann ist nach Definition 3-19 ft ∈ SEQ und fur alle j < Dom(ft) gilt: ftlj+1
∈ RGF(ftΓj). Sodann gilt mit Theorem 3-8 fur alle j ∈ Dom(ft), dass ftlj+1 ∈ RGS∖{0}.
Damit gilt nach I.V. fur alle j < Dom(ft)-1: VAN(ftlj+1) к K(ftlj+1). Nach Theorem
3-6 und Definition 3-18 gilt sodann, dass ft ∈ AF(ftlDom(ft)-1) oder ft ∈
SEF(ftlDom(ft)-1) oder ft ∈ SBF(ftlDom(ft)-1) oder ft ∈ KEF(ftlDom(ft)-1) oder ft ∈
KBF(ftlDom(ft)-1) oder ft ∈ BEF(ftΓDom(ft)-1) oder ft ∈ BBF(ftΓDom(ft)-1) oder ft ∈
AEF(ftΓDom(ft)-1) oder ft ∈ ABF(ftΓDom(ft)-1) oder ft ∈ NEF(ftΓDom(ft)-1) oder ft ∈
NBF(ftΓDom(ft)-1) oder ft ∈ UEF(ftΓDom(ft)-1) oder ft ∈ UBF(ftΓDom(ft)-1) oder ft
∈ PEF(ftΓDom(ft)-1) oder ft ∈ PBF(ftΓDom(ft)-1) oder ft ∈ IEF(ftΓDom(ft)-1) oder ft
∈ IBF(ftlDom(ft)-1).
Ferner ist ft ∈ AF(ftΓDom(ft)-1) и SEF(ftΓDom(ft)-1) и NEF(ftΓDom(ft)-1) и
PBF(ftlDom(ft)-1) oder ft ∉ AF(ftlDom(ft)-1) и SEF(ftlDom(ft)-1) и
NEF(ftΓDom(ft)-1) и PBF(ftΓDom(ft)-1). Damit lassen sich zwei Grobfalle unterschei-
den. Sei fur den ersten Fall nun zunachst ft ∈ AF(ftΓDom(ft)-1) и SEF(ftΓDom(ft)-1) и
NEF(ftΓDom(ft)-1) и PBF(ftΓDom(ft)-1). Damit lassen sich vier Unterfalle unterschei-
den, wobei fur die drei letzteren mit Definition 3-2, Definition 3-10 und Definition 3-16
gilt: Dom(ft)-1 ≠ 0 und damit ft!Dom(ft)-1 ∈ RGS∖{0} und VAN(ftlDom(ft)-1) к
K(ftlDom(ft)-1).
(AF): Sei ft ∈ AF(ftΓDom(ft)-1). Nach Theorem 3-15-(viii) ist dann K(ft) ∈ VAN(ft).
Theorem 5-14 liefert dann VAN(ft) к K(ft).
(SEF): Sei ft ∈ SEF(ftΓDom(ft)-1). Nach Theorem 3-19-(x) ist dann K(ft) =
rA(ftmax(Dom(VΛNS(ft∣Dom(ft)-1)))) → K(ftlDom(ft)-1)π. Sodann gilt VAN(ftlDom(ft)-1) к
K(ftΓDom(ft)-1). Mit Theorem 3-19-(ix) gilt VAN(ftlDom(ft)-1) = VAN(ft) и
{A(ftmax(Dom(VANS(ft∣Dom(ft)-1))))} und damit VAN(ft) и {A(ftmax(Dom(VANS(ft|Dom(ft)-1))))} к