Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

50    2 Verfugbarkeit von Aussagen

Theorem 2-3. Abschnitte in Beschrankungen¹¹

Wenn ft ∈ SEQ, dann: 21. ist ein Abschnitt in ft gdw ^ ist ein Abschnitt in
fti max(Dom(^))+1.

Beweis: Sei ft ∈ SEQ. (L-R): Sei 2i ein Abschnitt in ft. Dann ergibt sich: 2i ≠ 0, 2i ⊆ ft
und damit: ftfmax(Dom(W))+1 ∈ SEQ. Sodann ist 2i ⊆ ftfmax(Dom(W))+1 ⊆ ft und
somit

21. = {(i, ft_i) | min(Dom(^)) ≤ i ≤ max(Dom(2i))}

{(i, (ftimax(Dom(2i))+i),) | min(Dom(^)) ≤ i ≤ max(Dom(2i))}

und 2i somit insgesamt ein Abschnitt in ftΓmax(Dom(W))+1. (R-L): Ist umgekehrt 2i ein
Abschnitt in ftfmax(Dom(W))+1, dann ist ftΓmax(Dom(^))+1 ∈ SEQ und nach der Ein-
gangsvoraussetzung ft eine Sequenz und mit ftΓmax(Dom(^))+1 ⊆ ft und Theorem 2-2
2i auch ein Abschnitt in ft. ■

Bemerkung 2-2. F-Abschnitte in Beschrankungen

Wenn F eines der im Folgenden definierten Abschnittspradikate ist, dann gilt: Wenn ft ∈
SEQ, dann: 21. ist ein F -Abschnitt in ft gdw 21. ist ein F-Abschnitt in ftfmax(Dom(^))+1.

Erlauterung: Alle folgenden Definitionen von Abschnittspradikaten haben die Form wie
in Bemerkung 2-1 angegeben, wobei fur H jeweils gilt: Wenn ft ∈ SEQ, 2i ∈ ABS(ft)
(bzw., aquivalent dazu: 2i ist ein Abschnitt in ft) und H(2L ft), dann H(2f
ftΓmax(Dom(W))+1). Der Grund ist jeweils, dass in den Definientia nur Bezug auf Ver-
haltnisse in ftΓmax(Dom(^))+1 genommen wird. Damit ergibt sich dann mit Theorem 2-3
und der entsprechenden Definition jeweils: Wenn ft eine Sequenz ist und 2i ein F -
Abschnitt in ft ist, dann ist 2i ein F -Abschnitt in ftΓmax(Dom(^))+1. Fur die Gegenrich-
tung siehe Bemerkung 2-1. ■

'..!..' ist der Beschrankungsoperator. Dabei gelte: RіX = {(a, b) | (a, b) ∈ R und a ∈ X}.

<<   50   51   52   53   54   55   56   >>

More intriguing information