Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

62    2 Verfugbarkeit von Aussagen

max(Dom( G (j))) = max(Dom(∖M(max(Dom( G (j)))+1))). Zu c): Sei nun l ∈
Dom(ANS(⅛)) ∩ Dom(^↑(max(Dom( G (j)))+1)). Dann gibt es ein i ∈ Dom( G), so dass l
∈ Dom(G(i)). Ware nun j+1 ≤ i. Dann ware mit G ∈ ABSF(⅛) und mit Definition 2-7
max(Dom(G(j))) < min(Dom(G(i))) ≤ l ≤ max(Dom(G(i))) und andererseits l ≤
max(Dom(G(j))). Widerspruch! Also ist i < j+1 und damit G(i) = (GΓ(j+1))(i). Also gilt
fur alle l ∈ Dom(ANS(⅛)) ∩ Dom(^Γ(max(Dom(G(j)))+1)), dass es ein i ∈
Dom( G Γ(j+1)) gibt, so dass l ∈ Dom(( G Γ(j+1))(i)). Damit ist dann nach Definition 2-9
G Γ(j+1) insgesamt eine ANS-umfassende Abschnittsfolge fur ^Γ(max(Dom( G (j)))+1). ■

Theorem 2-26. Hinreichende Bedingungen fur die Identitat der Argumente einer ANS-
umfassenden Abschnittsfolge

Wenn A ∈ SEQ und G ∈ ANSUMF(⅛), dann gilt fur alle i, j ∈ Dom(G):

(i) Wenn min(Dom( G (i))) = min(Dom( G (j))), dann i = j,
(ii) Wenn max(Dom( G (i))) = max(Dom( G (j))), dann i = j.

Beweis: Sei ⅛ ∈ SEQ und G ∈ ANSUMF(⅛). Dann folgt mit Definition 2-9 und
Definition 2-10, dass G ∈ ABSF(⅛)∖{0} und damit mit Theorem 2-18 die Behauptung. ■

Theorem 2-27. Verschiedene Glieder einer ANS-umfassenden Abschnittsfolge sind element-
fremd

Wenn A ∈ SEQ und G ∈ ANSUMF(⅛), dann gilt fur alle i, j ∈ Dom(G): Wenn G(i) ≠ G(j),
dann G (i) ∩ G (j) = 0.

Beweis: Sei ⅛ ∈ SEQ und G ∈ ANSUMF(⅛). Dann folgt mit Definition 2-9 und
Definition 2-10, dass G ∈ ABSF(⅛)∖{0} und damit mit Theorem 2-19 die Behauptung. ■

<<   62   63   64   65   66   67   68   >>

More intriguing information