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} PARTTFM({Δ}
VAN(Q)), wobei fur alle i, jk 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 β PARTTFM({Δ} 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(ξΔπ)) = 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}, {ξ0, ., ξk} VAR, wobei fur i,
j k+1 mit i j gelte: ξi ≠ ξj, Δ FORM, wobei FV(Δ) o, ., ξk} und {βo, . βk}
PARTTFM({Δ} 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, . β} PARTTFM({Δ} VAN(Q)) ist dann βfcPARTTFM({[<β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>, ΔJ1) UEF(Q) RGS{0} und K(Q') = ξk[<βo, ., βk-1>, <ξo, ., ξk-1>, ΔJ1
und PAR TTSEQ(Q') = (PAR TTSEQ(Q)) (PAR TT(ξ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) = ξk[<βo, ., βk-1>, <ξo, ., ξk-1>, Δ]π = [<βo, ., βk-1>, <ξo, ., ξk-1>, rΛξkΔ1].

Mit FV(Δ) o, ., ξk} ist dann FV(ξkΔπ) o, ., ξk-1}, wobei die ξi mit ik
paarweise verschieden sind. Sodann ist mit {βo, . βk} PARTTFM({Δ} VAN(Q))
dann {βo, . β
k-1} PARTTFM({ ξ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, .,



More intriguing information

1. Should Local Public Employment Services be Merged with the Local Social Benefit Administrations?
2. Understanding the (relative) fall and rise of construction wages
3. The name is absent
4. Declining Discount Rates: Evidence from the UK
5. The name is absent
6. The name is absent
7. The name is absent
8. The name is absent
9. Design and investigation of scalable multicast recursive protocols for wired and wireless ad hoc networks
10. The name is absent