Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.2 Eigenschaften der deduktiven Konsequenzschaft 203

VANS(ft⁴) = VANS(ft³) = VANS(ft¹) und (Dom(ft²), ^rAlso Γ л -Γ^π), (Dom(ft³), ^rAlso
-(Γ л -Γ)^π) ∈ VERS(ft⁴) sowιe (Dom(ft), rSeι Α^π) ∈ VANS(ft¹) = VANS(ft⁴).

Insgesamt gilt Dom(ft), Dom(ft²) ∈ Dom(ft⁴), wobei Dom(ft) ≤ Dom(ft²), A(ft⁴_Dom(_ft))
= Α und (Dom(ft), A'∣>o,,,_l∙<,∙_l) ∈ VANS(ft4), A(ft∏om(ft²)) = T л -Γ und A(ft4Dom(ft⁴)-1) =
г—(Γ л —Γ)^^l, (Dom(ft²), ^D_om(⅛2)) ∈ VERS(ft⁴) und es gibt kein l mit Dom(ft) < l ≤
Dom(ft⁴)-1, so dass (l, ft⁴_l) ∈ VANS(ft⁴). Damit ist dann schlieβlich Junftens nach
Definition 3-10 ft⁵ ∈ NEF(ft⁴) ⊂ RGS∖{0} und mit Theorem 3-20-(iv) und -(v)
VΛ∖S(C√)    = VANS(ft⁴)∖{(max(Dom(VANS(ft⁴))), ft5max(Dom(VANS(ft⁴))))}    =

VANS(ft⁴)∖{(Dom(ft), rSei Α^π)} = VANS(ft¹)∖{(Dom(ft), rSei Α^π)} = (VANS(ft) и
{(Dom(ft), rSei Α^π)})∖{(Dom(ft), rSei Α^π)} = VANS(ft)∖{(Dom(ft), rSei Α^π)} ⊆
VANS(ft). Mit Theorem 2-75 ist dann VAN(ft⁵) ⊆ VAN(ft) ⊆ (X и Y)∖{Α}. Da K(ft⁵)
= r—Α^^l, gilt mit Theorem 3-12 (X и Y)∖{Α} H r—a^ⁱ .

Zu (xvi) (PB): Sei X H ryξ∆^^ι und Y H Γ und [β, ξ Δ] ∈ Y und β ∉

TTFM((Y∖{[β, ξ, Δ]}) и {Δ, Γ}). Dann gilt mit (i): Y∖{[β, ξ, Δ]} H r[β, ξ, Δ] → Г. So-
dann gilt mit Γ ∈ GFORM: [β, ξ, Γ] = Γ. Damit ist [β, ξ, rΔ → Γ^^l] = ^r[β, ξ, Δ] → [β, ξ,
Γ]^^l = r[β, ξ, Δ] → Γ und damit gilt Y∖{[β, ξ, Δ]} H [β, ξ, rΔ → Γ^π ]. Sodann ergibt sich
mit β ∉ TTFM({Δ, Γ}), dass β ∉ TT(rΔ → Γ^π). Sodann ist mit Γ ∈ GFORM und FV(Δ)
⊆ {ξ} auch FV(rΔ → Γ^π) ⊂ {ξ}. Da nach Annahme auch β ∉ TTFM(Y∖{[β, ξ, Δ]}), gilt
dann mit (xv): Y∖{[β, ξ, Δ]} H rΛξ(Δ → Γ)^π. Mit (iii) gilt X и (Y∖{[β, ξ, Δ]}) H rΛξ(Δ
→ Γ) л VξΔ^π.

Dann gibt es nach Theorem 3-12 ein ft ∈ RGS∖{0}, so dass VAN(ft) ⊂ X и (Y∖{[β, ξ,
Δ]}) und K(ft) = rΛξ(Δ → Γ) л VξΔ^^l. Mit Theorem 4-5 gibt es dann ein ft* ∈ RGS∖{0},
so dass VAN(ft*) = VAN(ft) ⊆ Xu (Y∖{[β, ξ, Δ]}) und rΛξ(Δ → Γ)^π, rVξΔ^π∈
VER(ft*) und K(ft*) = rVξΔ^π. Mit Theorem 2-82 ist genauer (Dom(ft*)-1, Ъ VξΔ^^l) ∈
VERS(ft*) fur ein Ξ ∈ PERF. Nun gibt es ein β* ∈ PAR∖TTSEQ(ft*) und ein α ∈
KONST∖TTSEQ(ft*). Damit lasst sich ft* wie folgt zu ft⁵ ∈ SEQ mit ft⁵ΓDom(ft*) = ft*
fortsetzen:

rSei [β*, ξ, Δ∏}
rAlso α = α^-l)}
rAlso [β*, ξ, Δ] → Γ-)}

<<   <   176   177   178   179   180   181   182   >   >>