Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 189

Theorem 4-11. UE-Fortsetzung einer Sequenz

Wenn Q ∈ RGS∖{0}, k ∈ N∖{0}, {ξ_o, ., ξ_k-ι} ⊆ VAR, wobei fur alle i, j < k mit i ≠ j gilt: ξi
≠ ξj, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξo, ., ξk-ι}, und {βo, ... βk-1} ⊆ PAR∖TTFM({Δ} ∪
VAN(Q)), wobei fur alle i, j < k mit i ≠ j gilt: βi ≠ βj, und K(Q) = [<βo, ., βk-1>, <ξo, ., ξ⅛-ι>,
Δ], dann gibt es ein Q* ∈ RGS∖{0}, so dass

(i) PAR ∩ TTSEQ(Q*) = PAR ∩ TTSEQ(Q),

(ii)  VAN(Q*) ⊆ VAN(Q) und

(iii) K(Q*) = 'ξ.'ξ Δ'.

Beweis: Durch Induktion uber k. Sei k = 1 und Q ∈ RGS∖{0}, sei ξ ∈ VAR, Δ ∈ FORM,
wobei FV(Δ) ⊆ {ξ} und β ∈ PAR∖TTFM({Δ} ∪ VAN(Q)) und K(Q) = [β, ξ, Δ]. Da dann
mit Theorem 2-82 [β, ξ, Δ] = K(Q) ∈ VER(Q), ist nach Definition 3-12 Q* = Q ∪
{(Dom(Q), ^rAlso ΛξΔ^^l) ∈ UEF(Q) ⊆ RGS∖{0} und K(Q*) = ^rΛξΔ^^l. Sodann ist PAR ∩
TTSEQ(Q*) = (PAR ∩ TTSEQ(Q)) ∪ (PAR ∩ TT(rΛξΔ^π)) = PAR ∩ TTSEQ(Q) und mit
Theorem 3-26-(v) ist VAN(Q*) ⊆ VAN(Q).

Gelte die Behauptung nun fur k und sei Q ∈ RGS∖{0}, {ξ₀, ., ξ_k} ⊆ VAR, wobei fur i,
j < k+1 mit i ≠ j gelte: ξi ≠ ξj, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξo, ., ξk} und {βo, . βk} ⊆
PAR∖TTFM({Δ} ∪ VAN(Q)), wobei fur i, j < k+1 mit i ≠ j gelte: β_i ≠ β_j, und K(Q) =
[<βo, ., β_fc>, <ξo, ., ξ_fc>, Δ]. Mit Theorem 1-28-(ii) ist dann K(Q) = [<βo, ., β_fc>, <ξo, .,
ξk>, Δ] = [βk, ξk, [<βo, ., βk-1>, <ξo, ., ξk-1>, Δ]]. Mit FV(Δ) ⊆ {ξo, ., ξk} ist dann
FV<[<βo, ., βk-1>, <ξo, ., ξk-1>, Δ]) ⊆ {ξk} und mit der paarweisen Verschiedenheit der βi
und {βo, . β⅛} ⊆ PAR∖TTFM({Δ} ∪ VAN(Q)) ist dann β_fc ∈ PAR∖TTFM({[<βo, .,
βk-1>, <ξo, ., ξ_fc-1>, Δ]} ∪ VAN(Q)). Da sodann [β_fc, ξ_fc, [<βo, ., βk-1>, <ξo, ., ξk-1>, Δ]] =
K(Q) ∈ VER(Q) ist nach Definition 3-12 Q' = Q ∪ {(Dom(Q), rAlso Λξ_k[<β_o, ., β_k-1>,
<ξo, ., ξk-1>, ΔJ¹) ∈ UEF(Q) ⊆ RGS∖{0} und K(Q') = rΛξk[<βo, ., βk-1>, <ξo, ., ξk-1>, ΔJ¹
und PAR ∩ TTSEQ(Q') = (PAR ∩ TTSEQ(Q)) ∪ (PAR ∩ TT(rΛξk[<βo, ., βk-1>, <ξo, .,
ξ_k-1>, Δ]^^l)) = PAR ∩ TTSEQ(Q) und mit Theorem 3-26-(v) ist VAN(Q') ⊆ VAN(Q).
Wegen der paarweisen Verschiedenheit der ξi ist sodann fur alle i < k: ξi ≠ ξk. Damit ist

dann K(Q) = rΛξk[<βo, ., βk-1>, <ξo, ., ξk-1>, Δ]^π = [<βo, ., βk-1>, <ξo, ., ξk-1>, ^rΛξkΔ¹].

Mit FV(Δ) ⊆ {ξo, ., ξk} ist dann FV(rΛξkΔ^π) ⊆ {ξo, ., ξk-1}, wobei die ξi mit i < k
paarweise verschieden sind. Sodann ist mit {β_o, . β_k} ⊆ PAR∖TTFM({Δ} ∪ VAN(Q))
dann {β_o, . β_k-1} ⊆ PAR∖TTFM({ rΛξ_kΔ^^l} ∪ VAN(Q)), wobei die βi mit i < k ebenfalls
paarweise verschieden sind. Nach I.V. gibt es damit mit K(Q') = [<β_o, ., β_k-1>, <ξ_o, .,

<<   162   163   164   165   166   167   168   >>

More intriguing information