Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

6.2 Vollstandigkeit des Redehandlungskalkuls 251

(i*) Wenn F(к) = ^rΦ(θo, .., θ, _l)^,, dann G(k+1) = G(k) и {^rΦ(θ'0, ∙., θ'r-ʃ I Fur alle i <
r∙. ^rθi = θ'ɔ ∈ G(k)} U {^rφ(θ*o, ..., θ*s-1) = φ(θ⁺0, ..., θ⁺s-1), I ^rφ(θ*0, ..., θ*s-1), = θ0 und
fur alle i < s: ^rθ*,; = θ⁺,^π ∈ G (k)},

(ii*) Wenn F(k) = ^r-Φ(θo, ..., θr-1),, dann G(k+1) = G(k),

(iii*) Wenn F(k) = ^г—Α^π, dann G(к+1) = G(к) и {A},

(iv*) Wenn F(к) = ^rA л В, dann G(k+1) = G(к) и {A, Β},

(v*) Wenn F(к) = r-(A л Β),, dann G(k+1) = G(к) и { A^l}, falls G(к) и { A^l}
konsistent_H, G (к+1) = G (к) и {^r-₁ Β^π} sonst,

(vi*) Wenn F(к) = га V Β^^l, dann G(k+1) = G(к) и {A}, falls G(к) и {A} konsistentH,
G (к+1) = G (к) и {Β} sonst,

(vii*) Wenn F (к) = r-(A V Β),, dann G (к+1) = G (к) и {A¹, В¹},

(viii*) Wenn F(к) = га → В"¹, dann G(к+1) = G(к) и {— A}, falls G(к) и {Г—A"^l}
konsistentH, G (к+1) = G (к) и {Β} sonst,

(ix*) Wenn F (к) = г—(A → Β),, dann G (к+1) = G (к) и {A, Г— B¹},

(x*) Wenn F(к) = га θ B^π, dann G(к+1) = G(к) и {A, B}, falls G(к) и {A, B}
konsistentH, G(к+1) = G(к) и {Г—Aⁿ Г—в-} sonst,

(xi*) Wenn F(к) = Г—(A θ в)-, dann G(к+1) = G(к) и {A, Г—в-}, falls G(к) и {A,
Г—В-} konsistentH, G (к+1) = G (к) и {Г—A-, Β} sonst,

(xii*) Wenn F(к) = rΛξΔ-, dann G(к+1) = G(к) и {[θ, ξ, Δ] | θ ∈ TTFMH(G(к)) ∩
GTERMH},

(xiii*) Wenn F(к) = ^ΛξΔ-, dann G(к+1) = G(к) и {Г—[α, ξ, Δ]-} fur das α ∈
KONSTNEU mit dem kleinsten Index, fur welches gilt α ∉ TTFMH( G (к)),

(xiv*) Wenn F (к) = r√ξΔ-, dann G (к+1) = G (к) и {[α, ξ, Δ]} fur das α ∈ KONSTNEU
mit dem kleinsten Index, fur welches gilt α ∉ TTFMH( G (к)),

(xv*) Wenn F (к) = г—VξΔ-, dann G (к+1) = G (к) и {Г—[θ, ξ, Δ]- | θ ∈ TTFMH( G (к)) ∩
GTERMH }.

Wenn F (к) ∉ G (к), dann: Wenn F (к) = rθ = θ^^l fur ein θ ∈ GTERMH, dann G (к+1) =
G (к) и {rθ = θ-}, G(к+1) = G (к) sonst.

<<   <   221   222   223   224   225   226   227   >   >>