Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 177

Erster Fall: Sei β⁺ = β. Dann ist A(‰) = [β*, β, [β⁺, ζ, Δ]] = [β*, β, [β, ζ, Δ]] und mit
β⁺ ∉ TT(Δ) auch β ∉ TT(Δ) und somit mit Theorem 1-24-(ii) A(⅛_i+1) = [β*, β, [β, ζ, Δ]]
= [β*, ζ, Δ]. Mit β ∉ TT(Δ) ist sodann [β*, β, Δ] = Δ und damit A(⅛*i) = ^rVζ[β*, β, Δ]^π =
^rVζΔ^π. Sodann gilt mit β = β⁺ und β* ∉ TTSEQ(^): β, β* ∉ TTFM({Δ, A(‰m(⅛-2)})
und damit auch β* ∉ TTFM({Δ, [β*, β, A(^D_om(⅛)_-2)]}). Gabe es nun ein j ≤ i, so dass β*
∈ TT(⅛*j). Dann ist mit b) β* ∈ TT(⅛*_j) = [β*, β, ⅛_j∙]. Sodann ist mit β* ∉ TTSEQ(⅛)
auch β* ∉ TT(.ħ ). Damit gilt mit β* ∈ TT(⅛*j) dann aber β ∈ TT(.ħ ) und andererseits
nach Voraussetzung β = β⁺ ∉ TT(.ħ ). Widerspruch! Also gilt, dass es kein j ≤ i gibt, so
dass β* ∈ TT(⅛*j). Damit ist dann insgesamt .ħ' ∈ PBF(⅛*).

Zweiter Fall: Sei nun β⁺ ≠ β. Dann lassen sich mit β⁺ ≠ β* und β⁺ = β* zwei Unterfalle
unterscheiden. Erster Unterfall: Sei β⁺ ≠ β*. Dann ist mit Theorem 1-25-(ii) und β⁺ ≠ β:
A(S*_f+ι) = [β*, β, [β⁺, ζ, Δ]] = [β⁺, ζ, [β*, β, Δ]]. Sodann ist A(S*_i) = ^rVζ[β*, β, Δ]^η. Wa-
re nun β⁺ ∈ TTFM({[β*, β, Δ], [β*, β, A(‰om(⅛)-2)]}) oder gabe es ein j ≤ i, so dass β⁺ ∈
TT(⅛*,∙). Dann ware wegen β⁺ ≠ β* mit b) auch β⁺ ∈ TTFM({Δ, A(^D_om(⅛)_-2)}) oder es
gabe j ≤ i, so dass β⁺ ∈ TT(.ħ ). Widerspruch! Also ist β⁺ ∉ TTFM({[β*, β, Δ], [β*, β,
A(‰_om(⅛)_-2)]}) und es gibt kein j ≤ i, so dass β⁺ ∈ TT(⅛*j) und damit wiederum insge-
samt .ħ' ∈ PBF(⅛*).

Zweiter Unterfall: Sei nun β⁺ = β*. Dann ist ζ ∉ FV(Δ), da sonst β* ∈ TT([β⁺, ζ, Δ]) ⊆
TTSEQ(^). Damit ist dann [β⁺, ζ, Δ] = Δ und damit A(^*i+1) = [β*, β, [β⁺, ζ, Δ]] = [β*, β,
Δ] und sodann ist A(⅛*i) = ^rVζ[β*, β, Δ]^^l. Sei nun в§ ∈ PAR∖TTSEQ(⅛*). Dann ist mit ζ
∉ FV(Δ) auch ζ ∉ FV([β*, β, Δ]) und damit A(⅛*i₊ι) = [β*, β, Δ] = [β^δ, ζ, [β*, β, Δ]] und
es gilt: в§ ∉ TTFM({[β*, β, Δ], [β*, β, A(‰m(⅛)-2)]}) und es gibt kein j ≤ i, so dass в§ ∈
TT(⅛*,∙). Damit ist dann wieder insgesamt auch .ħ' ∈ PBF(⅛*). Damit gilt in beiden
Unterfallen und somit insgesamt in beiden Fallen, dass .ħ' ∈ PBF(⅛*) und damit .ħ' ∈
RGS.

Sodann ergibt sich mit Theorem 3-21-(iii), dass VERS(⅛) = VERS(⅛ΓDom(⅛)-1)∖{(j,
⅛j) | i+1 ≤ j < Dom(⅛)-1} ∪ {(Dom(⅛)-1, ^rAlso A(^D_om(⅛)_-2)^π)} und dass VERS(Ef) =
VERS(⅛*)X{(j,  ⅛⁺j)  |  i+1  ≤ j < Dom(⅛)-1}  ∪  {(Dom(⅛)-1,  rAlso  [β*, β,

A(^D_om(⅛)_-2)]^π)}. Mit Dom(VERS(E)*)) = Dom( VERS(Vf Dom(E)-1)) ergibt sich dann
wieder Dom(VERS( E')) = Dom(VERS( E)).

Ausschlussannahme: Fur die verbleibenden Schritte sei ⅛ ∉ SEFC⅛fDom(⅛)-1) ∪
NEF(⅛ΓDom(⅛)-1) ∪ PBF(⅛ΓDom(⅛)-1). Mit e) ist dann V ∉ SEF(⅛*) ∪ NEF(⅛*) ∪
PBF(⅛*). Damit ergibt sich fur die folgenden Falle dann mit Theorem 3-25 jeweils, dass

<<   150   151   152   153   154   155   156   >>

More intriguing information