Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

90    2 Verfugbarkeit von Aussagen

Theorem 2-60. Sind alle Folgenglieder einer ANS-Umfassenden Abschnittsfolge fur 21. ge-
schlossene Abschnitte, dann ist jeder geschlossene Teilabschnitt von 21. Teilabschnitt eines
Folgengliedes

Wenn ft ∈ SEQ, ^ ∈ ABS(ft) und G ∈ ANSUMF(ft) eine ANS-umfassende Abschnittsfolge
fur 21. in ft ist und {ft} × Ran(G) ⊆ GS, dann gilt fur alle ¢: Wenn £ ⊆ 21. ein geschlossener
Abschnitt in ft ist, dann gibt es ein i ∈ Dom(G), so dass £ ⊆ G(i).

Beweis: Sei ft ∈ SEQ, 2i ∈ ABS(ft) und G ∈ ANSUMF(ft) eine ANS-umfassende Ab-
schnittsfolge fur 2i in ft und {ft} × Ran(G) ⊆ GS. Sei nun £ ⊆ 2i ein geschlossener Ab-
schnitt in ft. Dann ist mit Definition 2-11 bis Definition 2-13 und Theorem 2-42
min(Dom(C)) ∈ ANS(ft) ∩ 2i. Damit gibt es nach Definition 2-9-(iii-c) ein i ∈ Dom(G),
so dass min(Dom(C)) ∈ Dom( G (i)) und nach Voraussetzung ist (ft, G (i)) ∈ GS. Dann
folgt mit Theorem 2-52: £ ⊆ G (i). ■

Nachdem bisher vor allem Theoreme gezeigt wurden, die fur alle geschlossenen Ab-
schnitte gelten, liegt das Interesse spater auch gerade bei den besonderen Eigenschaften
von geschlossenen Abschnitten, insofern diese durch die Anwendung von Subjunktorein-
fuhrung (SE-geschlossene), Negatoreinfuhrung (NE-geschlossene) und Partikularquan-
torbeseitigung (PB-geschlossene) entstehen. Daher werden nun fur diese Arten von ge-
schlossenen Abschnitten eigene Pradikate bereitgestellt, wobei jeder geschlossene
Abschnitt einer dieser Arten angehort (Theorem 2-61).

Definition 2-23. SE-geschlossener Abschnitt

21. ist ein SE-geschlossener Abschnitt in ft
gdw

21. ist ein geschlossener Abschnitt und ein SE-artiger Abschnitt in ft.

Definition 2-24. NE-geschlossener Abschnitt

21.ist ein NE-geschlossener Abschnitt in ft
gdw

21. ist ein geschlossener Abschnitt und ein NE-artiger Abschnitt in ft.

<<   65   66   67   68   69   70   71   >>

More intriguing information