Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie



30    1 Zum grammatischen Rahmen

Gelte die Behauptung nun fur θ'0, ., θ'r-1 TERM und sei θ = rφ(θ'0, ... θ'r-1)^l
FTERM. Sei nun k N{0}, {θo, ., θw} GTERM und {ξo, ., ξk-ι} VARTT(θ),
wobei ξ
i ξj fur alle i, jk mit i ≠ j. Mit U {TT(θ'i) | ir} TT(θ), gilt dann fur alle i <
r, dass {ξ0, ., ξk-1} VARTT(θ'i). Damit gibt es nach I.V. fur jedes θ'i (i r) ein θ+i
TERM, so dass θ'i = [<θo, ., θk-ι>, <ξ1, ., ξw>, θ+i] und FV(θ+i) o, ., ξk-ι} FV(θ'i)
und TT(θ+
i) 0, ., θk-1} = 0. Dann gibt es kein i k, so dass rφ(θ'0, . θ'r-1)^l = θi,
oder es gibt ein
i k, so dass rφ(θ'0, . θ'r-1)^l = θi. Im ersten Fall ist rφ(θ'0, . θ'r-1)^l =
rφ([<θo, ., θk-ι>, <ξ0, ., ξk-ι>, θ+0], ., [<θ0, ., θk-ι>, <ξ0, ., ξk-ι>, θ+r-ι])π = [<θ0, ., θk-ι>,
<ξ0, ., ξk-ι>, rφ(θ+0, ., θ+r-ι)π]. Sodann ist FV(rφ(θ+0, ., θ+r-ι>π) = U JFV(O) | i r}
und somit mit I.V. FV(
rφ(θ+0, ., θ+r-ι)π) U{FV(θ'i) | ir} 0, ., ξk-ι} =
FV(
rφ(θ'0, ., θ'r-1)^l) 0, ., ξk-1}. Sodann ist nach Fallannahme und I.V. TT(rφ(θ+0,
., θ+
r-ι)π) 0, ., θk-ι} = ({rφ(θ+0, ., θ+r-ι)π} U{TT(θ+i) | i r}) 0, ., θk-ι} =
({
rφ(θ+0, ., θ+r-ι)π} 0, ., θk-ι}) (U{TT(θ+i) | i r} 0, ., θk-ι}) = 0
U
{TT(θ+i) 0, ., θk-1} | i r} = 0. Im zweiten Fall ist dann fur ein i k rφ(θ'0, .
θ'
r-ι)^, = [<θ0, ., θi>, <ξ0, ., ξi>, ξi]. Wegen ξi ≠ ξj fur alle i, j k mit i j, gilt aber auch
rφ(θ'0, . θ'r-ι)π = [<θ0, ., θi>, <ξ0, ., ξi>, ξi] = [<θ0, ., θk-ι>, <ξ0, ., ξk-1>, ξi] und FV(ξi)
0, ., ξk-ι} FV(rφ(θ'0, . θ'r-ι)π) und wegen ξi GTERM auch TT(ξi) 0, .,
θ
k-1} = 0. ■

Theorem 1-16. Basen fur die Substitution von geschlossenen Termen in Formeln

Wenn Δ FORM, k N{0},{θ0, ., θk-ι} GTERM und {ξ0, ., ξk-ι} VARTT(Δ), wo-
bei ξ
i ≠ ξj fur alle i, j k mit i j, dann gibt es ein Δ+ FORM, wobei FV(Δ+) 0, ., ξk-1}
FV(Δ) und TT(Δ+) 0, ., θk-ι} = 0, so dass Δ = [<θ0, ., θk-ι>, <ξ0, ., ξk-ι>, Δ+].

Beweis: Durch Induktion uber den Formelaufbau von Δ. Sei Δ = rΦ(θ'0, . θ'r-1)^l
AFORM. Sei nun k N\{0}, {θ0, ., θk-1} GTERM und {ξ0, ., ξk-1}
VARVΓT(rΦ(θ'0, . θ'r-1)^l), wobei ξi ≠ ξj fur alle i, j k mit i j. Mit U {TT(θ'i) | i r} =
TT(
rΦ(θ'0, . θ'r-1)π), gilt dann fur alle i r, dass {ξ0, ., ξk-1} VARTT(θ'i). Dann
gibt es nach Theorem 1-15 fur jedes θ'
i (i r) ein θ+i TERM, so dass θ'i = [<θ0, ., θk-1>,
<ξ0, ., ξk-1>, θ+i] und FV(θ+i) 0, ., ξk-1} FV(θ'i) und TT(θ+i) 0, ., θk-1} = 0.
Dann ist
rΦ(θ'0, . θ'r-ι)π = rΦ([(θ0, ., θk-ι>, <ξ0, ., ξk-ι>, θ+0], ., [<θ0, ., θk-ι>, <ξ0, .,
ξ
k-ι>, θ+r-ι])π = [<θ0, ., θk-ι>, <ξ0, ., ξk-ι>, rΦ(θ+0, ., θ+r-ι)π]. Sodann ist FV(rΦ(θ+0, .,
θ+
r-ι)π) = U{FV(θ+i) | i r} und daher FV(rΦ(θ+0, ., θ+r-ι)π) U{FV(θ'i) | i r} 0,



More intriguing information

1. The urban sprawl dynamics: does a neural network understand the spatial logic better than a cellular automata?
2. MATHEMATICS AS AN EXACT AND PRECISE LANGUAGE OF NATURE
3. The name is absent
4. Commitment devices, opportunity windows, and institution building in Central Asia
5. The name is absent
6. WP 1 - The first part-time economy in the world. Does it work?
7. The name is absent
8. AGRIBUSINESS EXECUTIVE EDUCATION AND KNOWLEDGE EXCHANGE: NEW MECHANISMS OF KNOWLEDGE MANAGEMENT INVOLVING THE UNIVERSITY, PRIVATE FIRM STAKEHOLDERS AND PUBLIC SECTOR
9. The Mathematical Components of Engineering
10. On s-additive robust representation of convex risk measures for unbounded financial positions in the presence of uncertainty about the market model