Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

2.1 Abschnitte und Abschnittsfolgen 49

{(i, ft'_i) | min(Dom(2l)) ≤ i ≤ max(Dom(2l))}

und somit 2i insgesamt ein Abschnitt in ft'. ■

Bemerkung 2-1. Alle der im Folgenden definierten Abschnittspradikate sind bezuglich Teil-
mengenschaft zwischen Sequenzen monoton. Dies wird in der weiteren Darstellung benutzt,
aber nicht extra gezeigt

Wenn F eines der im Folgenden definierten Abschnittspradikate ist, dann gilt: Wenn ft, ft' ∈
SEQ, ft ⊆ ft' und 21. ein F-Abschnitt in ft ist, dann ist 21. ein F -Abschnitt in ft'.

Erlauterung: Alle folgenden Definitionen von Abschnittspradikaten haben eine der bei-
den folgenden Formen:

21. ist ein F-Abschnitt in ft gdw ft ∈ SEQ, ^ ∈ ABS(ft) und H(21., ft).

oder

21. ist ein F-Abschnitt in ft gdw ^ ist ein Abschnitt in ft und H (21., ft).

Dabei ist H der variable Teil im Definiens, der die einzelnen Definitionen voneinander
unterscheidet. Fur H gilt jeweils: Wenn ft, ft' ∈ SEQ, ft ⊆ ft' und 2i ∈ ABS(ft) (bzw.,
Equivalent dazu: 2i ist ein Abschnitt in ft) und H(2L ft), dann H(2i, ft'). Damit ergibt sich
mit Theorem 2-2 und der entsprechenden Definition dann jeweils: Wenn ft, ft' Sequenzen
sind, ft ⊆ ft' und 2i ein F -Abschnitt in ft ist, dann ist 2i ein F -Abschnitt in ft'.

Daraus ergibt sich auch: Wenn ft, ft' Sequenzen sind, und 2i ein F -Abschnitt in ft ist,
dann ist 2i auch ein F-Abschnitt in ft"~"ft'.^l° Zu beachten ist allerdings, dass fur viele der
im Folgenden definierten Abschnittspradikate nicht gilt: Wenn ft, ft' Sequenzen sind, und
ft ein F-Abschnitt in ft ist, dann ist ft auch ein F-Abschnitt in ft'~ft. ■

'ʃ..' ist der Operator der Folgenverkettung. Die Klammern sind weggelassen und es ist Linksklamme-
rung unterstellt. Also: Ai.ftaft'aft ....~α_n-f^, = ^r(...((⅛''(⅛)''(⅛)'' ... )^a,_λ-ι)^^,.

<<   49   50   51   52   53   54   55   >>

More intriguing information