Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

2.2 Geschlossene Abschnitte

Theorem 2-65. Vorbereitungstheorem fur Theorem 2-67, Theorem 2-68 und Theorem 2-69
Wenn 21. ein Abschnitt in A ist und fur alle geschlossenen Abschnitte ® in Atmax(Dom(2))
gilt, dass min(Dom(2)) < min(Dom(Φ)) oder max(Dom(Φ)) ≤ min(Dom(2)), dann gilt fur
alle i ∈ Dom(2):

(i) 2ti ist kein geschlossener Abschnitt in A und

(ii) Es gibt kein G ∈ ANSUMF(A), so dass {A} × Ran(G) ⊆ GS und 2ti ∈ PERZ((A,
G )).

Beweis: Sei 2 ein Abschnitt in ft und gelte fur alle geschlossenen Abschnitte ® in
Atnuιx(Dom(2)), dass min(Dom(2)) < mιn(Dom('B)) oder max(Dom('B)) ≤
min(Dom(2)). Sei weiter i ∈ Dom(2). Zunachst ist ft ∈ SEQ. Zu (i): Ware nun 2ti ein
geschlossener Abschnitt in ft, dann wurde mit Theorem 2-64-(viii) gelten: 2ti ist ein ge-
schlossener Abschnitt in Ati. Ferner ist i ≤ max(Dom(2)) und somit Ati ⊆
Atmax(Dom(2)) und damit gilt mit Theorem 2-62-(viii): 2ti ist ein geschlossener Ab-
schnitt in Atmax(Dom(2)). Offenbar gilt mit Theorem 2-7 min(Dom(2ti)) =
min(Dom(2l)) und somit mit Theorem 2-31 weder min(Dom(2)) < min(Dom(2ti)) noch
πuιx(Dom(2ti)) ≤ min(Dom(2)), was der Voraussetzung widerspricht.

Zu (ii): Gabe es nun ein G ∈ ANSUMF(A), so dass {A} × Ran(G) ⊆ GS und 2ti ∈
PERZ((A, G)). Sei nun j = min({i | i ∈ Dom(2) und es gibt G ∈ ANSUMF(A), so dass
{A} × Ran( G) ⊆ GS und 2ti ∈ PERZ((A, G))}). Dann gibt es G * ∈ ANSUMF(A), so
dass {A} × Ran(G*) ⊆ GS und 2tj ∈ PERZ((A, G*)). Ware es nun der Fall, dass es ein
k ∈ Dom(2tj) und ein l ∈ Dom(G*) gabe, so dass 2tk ∈ PERZ((A, G*t(l+1))). Dann ist
nach Theorem 2-25 G *t(l+1) eine ANS-umfassende Abschnittsfolge fur
2tmax(Dom( G *(l))+1. Damit ist dann nach Definition 2-10 G *t(l+1) ∈ ANSUMF(A)
und nach Annahme 2tk ∈ PERZ((A, G*t(l+1))) und andererseits k < j, was im Wider-
spruch zur Minimaliat von j steht. Also gibt es kein k ∈ Dom(2tj) und kein l ∈
Dom(G*), so dass 2tk ∈ PERZ((A, G*t(l+1))). Damit ist nach Definition 2-19 2tj ∈
ERZ((A, G*)) und damit mit {A} × Ran(G*) ⊆ GS und Theorem 2-41 (A, 2tj) ∈ GS
und also 2tj im Widerspruch zu (i) ein geschlossener Abschnitt in ft. ■

Die folgenden vier Theoreme schlieβen Kap. 2.2 ab und stellen die Basis fur den Nach-
weis der Korrektheit und der Vollstandigkeit des Redehandlungskalkuls bereit. Mit diesen
Theoremen lasst sich spater zeigen, dass SE resp. NE resp. PB und nur diese SE- resp.

<<   68   69   70   71   72   73   74   >>

More intriguing information