4.1 Vorbereitungen 195
S3
S4
S5
S2 и |
{(Dom(S2), |
Sei A(S max(Dom(VANS(S')))) )} |
S3 и |
{(Dom(S3), |
rAlso α = α-l)} |
S4 и |
{(Dom(S4), |
rAlso K(S'Γ)}. |
Mit Theorem 1-12 ist zunachst K(S3) ∉ FSATZ und daher S3 ∉ SEF(S2) и NEF(S2) и
PBF(S2). Mit Theorem 1-10 und Theorem 1-11 ist auβerdem K(S4) keine Negation oder
Subjunktion und daher S4 ∉ SEF(S3) и NEF(S3). Ware A(S'max(Dom(VANS(S')))) = ⅛ = ɑ^ ,
dann ware α ∈ TT(A(S'max(Dom(VANS(S'))))) ⊆ TT(K(S1)) ⊆ TTFM(VER(S2)) ⊆
TTSEQ(S2), was der Annahme uber α widerspricht. Also S4 ∉ SEF(S3) и NEF(S3) и
PBF(S3). Ware S5 ∈ SEF(S4) и NEF(S4) и PBF(S4), dann ware α ∈
TT(A(‰Dom(VANS(⅞'))))) и TT(K(S')) ⊆ TT(K(S1)) ⊆ TTSEQ(S2), was wieder der
Annahme uber α widerspricht. Also S5 ∉ SEF(S4) и NEF(S4) и PBF(S4).
Hingegen ist S3 ∈ AF(S2) und damit S3 ∈ RGS und mit Theorem 3-15-(vi) K(S),
K(S1), A(S'max(Dom(VANS(S')))) ∈ VER(S2) и {A(S'max(Dom(VANS(S'))))} = VER(S3) und mit
Theorem 3-15-(viii) VANAA = VAV(S) и {A(S'max(Dom(VANS(S'))))} ⊆ VAN(S) и
VAN(S'). Sodann ist S4 ∈ IEF(S3) und damit S4 ∈ RGS und mit Theorem 3-25
VERS(S4) = VERS(S3) и {(Dom(S3), rAlso α = απ)}. Damit gilt VAN(S4) = VAN(S3)
⊆ VAN(S) и VAN(S') und K(S), K(S1), A(S'max(Dom(VANS(S')))) ∈ VIA(AA) ⊆ VER(S4).
Wegen K(S1) = ΓA(S'max(Dom(VANS(S'))) → K(^')π ist ^5 ∈ SBF(64) ⊆ RGS∖{0}. Mit
Theorem 3-25 gilt sodann VERS(^5) = VERS(^4) и {(Dom(S4), rAlso K(⅛')π)}. Damit
gilt VAN(^5) = VAN(^4) ⊆ VAN(S) и VAN(S') und K(S) ∈ VER(S4) ⊆ VER(S5)
und mit Theorem 2-82 K(S') = K(S5) ∈ VER(S5) und S5 ∈ RGS∖{0}. S5 ist damit das
gesuchte RGS-Element. ■