Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 167

gdw

k ∈ Dom(VERS(⅛*)) und k < Dom(⅛)+1+i oder k = Dom(⅛)+1+Dom(⅛')-1
gdw

k ∈ Dom(VERS(⅛)) ∪ {Dom(⅛)} oder k ∈ {(Dom(⅛)+1+l | l ∈
Dom(VERS(⅛'[^Dom(⅛')-1))} und k < Dom(⅛)+1+i oder k = Dom(^)+1+Dom(⅛')-1
gdw

k < Dom(⅛)+1 und k ∈ Dom(VERS(⅛)) ∪ {Dom(⅛)} oder k ≥ Dom(⅛)+1 und
k-Dom(⅛)+1 ∈ Dom(VERS(⅛'[^Dom(⅛')-1)) und k-Dom(⅛)+1 < i oder k-Dom(⅛)+1 =
Dom(⅛')-1
gdw

k < Dom(⅛)+1 und k ∈ Dom(VERS(⅛)) ∪ {Dom(⅛)} oder k ≥ Dom(⅛)+1 und
k-Dom(⅛)+1 ∈ Dom(VERS(⅛'∣Dom(⅛')-1))∖{j' | i ≤ j < Dom(⅛')-1} oder k-Dom(⅛)+1 =
Dom(⅛')-1
gdw

k < Dom(⅛)+1 und k ∈ Dom(VERS(⅛)) ∪ {Dom(⅛)} oder k ≥ Dom(⅛)+1 und k-
Dom(^)+1 ∈ Dom(VERS(⅛'))

und somit, dass Dom(VERS(⅛⁺)) = Dom(VERS(⅛)) и {Dom(⅛)} и {(Dom(⅛)+1+l | l ∈
Dom(VERS(⅛'))} und damit (v) gilt. Fur den Fall, dass ⅛' ∈ NEF(⅛'ΓDom(⅛')-1), zeigt
man analog, dass dann auch .A ∈ NEF(⅛*) ⊂ RGS∖{0} und v) gilt.

(PBF): Sei nun ⅛' ∈ PBF(⅛'ΓDom(⅛')-1). Dann gilt nach Definition 3-15, dass es β ∈
PAR, ξ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξ}, und i ∈ Dom(VERS(⅛'ΓDom(⅛')-1))
gibt, so dass mit iv') ^rVξΔ^^, = A(⅛'_i) = A(^*Dom(⅛)+1+i) und [β, ξ, Δ] = A(⅛'_i+1) =
A(^*_Dom(^)+2+_i), wobei i ∈ Dom(VANS(⅛'ΓDom(⅛')-1)) und K(⅛'ΓDom(⅛')-1) =
A⁽A Dom(⅛')-2) A⁽A Dom(⅛)+1+Dom(⅛')-2) = K(⅛*) und ⅛' = ⅛'ΓDom(⅛')-1 и {(Dom(⅛')-1,
^rAlso K(⅛'ΓDom(⅛')-1)} und β ∉ TTFM({Δ, K(⅛'ΓDom(⅛')-1)}) und es gibt kein j ≤ i,
so dass β ∈ TT(⅛'j), und es gibt kein l mit i+1 < l ≤ Dom(⅛')-2, so dass l ∈
Dom(VANS(⅛TDom(⅛')-1).

Dann gilt mit iv') und v'): Dom(⅛)+1+i ∈ Dom(VERS(⅛*)) und Dom(⅛)+2+i ∈
Dom(VANS(⅛*)) und es gibt kein l mit Dom(⅛)+2+i < l ≤ Dom(⅛)+1+Dom(⅛')-2, so
dass l ∈ Dom(VANS(⅛*)). Sodann gilt mit vi'), dass .ħ' = ⅛* и
{(Dom(⅛)+1+Dom(⅛')-1, rAlso K(⅛'ΓDom(⅛')-1)} = b* и {(Dom(⅛)+1+Dom(⅛')-1,
rAlso K(⅛*)^π}.

Sodann ist ξ ∈ FV(Δ) oder ξ ∉ FV(Δ). Sei nun ξ ∈ FV(Δ). Dann ist β ∈ TT([β, ξ, Δ])
⊂ TTSEQ(⅛'). Da nun nach Voraussetzung PAR ∩ TTSEQ(⅛) ∩ TTSEQ(⅛') = 0 ist
damit β ∉ TTSEQ(⅛). Damit ergibt sich mit i') bis iv') daraus, dass β ∉ TTFM({Δ,
K(⅛'ΓDom(⅛')-1)}) und es kein j ≤ i gibt, so dass β ∈ TT(⅛'_j), dass auch β ∉ TTFM({Δ,

<<   140   141   142   143   144   145   146   >>

More intriguing information