Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

3.3 VERS, VANS, VER und VAN in Ableitungen und bei einzelnen Ubergangen 147

A(A‘Dom(_A)) = Γ. Damit gilt mit Theorem 2-93, dass ® ein PB-geschlossener und damit
auch ein geschlossener Abschnitt in A' ist.

Da sodann max(Dom(Φ)) = Dom(A) = Dom(A')-1, ergibt sich mit Theorem 2-86,
dass   VANS(A'TDom(A')-1)∖VANS(A')    =    {(min(Dom(Φ)), ^A min(Dom(Φ)))}

{(max(Dom(VANS(A'TDom(A')-1))), ^A max(Dom(VANS(A'TDom(A')-1))))}. ^{Da A A} fDo^m(^ ^)-1
folgt    daraus: VANS(A)∖VANS(A')    =    {(min(Dom(Φ)), ^A min(Dom(!B)))}

{(max(Dom(VANS(A))), A'm_ax(i>o,,,,∙vans(a)))) }. Damit ist i = min(Dom(Φ)) =
max(Dom(VANS(A))) und es gilt: ® = {(j, A'j) | max(Dom(VANS(A))) ≤ j ≤ Dom(A)}.
Damit gilt dann (i). Auβerdem gilt dann K(A) = A(A'D_om(A)-ι) = Γ = K(A') und somit gilt
(x). Sodann ergibt sich mit VANS(A)∖VANS(A') ≠ 0 und Theorem 2-73 auch
VERS(A)∖VERS(A') ≠ 0. Damit und mit A = ATDom(A)-I und ® = {(j, A'j) |
max(Dom(VANS(A))) ≤ j ≤ Dom(A)} ergeben sich dann mit Theorem 2-83-(iv) bis -(xi)
und mit der eindeutigen Bestimmtheit geschlossener Abschnitte mit demselben Endglied
(Theorem 2-53) die restlichen Klauseln ((ii) bis (ix)). ■

Theorem 3-22. Ist die zuletzt angenommene Aussage nur einmal als Annahme verfugbar,
dann wird sie bei SE, NE undPB eliminiert

Wenn A ∈ SEQ, Δ ∈ GFORM und fur alle i ∈ Dom(VANS(A)) gilt: Wenn A(Ai) = Δ, dann i
= max(Dom(VANS(A))), dann gilt fur alle A' ∈ SEF(A) ∪ NEF(A) ∪ PBF(A): VAN(A) ⊆
VAN(A)∖{Δ}.

Beweis: Sei A ∈ SEQ, Δ ∈ GFORM und gelte fur alle i ∈ Dom(VANS(A)): Wenn A(Ai)
= Δ, dann i = max(Dom(VANS(A))). Sei nun A' ∈ SEF(A) ∪ NEF(A) ∪ PBF(A). Dann
gilt mit Theorem 3-19-(iv), -(v), Theorem 3-20-(iv), -(v) und Theorem 3-21-(iv), -(v),
dass VANS(A)∖VANS(A') = {(max(Dom(V ANS(A))), A'max(Dom(VANS(A))))} und
VANS(A') ⊆ VANS(A). Mit Theorem 2-75 gilt VAN(A') ⊆ VAN(A).

Damit gilt: Δ ∉ VAN(A'). Ware namlich Δ ∈ VAN(A'). Dann gabe es nach Definition
2-31 i ∈ Dom(VANS(A')), so dass Δ = A(A'i). Dann gilt mit VANS(A') ⊆ VANS(A),
dass i ∈ Dom(VANS(A)) und es ist Δ = A(Ai). Da nun nach Annahme fur alle i ∈
Dom(VANS(A)) gilt: Wenn A(Ai) = Δ, dann i = max(Dom(V ANS(A))) ware damit
max(Dom(VANS(A))) = i ∈ Dom(VANS(A')). Mit VANS(A)∖VANS(A') =
{(max(Dom(VANS(A))), A'max(Dom(VANS(A))))} gilt nun jedoch max(Dom(VANS(A))) ∉
Dom(VANS(A')). Widerspruch! Also ist Δ ∉ VAN(A') und damit VAN(A') ⊆
VAN(A)∖{Δ}. ■

<<   121   122   123   124   125   126   127   >>

More intriguing information