Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

242   6 Korrektheit und Vollstandigkeit des Redehandlungskalkuls

{A(ftmax(Dom(VANS(ft∣^Dom(ft)-1))))} = VAN(ft) U {[β, ξ, Δ]} U∏d S0mit VAN(ft) U {[β, ξ, Δ]}
к K(ft). Soda∏∏ gilt VAN(ftΓmax(Dom(VANS(ftΓDom(ft)-1)))) к ^rVξΔ^^l.

Nu∏ gilt, dass VAN(ftΓmax(Dom(VANS(ftΓDom(ft)-1)))) ⊂ VAN(ft). Nach Theorem
3-21-(iii) ist ∏amlich zu∏achst (max(Dom(VANS(ftΓDom(ft)-1)))-1, ^rVξΔ^^l) ∈ VERS(ft),
da       (max(Dom(VANS(⅛ΓDom(⅛)-1)))-1,       ftmax(Dom(VANS(ft∣Dom(ft)-1)))-1)       ∈

VERS(ftΓDom(ft)-1)       u∏d       max(Dom(VANS(ftΓDom(ft)-1)))-1       <

max(Dom(VANS(ftΓDom(ft)-1))).     Also ist     ^rVξΔ^^l     i∏ ft bei

max(Dom(VANS(ftΓDom(ft)-1)))-1 verfugbar. Mit Theorem 3-29-(iv) folgt, dass
VAN(ftΓmax(Dom(VANS(ftΓDom(ft)-1)))) ⊂ VAN(ft). Damit gilt mit Theorem 5-13,
dass VAN(ft) к ^rVξΔ^^l.

Es gilt bereits, dass   β   ∉ TTFM({Δ, K(ft)}).   Da es   kei∏ j  ≤

max(Dom(VANS(ftΓDom(ft )-1)))-1 gibt, so dass β ∈ TT(ftj), gibt es soda∏∏ kei∏ j ∈
Dom(VANS(ftΓDom(ft)-1)),  so  dass β ∈ TT(ftj) =  TT(A(ft_j))  u∏d j  ≠

max(Dom(VANS(ftΓDom(ft)-1))). Damit gilt mit Theorem 3-21-(iv) u∏d -(v), dass es
kei∏ j ∈ Dom(VANS(ft)) gibt, so dass β ∈ TT(A(ft_j)). Also ist β ∉ TTFM(VAN(ft)) u∏d
damit i∏sgesamt β ∉ TTFM(VAN(ft) и {Δ, K(ft)}) u∏d schlieβlich β ∉
TTFM((VAN(ft)∖{[β, ξ, Δ]}) и {Δ, K(ft)}). Nach Theorem 5-30 (wobei X durch
VAN(ft) u∏d Y durch VAN(ft) и {[β, ξ, Δ]} i∏sta∏ziiert wird) folgt daher i∏sgesamt
VAN(ft) к K(ft).

Zweiter Fall: Sei ∏u∏ ft ∉ AF(ftΓDom(ft)-1) и SEF(ftΓDom(ft)-1) и
NEF(ftΓDom(ft)-1) и PBF(ftΓDom(ft)-1). Da∏∏ ist zu∏achst ∏ach Theorem 3-28
VAN(ft) = VAN(ftΓDom(ft)-1). Soda∏∏ lasse∏ sich 13 U∏terfalle u∏terscheide∏.

(SBF, KEF, BEF, BBF, IBF): Sei ft ∈ SBF(ftfDom(ft)-1). Nach Defi∏itio∏ 3-3 gibt es
da∏∏ Δ ∈ GFORM, so dass Δ, ^rΔ → K(ft)^^l ∈ VER(ftΓDom(ft)-1). Wege∏ Δ, ^rΔ →
K(ft)^^l ∈ VER(ftΓDom(ft)-1) gibt es soda∏∏ j, l ∈ Dom(ft)-1, so dass Δ i∏ ftΓDom(ft)-1
bei j u∏d ^rΔ → K(ft)^^l i∏ ftΓDom(ft)-1 bei l verfugbar ist. Da∏∏ ist K(ftΓj+1) = Δ u∏d
K(ftΓl+1) = ^rΔ → K(ft)^^l. Da∏∏ gilt VAN(ftΓj+1) к Δ u∏d VAN(ftΓl+1) к ^rΔ → K(ft)^^l.
Mit Theorem 3-29-(iv) gilt da∏∏ VAN(ftΓj+1) ⊂ VAN(ftΓDom(ft)-1) u∏d VAN(ftΓl+1)
⊆ VAN(ftΓDom(ft)-1). Da VAN(ft) = VAN(ftΓDom(ft)-1) gilt damit VAN(ftj+1) ⊆
VAN(ft) u∏d VAN(ftΓl+1) ⊂ VAN(ft) u∏d somit mit Theorem 5-13 auch VAN(ft) к Δ
u∏d VAN(ft) к ^rΔ → K(ft)^^l. Theorem 5-16 ergibt VAN(ft) к K(ft). Analog zeigt ma∏
fur KEF mit Theorem 5-17, fur BEF mit Theorem 5-19, fur BBF mit Theorem 5-21 u∏d
fur IBF mit Theorem 5-32, dass VAN(ft) к K(ft).

<<   212   213   214   215   216   217   218   >>

More intriguing information