Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

3.2 Ableitungsbegriff und deduktive Konsequenzschaft 133

Theorem 3-5. Eindeutige RGF-Vorganger

Wenn й ∈ SEQ und й' ∈ RGF($), dann Wt^Dom(W)-1 = й.

Beweis: Ergibt sich unmittelbar aus Theorem 3-3 und Theorem 3-4. ■

Definition 3-19. Die Menge der regelgemaβen Sequenzen (RGS)

RGS = {й | й ∈ SEQ und fur alle j < Dom(⅛) gilt: ⅛[^j+1 ∈ RGF(φ∣j)}.

Theorem 3-6. Eine Sequenz й ist genau dann in RGS, wenn sie leer oder eine regelgemaβe
Fortsetzung von ⅛fDom(⅛)-1 und ⅛fDom(⅛)-1 ein RGS-Element ist

Й ∈ RGS
gdw

Й = 0 oder й ∈ RGF(⅛fDom(⅛)-1) und ⅛[^Dom(⅛)-1 ∈ RGS.

Beweis: (L-R): Sei й ∈ RGS und й ≠ 0. Dann ist zunachst й ∈ SEQ∖{0}. Sodann ist
^Dom($)-1 ∈ SEQ. Auberdem ist ^Dom(⅛)-1 ⊆ й und fur alle j < l)om(fɔ) gilt
(#tDom(#)-1)tj‘ = #tj‘. Wegen й ∈ RGS gilt sodann fur alle j < l)om(fɔ) nach Definition
3-19 йИ+1 ∈ RGF(⅛Γj). Damit gilt zweierlei: Zum einen ist й = #fDom(#)-1+1 ∈
RGF(⅛ΓDom(⅛)-1). Zum anderen gilt dann fur alle j < Dom($)-1 = Dom(⅛ΓDom(⅛)-1)
ebenfalls (#fDom(#)-1)tj+1 = #tj‘+1 ∈ RGF(⅛Γj) = RGF((#tDom(#)-1)tj). Also ist
nach Definition 3-19 ^Dom(⅛)-1 ∈ RGS.

(R-L): Sei й = 0 oder й ∈ RGF(⅛ΓDom(⅛)-1) und ^Dom(⅛)-1 ∈ RGS. Wenn й = 0,
dann ist й ∈ SEQ und es gilt trivial, dass йЦ+1 ∈ RGF(⅛Γj) fur alle j < l)om(fɔ) und
somit gilt й ∈ RGS. Sei nun й ≠ 0 und й ∈ RGF(⅛ΓDom(⅛)-1) und ^Dom(⅛)-1 ∈
RGS. Also gilt nach Definition 3-19 ^Dom(⅛)-1 ∈ SEQ und (#tDom(#)-1)tj‘+1 ∈
RGF((⅛ΓDom(⅛)-1)Γj) fur alle j < Dom(⅛ΓDom(⅛)-1) und daruber hinaus й ∈
RGF(⅛ΓDom(⅛)-1). Nach Theorem 3-1 ist dann й ∈ SEQ und somit, wegen й ≠ 0,
l)om(fɔ) = Dom(⅛)-1+1 = Dom(⅛ΓDom(⅛)-1)+1. Dann gilt fur alle j < Dom($), dass
йИ = ($tDom($)-1)tj‘. Damit gilt йГ;+1 = (£tDom(£)-1)tj+1 ∈ RGF(($tDom($)-1)tj‘)
= RGF(йИ) fur alle j < Dom(#)-1. Wenn aber j = Dom(#)-1, dann ist #tj+1 =
#fDom(#)-1+1 = й ∈ RGF(#tDom(#)-1) = RGF(⅛Γj). Also gilt insgesamt fur alle j <
Dom($), dass #tj+1 ∈ RGF(⅛Γj) und damit й ∈ RGS. ■

Das folgende Theorem wird in den weiteren Kapiteln haufig genutzt, ohne jedes Mal ex-
plizit angezogen zu werden:

<<   107   108   109   110   111   112   113   >>

More intriguing information