Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

182  4 Theoreme zur deduktiven Konsequenzschaft

{(l+1 | l ∈ Dom(VERS(⅛))} и {0}. Sei nun 0 < Dom(⅛). Dann ist Й ∈ RGS∖{0}. Dann
ist mit Theorem 3-6 Й ∈ RGF(⅛ΓDom(⅛)-1). Dann ist nach I.V.:

c) Й* = {(0, ^rAlso β = β^-l)}^[β, α, ⅛[^Dom(⅛)-1] ∈ RGS und Dom(VERS(⅛*)) = {(l+1 |
l ∈ Dom(VERS(⅛fDom(⅛)-1))} и {0}.

Sodann ergibt sich mit Й ∈ RGF(^ΓDom(⅛)-1) mit Definition 3-18, dass Й ∈
AF(⅛ΓDom(⅛)-1) oder Й ∈ SEF(⅛fDom(⅛)-1) oder Й ∈ SBF(⅛tDom(⅛)-1) oder Й ∈
KEF(⅛ΓDom(⅛)-1) oder Й ∈ KBF(#fDom(#)-1) oder Й ∈ BEF($tDom(#)-1) oder Й ∈
BBF(⅛ΓDom(⅛)-1) oder Й ∈ AEF(^Dom^)-1) oder Й ∈ ABF(^Dom^)-1) oder Й ∈
NEF(^Dom^)-1) oder Й ∈ NBF(^Dom^)-1) oder Й ∈ UEF(^Dom^)-1) oder Й ∈
UBF(^Dom^)-1) oder Й ∈ PEF(^Dom^)-1) oder Й ∈ PBF(^Dom^)-1) oder Й ∈
IEF(⅛ΓDom(⅛)-1) oder Й ∈ JBF(^Domφ)-1).

Da sich Operatoren durch die Substitution nicht verandern, gilt nun zunachst:

d) Fur alle i ∈ Dom($)-1: А(Й*_г+і) = [β, α, A(⅛)] und й*_і+1 = rΞ [β, α, A(⅛)Γ, wobei
Йг = rΞ A(⅛)^^l fur ein Ξ ∈ PERF.

Sodann gilt mit β ∈ PAR\TTSEQ($) und α ∈ KONST:

e) Fur alle i ∈ Dom(£): β ∉ TT(A(⅛)) und α ∉ TT([β, α, A(&)]),

da sonst im Gegensatz zur Voraussetzung β ∈ TTSEQ(F)) oder aber im Gegensatz zu
Postulat 1-1 α = β. Mit a) gilt:

f) Й⁺ = Й* и {(Domφ*), ^Domm)} = Й* и {(Dom(£), [β, α, ‰m(s)-1])}.

Nun wird gezeigt, dass sich fur die einzelnen Falle AF ... IBF jeweils ergibt, dass Й⁺ ∈
RGS und b), womit Й⁺ dann jeweils das gesuchte RGS-Element ist. Um Sonderbetrach-
tungen bei SBF, KEF, KBF, BEF, BBF, AEF, ABF, NBF, UEF, UBF, PEF, IEF und IBF
zu vereinfachen wird nun noch vorbereitend gezeigt:

g) Wenn Й⁺ ∈ SEF($*) и NEF($*) и PBF($*), dann Й ∈ SEF($|Dom($)-1) и
NEF(#rDom(£-1) и PBF(^Domφ-1).

Vorbereitungsteil: Sei Й⁺ ∈ SEF(#*). Dann gibt es nach Definition 3-2 und mit c) und f)
ein i ∈ Dom(VANS(⅛*)), so dass es kein l mit i < l ≤ Dom($)-1 gibt, so dass l ∈
Dom(VANS(⅛*)), und Й⁺ = Й* и {(Dom(⅛), rAlso A(#*i) → К(й*)^п)}. Nun ist Й*₀ =
rAlso β = β^^l ∉ VANS^*). Also ist i ≠ 0 und mit d) A^*_i) = [β, α, A( Йі)| und К(й*)
= [β, α, A‰m(⅛2)]. Also Й⁺ = Й* и {(Dom^), rAlso [β, α, A‰)] → [β, α,

<<   155   156   157   158   159   160   161   >>

More intriguing information