Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

92 2 Verfugbarkeit von Aussagen

Theorem 2-63. Geschlossene Abschnitte bleiben in Verkettungen in der Anfangssequenz ge-
schlossen

Wenn й', й ∈ SEQ, dann:

(i) Wenn ЭД ein SE-geschlossener Abschnitt in й ist, dann ist ЭД ein SE-geschlossener
Abschnitt in йГй,

(ii) Wenn ЭД ein NE-geschlossener Abschnitt in й ist, dann ist ЭД ein NE-geschlossener
Abschnitt in й^й',

(iii) Wenn ЭД ein PB-geschlossener Abschnitt in й ist, dann ist ЭД ein PB-geschlossener
Abschnitt in й^й',

(iv) Wenn ЭД ein geschlossener Abschnitt in й ist, dann ist ЭД ein geschlossener Abschnitt
in й~й'.

Beweis: Ergibt sich mit й ⊆ й~й' und Theorem 2-62-(i), -(ii), -(iii) und -(viii). ■

Theorem 2-64. (F-)geschlossene Abschnitte in Beschrankungen

Wenn й eine Sequenz ist, dann:

(i) ЭД ist ein SE-geschlossener Abschnitt in й gdw ЭД ist ein SE-geschlossener Abschnitt
in йї max(Dom^))+1,

(ii) ЭД ist ein NE-geschlossener Abschnitt in й gdw ЭД ist ein NE-geschlossener Abschnitt
in йї max(Dom^))+1,

(iii) ЭД ist ein PB-geschlossener Abschnitt in й gdw ЭД ist ein PB-geschlossener Abschnitt
in йї max(Dom^))+1,

(iv) ЭД ist ein minimaler SE-geschlossener Abschnitt in й gdw ЭД ist ein minimaler SE-
geschlossener Abschnitt in #|max(Dom^))+1,

(v) ЭД ist ein minimaler NE-geschlossener Abschnitt in й gdw ЭД ist ein minimaler NE-
geschlossener Abschnitt in #|max(Dom^))+1,

(vi) ЭД ist ein minimaler PB-geschlossener Abschnitt in й gdw ЭД ist ein minimaler PB-
geschlossener Abschnitt in #|max(Dom^))+1,

(vii) ЭД ist ein minimaler geschlossener Abschnitt in й gdw ЭД ist ein minimaler geschlosse-
ner Abschnitt in #|max(Dom^))+1, und

(viii) ЭД ist ein geschlossener Abschnitt in й gdw ЭД ist ein geschlossener Abschnitt in
йї max(Dom^))+1.

Beweis: Siehe Bemerkung 2-2. ■