Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

134   3 Der Redehandlungskalkul

Theorem 3-7. Die regelgemaβe Fortsetzung eines RGS-Elements Juhrt zu einem nicht-leeren
RGS-Element

Wenn S ∈ RGS und S' ∈ AF(S) и SEF(S) и SBF(S) ∪ KEF(S) ∪ KBF(S) и BEF(S) и
BBF(S) и AEF(S) и ABF(S) и NEF(S) и NBF(S) и UEF(S) и UBF(S) и PEF(S) и
PBF(S) и IEF(S) и IBF(S), dann ist S' ∈ RGS∖{0}.

Beweis: Sei S ∈ RGS und S' ∈ AF(S) и SEF(S) и SBF(S) и KEF(S) и KBF(S) и
BEF(S) и BBF(S) и AEF(S) и ABF(S) и NEF(S) и NBF(S) и UEF(S) и UBF(S) и
PEF(S) и PBF(S) и IEF(S) и IBF(S). Dann ist nach Definition 3-18 S' ∈ RGF(S). Mit
Theorem 3-5 gilt dann S = S'tDom(S')-1. Damit gilt wegen S ∈ RGS mit Theorem 3-6,
dass S' ∈ RGS. Mit Theorem 3-1 ist sodann S' ≠ 0 und damit S' ∈ RGS∖{0}. ■

Theorem 3-8. S ist genau dann ein nicht-leeres RGS-Element, wenn S eine nicht-leere Se-
quenz ist und alle nicht-leeren AnJangsabschnitte von S nicht-leere RGS-Elemente sind
S ∈ RGS∖{0} gdw S ∈ SEQ∖{0} und fur alle i ∈ Dom(S): SN+1 ∈ RGS∖{0}.

Beweis: (L-R): Sei S ∈ RGS∖{0}. Dann gilt nach Definition 3-19, dass S ∈ SEQ und fur
alle i ∈ Dom(S), dass SΓ(i+1) ∈ RGF(SΓi). Dann ist mit der Voraussetzung S ∈
SEQ∖{0}. Sei nun 0 ∈ Dom(S). Dann ist also St1 ∈ RGF(SΓ0) = RGF(0). Nun gilt mit
Theorem 3-6 0 ∈ RGS und damit ergibt sich mit St1 ∈ RGF(0) wiederum mit Theorem
3-6, dass St1 ∈ RGS und mit 0 ∈ Dom(SΓ1) dann auch St1 ∈ RGS∖{0}. Gelte nun fur i:
wenn i ∈ Dom(S), dann SΓi+1 ∈ RGS∖{0}. Sei nun i+1 ∈ Dom(S). Dann ist i ∈
Dom(S) und damit nach I.V. auch SΓi+1 ∈ RGS∖{0}. Nun ist aber SΓi+2 ∈ RGF(SΓi+1).
Wegen S ∈ SEQ und i+1 ∈ Dom(S) ist SΓi+1 = (SΓ(i+2))ΓDom(SΓ(i+2))-1. Mit
Theorem 3-6 und Theorem 3-1 ist dann SΓi+2 ∈ RGS∖{0}.

(R-L): Gelte nun umgekehrt S ∈ SEQ∖{0} und fur alle i ∈ Dom(S): SΓi+1 ∈ RGS∖{0}.
Dann ist mit S ∈ SEQ∖{0} Dom(S)-1 ∈ Dom(S) und somit SΓDom(S)-1+1 = S ∈
RGS∖{0}. ■

Unter Ruckgriff auf Definition 3-19 wird nun ein Ableitungsbegriff eingefuhrt. Darauf
aufbauend wird dann, nach einigen Theoremen und einer Beispielbetrachtung zum Ablei-
tungskonzept, ein entsprechender Konsequenzbegriff etabliert.

<<   108   109   110   111   112   113   114   >>

More intriguing information