Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.2 Eigenschaften der deduktiven Konsequenzschaft 201

Theorem 2-61 gilt dann, dass fur alle k mit 2 ≤ k ≤ 6 gilt: ft^k ∉ SEF(ft^k-1) и NEF(ft^k-1) и
PBF(ft^k-1).

Hingegen ist erstens nach Definition 3-1 ft¹ ∈ AF(ft) ⊂ RGS∖{0} und mit Theorem
3-15 VERS(ft¹) = VERS(ft) и {(Dom(ft), ^rSei α = α∣)} und VANS(ft¹) = VANS(ft) и
{(Dom(ft), rSei α = α∣)} und r(Α v Β) л ((Α → Γ) л (Β → Γ))∣ ∈ VER(ft) ⊂ VER(ft¹).
Also ist zweitens nach Definition 3-5 ft² ∈ KBF(ft¹) ⊆ RGS∖{0} und mit Theorem 3-25
VERS(ft²) = VERS(ft¹) и {(Dom(ft¹), rAlso Α v Β∣)}. Damit gilt VANS(ft²) =
VANS(ft¹), r(Α v Β) л ((Α → Γ) л (Β → Γ))∣ ∈ VER(ft¹) ⊆ VER(ft²) und rΑ v Β∣ ∈
VER(ft²). Also ist drittens nach Definition 3-5 ft³ ∈ KBF(ft²) ⊆ RGS∖{0} und mit
Theorem 3-25 VERS(ft³) = VERS(ft²) и {(Dom(ft²), rAlso (Α → Γ) л (Β → Γ)∣)}.
Damit gilt VANS(ft³) = VANS(ft²), rΑ v Β∣ ∈ VER(ft²) ⊆ VER(ft³) und r(Α → Γ) л
(Β → Γ)^^l ∈ VER(ft³). Also ist viertens nach Definition 3-5 ft⁴ ∈ KBF(ft³) ⊆ RGS∖{0}
und mit Theorem 3-25 VERS(ft⁴) = VERS(ft³) и {(Dom(ft³), rAlso Α → Γ∣)}. Damit
gilt VANS(ft⁴) = VANS(ft³), rΑ v Β∣, ^r(Α → Γ) л (Β → Γ)∣ ∈ VER(ft³) ⊆ VER(ft⁴)
und rΑ → Γ ∈ VER(ft⁴). Also ist funftens nach Definition 3-5 ft⁵ ∈ KBF(ft⁴) ⊆
RGS∖{0} und mit Theorem 3-25 VERS(ft⁵) = VERS(ft⁴) и {(Dom(ft⁴), rAlso Β → Γ¹)}.
Damit gilt VANS(ft⁵) = VANS(ft⁴), rΑ v Β∣, rΑ → Γ ∈ VER(ft⁴) ⊆ VER(ft⁵) und Ъ
→ Γ ∈ VER(ft⁵). SchlieBlich ist sechstens nach Definition 3-9 ft⁶ ∈ ABF(ft⁵) ⊆
RGS∖{0} und mit Theorem 3-25 VERS(ft⁶) = VERS(ft⁵) и {(Dom(ft⁵), rAlso Γ∣)}. Da-
mit gilt VANS(ft⁶) = VANS(ft⁵) = VANS(ft) и {(Dom(ft), rSei α = α∣)}. Damit gilt
VAN(ft⁶) = VAN(ft) и {rα = α∣} und es gilt Γ ∈ VER(ft⁶). Dann gibt es mit Theorem
4-7 ein ft⁺ ∈ RGS∖{0}, so dass VAN(ft⁺) ⊂ VAN(ft⁶)∖{Γα = α∣} = (VAN(ft) и {⅛ =
α^^l})∖{rα = α∣} = VAN(ft)∖{Γα = α∣} ⊂ (X и Y и Z)X{^rα = α∣} ⊂ X и Y и Z und
K(ft⁺) = Γ. Damit gilt dann nach Theorem 3-12 X и Y и Z H Γ.

Zu (x) (AB*): Sei X H га v Β^^l und Y H Γ und Α ∈ Y und Z H Γ und Β ∈ Z. Dann gilt
mit (i): Y∖{Α} H га → Β^^l und Z\{Β} H гв → Α^^l. Dann gilt mit (ix): X и (Y∖{Α}) и
(Z∖ {Β}) H г.

Zu (xi) (NE): Sei X H Γ und Y H Г—Γ und Α ∈ X и Y. Ist Α = ^rΔ' ∧ —Δ'∣ fur ein Δ'
∈ GFORM, dann gilt mit Theorem 4-17 direkt: (X и Y)∖{Α} H %(Δ' ∧ — Δ')∣ = Г—Α∣.
Sei nun Α ≠ ^rΔ' л —Δ'∣ fur alle Δ'. Mit (iii) ergibt sich zunachst: X и Y H T л -Γ^π. So-
dann gilt wiederum mit Theorem 4-17: X и Y H Г—(Γ л — Γ)∣ und damit mit (iii): X и

<<   174   175   176   177   178   179   180   >>

More intriguing information