Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 161

Theorem 3-18 £4 = £³~{(0, ^rAlso Γ → (Α^¹max(Dom(VANSc¾¹)))) → K(£))ⁿ } ∈ SEF(£³).
Dann ergibt sich mit Theorem 3-22, dass VAN(£4) ⊆ VAN(£³)\{Γ} ⊆ VAN(£). Also
gilt Γ ∉ VAN(£4) und damit, dass fur alle i ∈ Dom(VANS(£4)): A(£4i) ≠ Γ.

Sei nun £5 = £4~{(0, rSei Α(^¹max(Dom(VANS(⅛¹))))^π), (1, ^rSei Γ^π)}. Dann ist zunachst £5
∈ ΛFW4(0, rSei A(£1max(Dom(VANS(£1))))ⁿ)}) Und £4~{(0, rSei A(£¹max(Dom(VΛNS(,¾¹))))^^l )}
∈ AF(£⁴). Sodann gilt wegen A(£4i) ≠ Γ fur alle i ∈ Dom(VANS(£⁴)) und Γ ≠
A(£ 1max(Dom(VANS(£1)))) mit Theorem 3-15-(iv) fur alle i ∈ Dom(VANS(£5)): A(£5i) = Γ
gdw i = max(Dom(VANS(£5))). Sodann ist mit Theorem 3-15-(viii) VAN(£5) ⊆
VAN(£4) ∪ {Γ, A(£¹max(Dom(VANS(£¹))))} ⊆ VAN(£). Ferner ist mit Theorem 3-15-(vi) {Γ,
^A(£ max(Dom(VANS(£¹)))), ^,"^γ → ^(A(£1max(Dom(VANS(£1)))) → K(£))^ } ⊆ VER(£5) U∏d mit
Theorem 3-15-(iv) ist (Dom(£⁴), rSei A(£¹max(Dom(VANSC¾¹))))^^l ) ∈ ^VANS(£5).

Dann ist £6 = £5^{(0, rAlso A(£1max(Dom(VANS(£¹)))) → K(£f)} ∈ SBF(£5) und mit
Theorem 3-27-(v) gilt VAN(£6) ⊆ VAN(£5) ⊆ VAN(£). Sodann gilt fur alle i ∈
Dom(VANS(£6)): Wenn A(£6i) = Γ, dann i = max(Dom(VANS(£6))). Letzteres ergibt
sich wie folgt:

Gabe es ein i ∈ Dom(VANS(£6)), so dass A(£6i) = Γ und i ≠ max(Dom(VANS(£6))).
Mit Theorem 3-27-(ii) gilt dann i ∈ Dom(VANS(£⁵)). Dann ist i =
max(Dom(VANS(£⁵))) = Dom(£4)+1. Nach Konstruktion von £6 ist jedoch
max(Dom(VANS(£6))) ≤ Dom(£4)+1 = i und also mit i ≠ max(Dom(VANS(£6))) insge-
samt max(Dom(VANS(£6))) < i. Andererseits ist mit i ∈ Dom(VANS(£6)) jedoch i ≤
max(Dom(VANS(£6))). Widerspruch!

Sodann ist rA(£1max(Dom(VANS(£1)))) → K(£)ⁿ = K(£6) ∈ VER(£6). Ware nun
A(£¹max(Dom(VANS(£¹)))) ∉ VER(£6). Dann ware (Dom(£⁴), rSei A(£1max(Dom(VANS(£¹))))ⁿ ) ∉
VANS(£6) und damit (Dom(£⁴), rSei ^-^W))))¹) ∈ VANS(£5)\VANS(£6).
Mit Theorem 2-85 ware dann allerdings VANS(£5)\VANS(£6) =
{(max(Dom(VANS(£⁵))), £max(Dom(VANS(£⁵))))} = {(Dom(£4)+1, rSei Γ^^,)} und also
Dom(£⁴) = Dom(£4)+1. Widerspruch!

Daher ist £⁷ = £6~{(0, rAlso K(££)} ∈ SBF(£6) und mit Theorem 3-27-(v) gilt
VAN(£⁷) ⊆ VAN(£6) ⊆ VAN(£). Ferner gilt mit Theorem 3-27-(ii) fur alle i ∈
Dom(VANS(£⁷)): Wenn A(£⁷i) = Γ, dann i = max(Dom(VANS(£⁷))). Damit ist £⁷ das
gesuchte Element von RGS∖{0}.

Zweiter Fall: Γ ∉ VAN(£³). Sei nun £8 = £³~{(0, rSei A(£1max(Dom(VANS(£¹))))ⁿ )}. Dann
ist zunachst £8 ∈ AF(£³). Sodann ist mit Theorem 3-15-(viii) VAN(£⁸) = VAN(£³) ∪

<<   <   134   135   136   137   138   139   140   >   >>