Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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))))} к

<<   210   211   212   213   214   215   216   >>

More intriguing information