Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

132   3 Der Redehandlungskalkul

Als nachstes soil gezeigt werden, dass RGF(S) fur keine Sequenz S leer ist, dass also
jede Sequenz irgendwie fortgesetzt werden kann.

Theorem 3-2. RGF ist fur keine Sequenz leer

Wenn S ∈ SEQ, dann ist RGF(S) ≠ 0.

Beweis: Sei S ∈ SEQ. Nun gilt, dass ^rxo^^l ∈ GTERM. Also ist nach Definition 3-16 S и
{(Dom(S), ^rAlso x₀ = x₀∣)} ∈ IEF(S). Also ist S и {(Dom(S), ^rAlso x₀ = x₀∣)} ∈
RGF(S) ≠ 0. ■

Theorem 3-3. Die Elemente von RGF(S) sind Fortsetzungen von S um genau einen Satz
Wenn S ∈ SEQ und S' ∈ RGF(S), dann gibt es Ξ ∈ PERF und Γ ∈ GFORM, so dass S' = S
и {(Dom(S), rΞ γ∣)}.

Beweis: Sei S ∈ SEQ und S' ∈ RGF(S). Dann ist S' ∈ AF(S) oder S' ∈ SEF(S) oder S'
∈ SBF(S) oder S' ∈ KEF(S) oder S' ∈ KBF(S) oder S' ∈ BEF(S) oder S' ∈ BBF(S)
oder S' ∈ AEF(S) oder S' ∈ ABF(S) oder S' ∈ NEF(S) oder S' ∈ NBF(S) oder S' ∈
UEF(S) oder S' ∈ UBF(S) oder S' ∈ PEF(S) oder S' ∈ PBF(S) oder S' ∈ IEF(S) oder
S' ∈ IBF(S).

Sei S' ∈ AF(S). Dann gibt es gemaβ Definition 3-1 Γ ∈ GFORM, so dass S' = S и
{(Dom(S), rSei Γ∣)}. Dann ist S'_Dom(_S) = rSei Γ^l und damit gibt es Ξ ∈ PERF und Γ ∈
GFORM, so dass S' = S и {(Dom(S), rΞ Γ∣)}.

Sei S' ∈ SEF(S) oder S' ∈ SBF(S) oder S' ∈ KEF(S) oder S' ∈ KBF(S) oder S' ∈
BEF(S) oder S' ∈ BBF(S) oder S' ∈ AEF(S) oder S' ∈ ABF(S) oder S' ∈ NEF(S) oder
S' ∈ NBF(S) oder S' ∈ UEF(S) oder S' ∈ UBF(S) oder S' ∈ PEF(S) oder S' ∈ PBF(S)
oder S' ∈ IEF(S) oder S' ∈ IBF(S). Dann gibt es gemaβ Definition 3-2 bis Definition
3-17 jeweils Γ ∈ GFORM, so dass S' = S и {(Dom(S), rAlso Γ∣)}. Dann ist S'_Dom(_S) =
rAlso Γ^π und damit gibt es abermals Ξ ∈ PERF und Γ ∈ GFORM, so dass S' = S и
{(Dom(S), rΞ Γ∣)}. ■

Theorem 3-4. RGF-Fortsetzungen von Sequenzen sind genau um eins mdchtiger als die Aus-
gangssequenz

Wenn S ∈ SEQ und S' ∈ RGF(S), dann Dom(S') = Dom(S)+1.

Beweis: Sei S ∈ SEQ und S' ∈ RGF(S). Dann gibt es mit Theorem 3-3 Ξ ∈ PERF und Γ
∈ GFORM, so dass S' = S и {(Dom(S), rΞ Γ∣)} und damit Dom(S') = Dom(S)+1. ■

<<   106   107   108   109   110   111   112   >>

More intriguing information