Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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(Δ) ⊆ {ξ₀, ., ξ_k-₁}, und ^rΛξ₀ .
Λξ_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:

<<   163   164   165   166   167   168   169   >>

More intriguing information