Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 193

TTSEQ(ft'), wobei fur alle i, j < k mit i ≠ j gelte β_i ≠ βj. Nun gibt es β*_o, ..., β*_k-1 ∈
PAR∖(TTSEQ(ft) и TTSEQ(ft')), wobei fur alle i, j < k: Wenn i ≠ j, dann β*_i ≠ β*_j∙. So-
dann gibt es ξ_o, ..., ξ_k-1 ∈ VAR∖(TTSEQ(ft) и TTSEQ(ft')), wobei fur alle i, j < k: Wenn
i ≠ j, dann ξ_i ≠ ξj.

Nun gilt mit Theorem 2-77 wegen VANS(ft') = 0 auch VAN(ft') = 0. Sodann gibt es
mit Theorem 1-16 ein Δ ∈ FORM, wobei FV(Δ) ⊂ {ξ₀, ., ξ_k-1} и FV(K(ft')) = {ξ₀, .,
ξk-ι} und TT(Δ) ∩ {βo, ., βk-ι} = 0, so dass K(ft') = [<βo, ., βk-1>, <ξo, ., ξk-1>, Δ]. Mit
Theorem 4-11 gilt dann, dass es ein ft¹ ∈ RGS∖{0} gibt, so dass PAR ∩ TTSEQ(ft¹) =
PAR ∩ TTSEQ(ft'), VAN(ft¹) ⊂ VAN(ft') = 0 und damit auch VANS(ft¹) = 0 und K(ft¹)
= ^rΛξo.Λξk-1Δ^^,. Sodann gilt dann mit K(ft') = [<βo, ., βk-1>, <ξo, ., ξk-1>, Δ], dass PAR
∩ TT(Δ) ⊂ PAR ∩ TTSEQ(ft') = {βo, ., βk-1} und damit mit TT(Δ) ∩ {βo, ., βk-1} = 0,
dass PAR ∩ TT(Δ) = PAR ∩ TT(^rΛξ₀...Λξ_wΔ'∣) = PAR ∩ TT(K(ft¹)) = 0.

Sodann gilt mit Theorem 4-Ю: ft² = [<β*_o, ., β*_k-1>, <β_o, ., β_k-1>, ft¹] ∈ RGS und
Dom(VERS(ft²)) = Dom(VERS(ft¹)) und damit Dom(VANS(ft ²)) = Dom(VANS(ft¹)) =
0 und somit auch VAN(ft²) = 0. Auberdem ist dann PAR ∩ TTSEQ(ft) ∩ TTSEQ(ft²) ⊂
PAR ∩ TTSEQ(ft) ∩ {β*o, ., β*k-1} = 0. Ferner gilt wegen PAR ∩ TT(K(ft¹)) = 0, dass
K(ft²) = [<β*o, ., β*k-1>, <βo, ., βk-1>, K(ft¹)] = K(ft¹) = ^rΛξo. Λξk-1Δ". Nun gibt es ein α
∈ KONST∖(TT(ft) и TT(ft²)). Mit Theorem 4-4 gibt es dann wegen PAR ∩ TTSEQ(ft)
∩ TTSEQ(ft²) = 0 ein ft³ ∈ RGS∖{0}, so dass:

a)   Dom (ft³) = Dom(ft)+1+Dom(ft²),

b) ft³[^Dom(ft) = ft,

c) ft³Dom(ft) = ^rSei α = α ∣,

d)    Fur alle i ∈ Dom(ft²) ist ft²,_: = ft³Dom(ft)+1+i,

e)   Dom(VERS(ft³)) = Dom(VERS(ft)) и {Dom(ft)} и {(Dom(ft)+1+l | l ∈

Dom(VERS(ft²))},

f) VER(ft³) = VER(ft) и {rα = α∣} и VER(ft²) und

g) VAN(ft³) = VAN(ft) и {rα = α∣} и VAN(ft²) = VAN(ft) и {^rα = α∣}.

Nun ist mit Theorem 2-82 K(ft) ∈ VER(ft) und somit mit f) K(ft) ∈ VER(ft³). Sodann
ist rΛξ_o.Λξ_k-1Δ∣ = K(ft²) = K(ft³). Mit Theorem 4-12 gibt es dann ein ft⁴ ∈ RGS∖{0},
so dass

h)   Dom(ft⁴) = Dom(ft³)+k,

i)     ft⁴[^Dom(ft³) = ft³,

j)   VAN(ft⁴) ⊂ VAN(ft³) = VAN(ft) и {^rα = α∣},

<<   <   166   167   168   169   170   171   172   >   >>