Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

48    2 Verfugbarkeit von Aussagen

Definition 2-1. Abschnitt in einer Sequenz (Metavariablen: ЭД, ®, ¢, ЭД', ®', ¢', ЭД*, ®*, £*,
■■■)

ЭД ist ein Abschnitt in ʃɔ
gdw

ʃɔ ∈ SEQ, ЭД ≠ 0, ЭД ⊆ ⅛ und ЭД = {(i, ⅛) | min(Dom(^)) ≤ i ≤ max(Dom(^))}.

Definition 2-2. Zuordnung der Menge der Abschnitte von ^ (ABS)

ABS = {(⅛, X) | ⅛ ∈ SEQ und X = {ЭД | ЭД ist ein Abschnitt in ⅛}}.

Definition 2-3, Definition 2-4 und Definition 2-5 dienen vor allem der Verflussigung des
Ausdrucks.

Definition 2-3. Abschnitt

ЭД ist ein Abschnitt gdw es gibt ein ⅛, so dass ЭД ein Abschnitt in ʃɔ ist.

Definition 2-4. Teilabschnitt

ЭД ist ein Teilabschnitt von ЭД' gdw ЭД, ЭД' sind Abschnitte und ЭД ⊆ ЭД'.

Definition 2-5. Echter Teilabschnitt

ЭД ist ein echter Teilabschnitt von ЭД' gdw ЭД ist Teilabschnitt von ЭД' und ЭД ≠ ЭД'.

Theorem 2-1. Eine Sequenz ^ ist genau dann nicht-leer, wenn ABS⅛) nicht-leer ist

Wenn ʃɔ ∈ SEQ, dann: ʃɔ ≠ 0 gdw ABS(⅛) ≠ 0.

Beweis: Sei A ∈ SEQ. Sei zunachst A ≠ 0. Dann ist A ein Abschnitt in A und somit A ∈
ABS(⅛). Sei nun ABS(⅛) ≠ 0. Dann gibt es ein ЭД, so dass ЭД ein Abschnitt in A ist. Dann
ist ЭД ≠ 0 und ЭД ⊆ A und damit A ≠ 0. ■

Theorem 2-2. Das Abschnittspradikat ist bezuglich Teilmengenschaft zwischen Sequenzen
monoton

Wenn ⅛ ⅛' ∈ SEQ, ʃɔ ⊆ ⅛' und ЭД ein Abschnitt in ʃɔ ist, dann ist ЭД ein Abschnitt in ⅛'.

Beweis: Seien Д ⅛^, ∈ SEQ, A ⊆ ⅛^, und ЭД ein Abschnitt in ⅛. Dann ist ЭД ≠ 0 und ЭД ⊆
A ⊆ ⅛^,. Ferner ist A = ⅛'ΓDom(⅛). Damit ist

ЭД = {(i, ⅛_i) | min(Dom(2l.)) ≤ i ≤ max(Dom(2t))[

<<   48   49   50   51   52   53   54   >>

More intriguing information