Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 195

Mit Theorem 1-12 ist zunachst K(S³) ∉ FSATZ und daher S³ ∉ SEF(S²) и NEF(S²) и
PBF(S²). Mit Theorem 1-10 und Theorem 1-11 ist auβerdem K(S⁴) keine Negation oder
Subjunktion und daher S⁴ ∉ SEF(S³) и NEF(S³). Ware A(S'max(Dom(VANS(S')))) = ⅛ = ɑ^ ,
dann ware α ∈ TT(A(S'max(Dom(VANS(S'))))) ⊆ TT(K(S¹)) ⊆ TTFM(VER(S²)) ⊆
TTSEQ(S²), was der Annahme uber α widerspricht. Also S⁴ ∉ SEF(S³) и NEF(S³) и
PBF(S³). Ware S⁵ ∈ SEF(S⁴) и NEF(S⁴) и PBF(S⁴), dann ware α ∈
TT(A(‰Dom(VANS(⅞'))))) и TT(K(S')) ⊆ TT(K(S¹)) ⊆ TTSEQ(S²), was wieder der
Annahme uber α widerspricht. Also S⁵ ∉ SEF(S⁴) и NEF(S⁴) и PBF(S⁴).

Hingegen ist S³ ∈ AF(S²) und damit S³ ∈ RGS und mit Theorem 3-15-(vi) K(S),
K(S¹), 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 S⁴ ∈ IEF(S³) und damit S⁴ ∈ RGS und mit Theorem 3-25
VERS(S⁴) = VERS(S³) и {(Dom(S³), rAlso α = α^π)}. Damit gilt VAN(S⁴) = VAN(S³)
⊆ VAN(S) и VAN(S') und K(S), K(S1), A(S'max(Dom(VANS(S')))) ∈ VIA(AA) ⊆ VER(S⁴).
Wegen K(S¹) = ΓA(S'max(Dom(VANS(S'))) → K(^')^π ist ^⁵ ∈ SBF(6⁴) ⊆ RGS∖{0}. Mit
Theorem 3-25 gilt sodann VERS(^⁵) = VERS(^⁴) и {(Dom(S⁴), rAlso K(⅛')^π)}. Damit
gilt VAN(^⁵) = VAN(^⁴) ⊆ VAN(S) и VAN(S') und K(S) ∈ VER(S⁴) ⊆ VER(S⁵)
und mit Theorem 2-82 K(S') = K(S⁵) ∈ VER(S⁵) und S⁵ ∈ RGS∖{0}. S⁵ ist damit das
gesuchte RGS-Element. ■

<<   168   169   170   171   172   173   174   >>

More intriguing information