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. The name is absent
2. Survey of Literature on Covered and Uncovered Interest Parities
3. Apprenticeships in the UK: from the industrial-relation via market-led and social inclusion models
4. A Computational Model of Children's Semantic Memory
5. The name is absent
6. Geography, Health, and Demo-Economic Development
7. TWENTY-FIVE YEARS OF RESEARCH ON WOMEN FARMERS IN AFRICA: LESSONS AND IMPLICATIONS FOR AGRICULTURAL RESEARCH INSTITUTIONS; WITH AN ANNOTATED BIBLIOGRAPHY
8. NATURAL RESOURCE SUPPLY CONSTRAINTS AND REGIONAL ECONOMIC ANALYSIS: A COMPUTABLE GENERAL EQUILIBRIUM APPROACH
9. The name is absent
10. Conservation Payments, Liquidity Constraints and Off-Farm Labor: Impact of the Grain for Green Program on Rural Households in China
11. Language discrimination by human newborns and by cotton-top tamarin monkeys
12. Modelling Transport in an Interregional General Equilibrium Model with Externalities
13. Moi individuel et moi cosmique Dans la pensee de Romain Rolland
14. The name is absent
15. Fiscal federalism and Fiscal Autonomy: Lessons for the UK from other Industrialised Countries
16. Does adult education at upper secondary level influence annual wage earnings?
17. Olfactory Neuroblastoma: Diagnostic Difficulty
18. The name is absent
19. On Evolution of God-Seeking Mind
20. Peer Reviewed, Open Access, Free