Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

162   4 Theoreme zur deduktiven Konsequenzschaft

{Α(⅛¹maχ(Dom(VANs_ω⅛))}   ⊆ VAN(⅛). Ferner ist mit Theorem 3-15-(vi)

^{A(^ max(Dom(VANS(⅛¹)))), ^A(^¹max(Dom(VANS(⅛¹)))) → K(-AΓ} ⊆ VER(⅛8). Sodann gilt mit Γ
∉ VAN(>Y) und Α(A ¹_max(_Dom(_VANS(^i)))) ≠ Γ auch Γ ∉ VAN(A8) und damit fur alle i ∈
Dom(VA∖S(.A8): A(⅛8i) ≠ Γ. Dann gilt trivialerweise fur alle i ∈ Dom(VANS(A8)):
Wenn A(⅛8i) = Γ, dann i = max(Dom(VANS(⅛⁸))). Dann ist .A9 = .A8"~"{(0, ^rAlso K(.AΓ)}
∈ SBF(⅛⁸) und mit Theorem 3-27-(v) gilt VAN(⅛⁹) ⊆ VAN(⅛⁸) ⊆ VAN(W). Ferner gilt
fur alle i ∈ Dom(VANS(W⁹)) wiederum trivialerweise: Wenn A(W9i) = Γ, dann i =
max(Dom(VA∖S(.A9))). Damit ist W’ das gesuchte Element von RGS∖{0}. ■

Theorem 4-3. Blockierende Annahmen

Wenn 21. ein geschlossener Abschnitt in W ist, i ∈ Dom(2l.) ∩ Dom(ANS(W)), Δ = A(Wi) und
PAR ∩ TT(Δ) = 0, dann gibt es ein j ∈ Dom(W), so dass i ≠ j und Δ ∈ TA(W_j).

Beweis: Sei 21 ein geschlossener Abschnitt in W, i ∈ Dom(W) ∩ Dom(ANS(W)), Δ =
A(Wi) und PAR ∩ TT(Δ) = 0. Mit Theorem 2-47 gilt dann, dass es einen geschlossenen
Abschnitt Y in W mit Y ⊆ W gibt, so dass i = min(Dom(Φ)). Mit Theorem 2-42 ist ®
dann ein SE- oder ein NE- oder ein EA-artiger Abschnitt in W. Sei ® ein SE- oder ein
NE-artiger Abschnitt in W. Dann gilt mit Definition 2-11 und Definition 2-12, dass
max(Dom(Y)) ∈ Dom(W), ma∖(Dom(Y)) ≠ i und Δ ∈ TA(W_max(D_om(S))). Sei nun Y ein
EA-artiger Abschnitt in W. Dann gilt mit Definition 2-13: min(Dom(®))-1 ∈ Dom(W)
und min(Dom(®))-1 ≠ i. Sodann gibt es ξ ∈ VAR, Δ⁺ ∈ FORM, wobei FV(Δ⁺) ⊆ {ξ}
und β ∈ PAR, so dass A(Wmin(Dom(<B))-1) = r∀ξΔ⁺^^, und Δ = A(Wmin(Dom(<B))) = [β, ξ, Δ⁺]. Da
nun nach Annahme PAR ∩ TT(Δ) = 0, ist dann β ∉ TT([β, ξ, Δ⁺]) und mit Theorem
1-14-(ii) Δ = [β, ξ, Δ⁺] = Δ⁺. Damit ist dann A(W_min(Do_m(S))_-1) = r√ξΔ^π und somit Δ ∈
TA(⅛min(Dom(S))-1) und die Behauptung gilt. ■

Theorem 4-4. Verkettung parameterfremder RGS-Elemente mit eingeschobener blockierender
Annahme

Wenn W, ⅛' ∈ RGS, PAR ∩ TTSEQ(W) ∩ TTSEQ(W) = 0 und α ∈ KONST∖(TTSEQ(W) ∪
TTSEQ(W)), dann gibt es ein W* ∈ RGS∖{0}, so dass

(i)   Dom(W*) = Dom(W)+1+Dom(W'),

(ii)   W*t^Dom(W) = W,

(iii)   ⅛*Dom(f>) = rSei α = α¹,

(iv) Fur alle i ∈ Dom(W) ist W i ⅛ * Dom(W)+1+i^,

<<   135   136   137   138   139   140   141   >>

More intriguing information