Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie



188   4 Theoreme zur deduktiven Konsequenzschaft

{(Dom(S), [β, α, rAlso θ = θ])} = S* {(Dom(S), rAlso [β, α, θ] = [β, α, θ])}, wobei
mit θ
GTERM auch [β, α, θ] GTERM. Damit ist dann S+ IEF(S*) RGS.

(IBF): Sei nun S IBF(Dom(S)-1). Nach Definition 3-17 gibt es dann θ0, θ1
GTERM, ζ VAR und Δ FORM, wobei FV(Δ) {ζ}, so dass rθ0 = θ1^l, [θ0, ζ, Δ]
VER(Dom(S)-1) und S = Dom(S)-1 {(Dom(S)-1, rAlso [θ1, ζ, Δ])}. Dann ist
mit f)
S+ = S* {(Dom(S), [β, α, rAlso [θ1, ζ, Δ]])} = S* {(Dom(S), rAlso [β, α,
1, ζ, Δ]])}. Mit rθ0 = θf, [Θo, ζ, ∆] VER(SfDom(S)G) und Definition 2-30 gibt es
sodann
i, j ∈ Dom(VERS(Dom(S)-1)), so dass A(Si) = rθ0 = θ1^l und A(Sj) = [θ0, ζ,
Δ]. Dann gilt mit c) und d):
i+1, j+1 Dom(VERS(S*)) und A(S*i) = [β, α, A(Si)] =
[β, α,
rθo = θfl ] = r[β, α, Θo] = [β, α, θʃ und A(S*j+1) = [β, α, A(Sj)]. Dann ist mit
Theorem 1-26-(ii) A(
S*j+1) = [β, α, A(j = [β, α, [Θo, ζ, Δ]] = [[β, α, Θo], ζ, [β, α, Δ]]
und K(
S+) = [β, α, [θ1, ζ, Δ]] = [[β, α, θ1], ζ, [β, α, Δ]], wobei mit θ0, θ1 GTERM auch
[β, α, θ
o], [β, α, θ1] GTERM und mit FV(Δ) {ζ} auch FV([β, α, Δ]) {ζ}. Damit
gilt dann insgesamt
S+ IBF(S*) RGS. ■

Im Beweis des folgenden Theorems dient Theorem 4-8 als Induktionsbasis und als Hilfs-
mittel im Induktionsschritt. Das Theorem dient zur Vorbereitung der RGS-treuen Verket-
tung zweier RGS-Elemente, die nicht parameterfremd sind.

Theorem 4-10. Mehrfache Substitution von neuen und paarweise Verschiedenen Parametern
furpaarweise Verschiedene Parameter ist RGS-treu

Wenn S RGS, k N{0} und {β*0, .., β*k-ι} PARTTSEQ(S), wobei fur alle i, j k
mit ij gilt, dass β*i ≠ β*j, und {βo, ., βk-1} PAR{β*o, ., β*k-1}, wobei fur i, jk mit i
j gilt, dass βi ≠ βj, dann ist [(β*o, ., β*k-1>, (βo, ., βk-1>, S] RGS und Dom(VERS([(β*o,
., β*
k-1>, (βo, ., βk-1>, S])) = Dom(VERS(S)).

Beweis: Durch Induktion uber k. Die Behauptung gilt mit Theorem 4-8 fur k = 1. Gelte
die Behauptung nun fur
k. Sei nun S ∈ RGS, k+1 ∈ N∖{0} und {β*0, ., β*k}
PARTTSEQ(S), wobei fur alle i, jk+1 mit ij gelte, dass β*i ≠ β*j∙, und {β0, ., βk}
PAR, wobei fur alle i, jk+1 mit ij gelte, dass βi ≠ βj. Dann gilt mit I.V. [(β*0, .,
β*
k-1>, (βo, ., βk-1>, S] RGS und Dom(VERS([(β*o, ., β*k-1>, (βo, ., βk-1>, S])) =
Dom(VERS(
S)). Sodann ist mit Theorem 1-27-(iv) [β*k, βk, [(β*o, ., β*k-1>, (βo, ., βk-1>,
S]] = [(β*o, ., β*k>, (βo, ., βk>, S] und mit Theorem 4-8 dann [(β*o, ., β*k>, (βo, ., βk>,
S] RGS und Dom(VERS([(β*o, ., β*k>, (βo, ., βk>, S])) = Dom(VERS([(β*o, .,
β*
k-1>, (βo, ., βk-1>, S])) = Dom(VERS(S)). ■



More intriguing information

1. The name is absent
2. The name is absent
3. The name is absent
4. Biological Control of Giant Reed (Arundo donax): Economic Aspects
5. Public infrastructure capital, scale economies and returns to variety
6. The name is absent
7. The name is absent
8. Real Exchange Rate Misalignment: Prelude to Crisis?
9. A Classical Probabilistic Computer Model of Consciousness
10. The name is absent