Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

198   4 Theoreme zur deduktiven Konsequenzschaft

(xvi)  Wenn X H  ^rVξΔ^π und Y H Γ und [β, ξ Δ] ∈ Y und β ∉ (PB)

TTFM((Y∖{[β, ξ, Δ]}) ∪ {Δ, Γ}), dann X ∪ (Y∖{[β, ξ, Δ]}) H Γ,

(xvii)  Wenn X ⊆ GFORM, dann X H ^rθ₀ = θ₀^^l, und                             (IE)

(xviii) Wenn X H ^rθ₀ = θ₁^^l und Y H [θ₀, ξ, Δ], dann X ∪ Y H [θ₁, ξ, Δ].             (IB)

Beweis: Seien Α, Β, Γ ∈ GFORM, θ0, θ1 ∈ GTERM, ξ ∈ VAR und Δ ∈ FORM, wobei
FV(Δ) ⊆ {ξ}. Es wird zunachst der Fall (i) behandelt, bei dem sich die Pramissenmenge
verkleinert. Es folgen die Falle (ii), (iii), (v), (vii) und (xviii), bei denen zwei Pramissen-
mengen vereinigt werden. In den Fallen (iv), (viii), (xii), (xiii), (xiv) und (xv) bleibt die
Pramissenmenge unverandert. In der Reihenfolge (vi), (ix), (x), (xi), (xvi), (xvii) werden
die verbleibenden Sonderfalle bearbeitet.

Zu (i) (SE): Sei X H Β und Α ∈ X. Dann gibt es nach Theorem 3-12 ein ft ∈ RGS∖{0},
so dass K(ft) = Β und VAN(ft) ⊆ X. Dann gibt es mit Theorem 4-2 ein ft' ∈ RGS∖{0},
so dass VAN(ft') ⊆ VAN(ft) und K(ft') = K(ft) und fur alle i ∈ Dom(VANS(ft')): Wenn
ʌ(ft'i) = Α, dann i = max(Dom(VANS(ft'))). Dann gilt mit Theorem 2-82 Β = K(ft') ∈
VER(ft'). Sodann lassen sich mit Α ∈ VAN(ft') und Α ∉ VAN(ft') zwei Falle unterschei-
den.

Erster Fall: Sei Α ∈ VAN(ft'). Dann ist VANS(ft') ≠ 0 und es gilt fur alle i ∈
Dom(VANS(ft')): A(ft'i) = Α gdw i = max(Dom(VANS(ft'))). Dann ist mit Theorem 3-18
ft⁺ = ft^,^{(0, ^rAlso Α → Β^^l)} ∈ SEF(ft') ⊆ RGS∖{0}. Dann gilt mit Theorem 3-22, dass
VAN(ft⁺) ⊆ VAN(ft')∖{Α} ⊆ VAN(ft)∖{Α} ⊆ X∖{Α}. Damit gilt insgesamt: ft⁺ ∈
RGS∖{0}, K(ft⁺) = rΑ → Β^^l und VAN(ft⁺) ⊆ X∖{Α} und damit mit Theorem 3-12
X∖{Α} H rΑ → Β^π.

Zweiter Fall: Sei nun Α ∉ VAN(ft'). Dann lasst sich ft' wie folgt zu einem ft⁴ ∈ SEQ
mit ft⁴ΓDom(ft') = ft' fortsetzen:

Zunachst ist ft⁴D_om(_ft,) ∈ ASATZ. Mit Theorem 1-8, Theorem 1-10 und Theorem 1-11 gilt
sodann K(ft¹) ≠ K(ft²) und K(ft²) ≠ K(ft³). Weiter gilt, dass K(ft²) weder eine Subjunk-
tion noch eine Negation ist. Sodann gilt mit Theorem 1-8, dass K(ft³) = Β ≠ rΑ → (Α ∧

<<   <   171   172   173   174   175   176   177   >   >>