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(SΓDom(S)-1). Nach Definition 3-17 gibt es dann θ₀, θ₁ ∈
GTERM, ζ ∈ VAR und Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass rθ₀ = θ₁^^l, [θ₀, ζ, Δ] ∈
VER(SΓDom(S)-1) und S = SΓDom(S)-1 ∪ {(Dom(S)-1, rAlso [θ₁, ζ, Δ]∣)}. Dann ist
mit f) S⁺ = S* ∪ {(Dom(S), [β, α, rAlso [θ₁, ζ, Δ]∣])} = 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(SΓDom(S)-1)), so dass A(Si) = rθ₀ = θ₁^^l und A(Sj) = [θ₀, ζ,
Δ]. Dann gilt mit c) und d): i+1, j+1 ∈ Dom(VERS(S*)) und A(S*_i+ι) = [β, α, A(Si)] =
[β, α, rθo = θf^l ] = 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⁺) = [β, α, [θ₁, ζ, Δ]] = [[β, α, θ₁], ζ, [β, α, Δ]], wobei mit θ₀, θ₁ ∈ 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 {β*₀, .., β*_k-ι} ⊆ PAR∖TTSEQ(S), wobei fur alle i, j < k
mit i ≠ j gilt, dass β*i ≠ β*j, und {βo, ., βk-1} ⊆ PAR∖{β*o, ., β*k-1}, wobei fur i, j < k 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 {β*₀, ., β*_k} ⊆
PAR∖TTSEQ(S), wobei fur alle i, j < k+1 mit i ≠ j gelte, dass β*_i ≠ β*_j∙, und {β₀, ., β_k}
⊆ PAR, wobei fur alle i, j < k+1 mit i ≠ j gelte, dass β_i ≠ βj. Dann gilt mit I.V. [(β*₀, .,
β*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)). ■

<<   161   162   163   164   165   166   167   >>

More intriguing information