Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

k+1. Dann ist [θ*k, ξk, [<θ*0, ., θ*k-1>, <ξo, ., ξk-1>, θ]] = [θ*k, ξk, θ] = θ = [<θ*o, ., θ*k>,
<ξ_o, ..., ξ_k>, θ]. Angenommen ξ_i = θ fur ein i < k. Dann ist ξj ≠ θ fur alle i < j < k+1. Dann
ist [<θ*o, ., θ*k>, <ξo, ., ξk>, θ] = [<θ*o, ., θ*k-₁>, <ξo, ., ξk-1>, θ] = [<θ*0, ., θ*i>, <ξo, .,
ξi>, θ] = θ*i ∈ GTERM. Also [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, θ]] = [θ*k, ξk, θ*i] =
θ*i = [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, θ] = [<θ*o, ., θ*k>, <ξo, ., ξk>, θ]. Angenommen ξk =
θ. Dann ist ξ_iι ≠ θ fur alle i < k und [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, θ] = θ. Also [θ*k, ξk,
[<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, θ]] = [θ*k, ξk, θ] = θ*k = [<θ*o, ., θ*k>, <ξo, ., ξk>, θ].

Gelte die Behauptung nun fur {θ_o, ., θ_r-1} ⊆ TERM und sei θ = ^rφ(θ_o, ., θ_r-1)^π ∈
FTERM. Dann ist [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, θ]] = [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo,
., ξk-1>, ^rφ(θo, ., θr-1)^π ]] = ^rφ([θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, θo]], ., [θ*k, ξk,
[<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, θr-1]])^π. Mit I.V. gilt [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>,
θi]] = [<θ*o, ., θ*k>, <ξo, ., ξk>, θi] fur alle i < r. Also [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, .,
ξk-1>, θ]] = ^rφ([<θ*o, ., θ*k>, <ξo, ., ξk>, θo], ., [<θ*o, ., θ*k>, <ξo, ., ξk>, θr-1])^π = [<θ*o,
., θ*k>, <ξo, ., ξk>, ^rφ(θo, ., θr-1)^π ] = [<θ*o, ., θ*k>, <ξo, ., ξk>, θ].

Zu (ii): Sei Δ ∈ FORM. Der Beweis wird mittels Induktion uber den Formelaufbau von
Δ gefuhrt. Sei Δ = ^rΦ(θ_o, . θ_r-1)^^l ∈ AFORM. Der Fall verlauft analog zum FTERM-Fall
unter Verwendung von (i).

Gelte das Theorem nun fur Δ_o, Δ₁ ∈ FORM. Sei Δ = ^r— Δ_o^^l ∈ JFORM. Dann ist [θ*_k,
ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, Δ]] = [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, ' Δ ]] =
^r-[θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, Mb Mit I.V. gilt [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo,
., ξk-1>, Δo]] = [<θ*o, ., θ*k>, <ξo, ., ξk>, Δo]. Also [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>,
Δ]] = ^r-[<θ*o, ., θ*k>, <ξo, ., ξk>, ΔI = [<θ*o, ., θ*k>, <ξo, ., ξk>, ' Δ I = [<θ*o, .,
θ*_k>, <ξ_o, ., ξ_k>, Δ]. Sei Δ = ^r(Δ_o ψ Δ₁)^^l ∈ JFORM. Der Fall verlauft analog zum Nega-
torfall.

Sei Δ = ^rΠζΔ_o^^l ∈ QFORM. Angenommen ξi = ζ fur ein i < k. Dann ist ξj ≠ ζ fur alle j <
k+1 mit i ≠ j. Dann ist [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, Δ]] = [θ*k, ξk, [<θ*o, .,
θ*k-1>, <ξo, ., ξk-1>, ^r∏ζΔo^π]] = [θ*k, ξk, ^r∏ζ[<θ*o, ., θ*i-1, θ*i+1, ., θ*k-1>, <ξo, ., ξi-1,
ξi+1, ., ξk-1>, Δo]^π] = ^rΠζ[θ*k, ξk, [<θ*o, ., θ*i-1, θ*i+1, ., θ*k-1>, <ξo, ., ξi-1, ξi+1, .,
ξk-1>, Δo]]^π. Mit I.V. gilt [θ*k, ξk, [<θ*o, ., θ*i-1, θ*i+1, ., θ*k-1>, <ξo, ., ξi-1, ξi+1, ., ξk-1>,
Δo]] = [<θ*o, ., θ*i-1, θ*i+1, ., θ*k>, <ξo, ., ξi-1, ξi+1, ., ξk>, Δo]. Also [θ*k, ξk, [<θ*o, .,
θ*k-1>, <ξo, ., ξk-1>, Δ]] = ^rΠζ[<θ*o, ., θ*i-1, θ*i+1, ., θ*k>, <ξo, ., ξi-1, ξi+1, ., ξk>, M =
[<θ*o, ., θ*k>, <ξo, ., ξk>, ^r∏ζΔo^π ] = [<θ*o, ., θ*k>, <ξo, ., ξk>, Δ]. Angenommen ξk = ζ.
Dann ist ξi ≠ ζ fur alle i < k und [θ*k, ξk, [<θ*o, ., θ*k-1>, <ξo, ., ξk-1>, Δ]] = [θ*k, ξk, [<θ*o,

<<   <   45   46   47   48   49   50   51   >   >>