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 θ0, θ1 ∈
GTERM, ζ ∈ VAR und Δ ∈ FORM, wobei FV(Δ) ⊆ {ζ}, so dass rθ0 = θ1^l, [θ0, ζ, Δ] ∈
VER(SΓDom(S)-1) und S = 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(SΓ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-ι} ⊆ 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 {β*0, ., β*k} ⊆
PAR∖TTSEQ(S), wobei fur alle i, j < k+1 mit i ≠ j gelte, dass β*i ≠ β*j∙, und {β0, ., βk}
⊆ PAR, wobei fur alle i, j < k+1 mit i ≠ j 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)). ■