190 4 Theoreme zur deduktiven Konsequenzschaft
ξk-ι), rΛξkΔπ] ein S* ∈ RGS∖{0}, so dass PAR ∩ TTSEQ(S*) = PAR ∩ TTSEQ(S') =
PAR ∩ TTSEQ(S), VAN(S*) ⊆ VAN(S') ⊆ VAN(S) und K(S*) = rΛξo.ΛξfcΔπ. ■
Theorem 4-12. UB-Fortsetzung einer Sequenz
Wenn S ∈ RGS∖{0}, k ∈ N∖{O}, {θo, ., θjw} ⊆ GTERM, {ξo, ., ξw} ⊆ VAR, wobei fur
alle i, j < k mit i ≠ j gilt, dass ξi ≠ ξj, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξ0, ., ξk-1}, und rΛξ0 .
Λξk-1Δπ ∈ VER(S), dann gibt es ein S* ∈ RGS∖{0}, so dass
(i) Dom(S*) = Dom(S)+k,
(ii) S*t^Dom(S) = S,
(iii) VAN(S*) ⊆ VAN(S),
(iv) Fur alle i < k-1 gilt: K(S* [Dom(S)+i+1) = ‰ . ' - [<θo, ., θi), <ξo, ., ξi>, ΔΓ,
und
(v) K(S*) = [<θo, ., θk-ι), <ξo, ., ξk-1>, Δ].
Beweis: Durch Induktion uber k: Sei k = 1. Seien S ∈ RGS∖{0}, θ ∈ GTERM, ξ ∈ VAR,
Δ ∈ FORM, wobei FV(Δ) ⊆ {ξ} und rΛξΔ^l ∈ VER(S). Dann gilt mit Definition 3-13:
S* = S~{(O, rAlso [θ, ξ, Δ]^l)} ∈ UBF(S) ⊆ RGS∖{0} und es ist Dom(S*) = Dom(S)+1
und S*ΓDom(S) = S und mit Theorem 3-27-(v) ist VAN(S*) ⊆ VAN(S), (iv) ist wegen
k = 1 trivialerweise erfullt und K(S') = [θ, ξ, Δ].
Gelte die Behauptung nun fur k und sei S ∈ RGS∖{0}, {θo, ., θk} ⊆ GTERM, {ξo, .,
ξk} ⊆ VAR, wobei fur alle i, j < k+1 mit i ≠ j gelte, dass ξi ≠ ξj, Δ ∈ FORM, wobei
FV(Δ) ⊆ {ξo, ., ξfc}, und rΛξo . ΛξfcΔπ ∈ VER(S). Dann gilt mit FV(Δ) ⊆ {ξo, ., ξfc},
dass FV(Λξι . ΛξkΔ) ⊆ {ξo} und mit θo ∈ GTERM und rΛξo . Λξ⅛Δ^l ∈ VER(S) gilt
mit Definition 3-13: S' = S^{(O, rAlso [θo, ξo, Λξ1 . ΛξfcΔ]π)} ∈ UBF(S) ⊆ RGS∖{0}.
Dann ist Dom(S') = Dom(S)+1 und STDom(S) = S und mit Theorem 3-27-(v) ist
VAN(S') ⊆ VAN(S). Wegen der paarweisen Verschiedenheit der ξi ist sodann fur alle i
mit O < i ≤ k: ξo ≠ ξi. Damit ist dann K(S') = [θo, ξo, rΛξ1 . ΛξfcΔ^l ] = rΛξ1 . Λξfc[θo, ξo,
Δ]π.
Sei nun ζi = ξi+1 und θ'i = θi+1 fur alle i ∈ k. Dann gilt {θ'o, ., θ'k-1} ⊆ GTERM, {ζo, .,
ζk-1} ⊆ VAR, wobei fur alle i, j < k mit i ≠ j gilt, dass ζi ≠ ζj, [θo, ξo, Δ] ∈ FORM, wobei
mit FV(Δ) ⊆ {ξo, ., ξk} und θo ∈ GTERM gilt: FV([θo, ξo, Δ]) ⊆ {ξ1, ., ξk} = {ζo, .,
ζfc-1}, und mit Theorem 2-82 gilt: . Λζfc4[θo, ξo, ʌ]ɔ = . Λξfc[θo, ξo, ʌ]ɔ =
K(S') ∈ VER(S'). Dann gilt mit I.V., dass es ein S* ∈ RGS∖{0} gibt, so dass: