Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.2 Eigenschaften der deduktiven Konsequenzschaft 197

U PBF(W). Mit Theorem 3-25 gilt dann VERS(W) = VERS(W) и {(1, ^rAlso Γ)} =
VΓ2. Sodann gilt mit Theorem 3-27-(ii) und -(iii), dass VANS(VΓ2) = VANS(VΓ1) und
damit VAN(W) = VAN(W) = {T л —E^π}.

Wiederum nach Definition 3-5 ist sodann ⅛Γ3 ∈ KBF(⅛Γ2) ⊂ RGS∖{0}. Da nach
Theorem 1-8 T л —E^^l ∉ TF(Γ) und Γ ≠ Г—E^^l, gilt sodann nach Definition 3-2,
Definition 3-10 und Definition 3-15, dass VΓ3 ∉ SEF(⅛Γ2) и NEF(⅛Γ2) и PBF(⅛Γ2).
Mit Theorem 3-25 gilt dann wiederum VERS(VΓ3) = VERS(VΓ2) и {1, Wso — E^^l)} =
VlA und mit Theorem 3-27-(ii) und -(iii), dass VANS(VlA) = VANS(VlA) und damit
VAN(W) = VAN(W) = {T л — Γ}. Dann ist 0 = max(Dom(VANS(W))) und 1, 2 ∈
Dom(VERS(V∣A)) und A(VlA_i) = Γ und A(VlA₂) = r—Γ. Damit ist dann nach Definition
3-10 V ∈ NEF(W) und nach Theorem 3-20 ist VANS(V) = VANS(W)W, Wi Γ л
—E^^l)} = 0 und damit auch VAN(V) = 0. Damit gilt insgesamt: V ∈ RGS∖{0} und
VAN(V) = 0 und K(V) = r—(Γ л — E)^^l. Mit Theorem 3-12 gilt damit 0 H г—(e ∧ — E)^^l
und damit mit Theorem 4-16 X H r—(Γ л — Γ)^^l. ■

Theorem 4-18. Abgeschlossenheit unter Einfuhrung und Beseitigung

Wenn Α, Β, E ∈ GFORM, θ₀, θ₁ ∈ GTERM, ξ ∈ VAR und Δ ∈ FORM, wobei
FV(Δ) ⊂ {ξ}, dann:

(i)   Wenn X H Β und Α ∈ X, dann X\{Α} H га → b∖                     (SE)

(ii)  Wenn X H Α und Y H га → B¹, dann X и Y H Β,                      (SB)

(iii)  Wenn X H Α und Y H Β, dann X и Y H га λ Β^π,                       (KE)

(iv)  Wenn X H га л Β"¹ oder X H ^rΒ л Α"¹, dann X H Α,                     (KB)

(v)  Wenn X H га → Β^^l und Y H ^rΒ → Α^π, dann X и Y H га θ B^π,         (BE)

(vi)  Wenn X H Β und Α ∈ X und Y H Α und Β ∈ Y, dann (X\{Α}) и (Y\{B})  (BE*)

H га → B¹,

(vii)  Wenn X H Α und Y H га θ B^π oder Y H ^rB θ Α"¹, dann X и Y H B,      (BB)

(viii)  Wenn X H Α oder X H B, dann X H га v B^π,                          (AE)

(ix) Wenn X H га v B^π und Y H га → E^π und Z H ^rB → E^π, dann X и Y и Z (AB)
H E,

(x) Wenn X H га v B^π und Y H E und Α ∈ Y und Z H E und B ∈ Z, dann X и (AB*)
(Y\ {Α}) и (Z\ {B}) H E,

(xi)  Wenn X H E und Y H г—E und Α ∈ X и Y, dann (X и Y)\{Α} H г—Λ^π ,   (NE)

(xii)  Wenn X H г——E^π, dann X H E,                                       (NB)

(xiii)  Wenn X H [β, ξ, Δ] und β ∉ TTFM(X и {Δ}), dann X H rΛξΔ^π,            (UE)

(xiv)  Wenn X H WA¹, dann X H [θ₀, ξ, Δ],                                   (UB)

(xv)  Wenn X H [θ₀, ξ, Δ], dann X H r√ξΔ^π,                                     (PE)

<<   170   171   172   173   174   175   176   >>

More intriguing information