Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

40    1 Zum grammatischen Rahmen

Gelte die Behauptung fur Δ₀, Δ₁ ∈ FORM und sei Δ = ^r-Δ,√ ∈ JFORM. Dann ist [θ*₁,
Θ1, [θ*0, θ0, Δ]] = [θ*1, θ1, [θ*0, θ0, ^r- Δ ]] = ^r-[θ*1, θ1, [θ*0, θ0, Δo]]^π . Mit I.V. gilt [θ*_b
Θ1, [θ*o, θo, Δo]] = [θ*o, θo, [θ*1, θ1, Δo]]. Also [θ*1, θ_b [θ*o, θ0, Δ]] = ^r-[θ*o, θ0, [θ*_b θ_b
Δ Il = [θ*o, θo, [θ*1, θ1, ' Δ ]] = [θ*o, θo, [θ*1, θ1, Δ]]. Sei Δ = ^γ(Δo ψ Δ) ∈ JFORM.
Der Fall verlauft analog zum Negatorfall.

Sei Δ = ^rΠξΔ₀^^l ∈ QFORM. Angenommen ξ = θ₀. Dann ist ξ ≠ θɪ und [θ*ι, θ₁, [θ*₀, θ₀,
Δ]] = [θ*1, θ1, [θ*o, θo, ^r∏ξΔo^π]] = [θ*1, θ1, ^r∏ξΔo^π] = ^rΠξ[θ*1, θ1, ΔoΓ = [θ*o, θo,
^rΠξ[θ*_b θ1, Δo]T] = [θ*o, θo, [θ*1, θ1, FξΔ Ц = [θ*o, θo, [θ*1, θɪ, Δ]]. Angenommen ξ =
θ1. Dann ist ξ ≠ θo und [θ*_b θɪ, [θ*o, θo, Δ]] = [θ*1, θɪ, [θ*o, θo, ^r∏ξΔo^π]] = [θ*1, θɪ,
^rΠξ[θ*0, θo, Δo]^π] = ^rΠξ[θ*0, θo, Δ ] = [θ*0, θo, ^r∏ξΔo^π] = [θ*0, θo, [θ*1, θ1, ^r∏ξΔo^π]] =
[θ*o, θo, [θ*1, θ1, Δ]]. Sei θo ≠ ξ ≠ θ1. Der Fall verlauft analog zum Negatorfall. ■

Theorem 1-26. Substitution in Substitutionsergebnissen

Wenn ζ ∈ VAR, θ', θ* ∈ GTERM und θ⁺ ∈ KONST ∪ PAR, dann:

(i) Wenn θ ∈ TERM, dann [θ', θ⁺, [θ*, ζ, θ]] = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, θ]], und

(ii) Wenn Δ ∈ FORM, dann [θ', θ⁺, [θ*, ζ, Δ]] = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, Δ]].

Beweis: Seien ζ ∈ VAR, θ', θ* ∈ GTERM und θ⁺ ∈ KONST ∪ PAR. Zu (i): Sei θ ∈
TERM. Der Beweis wird mittels Induktion uber den Termaufbau von θ gefuhrt. Sei θ ∈
ATERM. Sei weiter θ ∈ KONST ∪ PAR. Angenommen θ = θ⁺. Dann ist [θ', θ⁺, [θ*, ζ,
θ]] = [θ', θ⁺, θ] = θ'. Nun ist ζ ∉ TT(θ') ∈ GTERM und daher [θ', θ⁺, [θ*, ζ, θ]] = θ' = [[θ',
θ⁺, θ*], ζ, θ'] = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, θ]]. Angenommen θ ≠ θ⁺. Dann ist [θ', θ⁺, [θ*, ζ, θ]]
= [θ', θ⁺, θ] = θ = [[θ', θ⁺, θ*], ζ, θ] = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, θ]]. Sei schlieβlich θ ∈ VAR.
Angenommen θ = ζ. Dann ist [θ', θ⁺, [θ*, ζ, θ]] = [θ', θ⁺, θ*] = [[θ', θ⁺, θ*], ζ, θ] = [[θ', θ⁺,
θ*], ζ, [θ', θ⁺, θ]]. Angenommen θ ≠ ζ. Dann ist [θ', θ⁺, [θ*, ζ, θ]] = [θ', θ⁺, θ] = θ = [[θ',
θ⁺, θ*], ζ, θ] = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, θ]].

Gelte die Behauptung nun fur {θ₀, ., θ_r-1} ⊆ TERM und sei θ = ^rφ(θ₀, ., θ_r-ι)^^l ∈
FTERM. Dann ist [θ', θ⁺, [θ*, ζ, θ]] = [θ', θ⁺, [θ*, ζ, ^rφ(θo, ., θr-₁)^π]] = ^rφ([θ', θ⁺, [θ*, ζ,
θo]], ., [θ', θ⁺, [θ*, ζ, θr-1]])T Mit I.V. gilt [θ', θ⁺, [θ*, ζ, θi]] = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, θi]]
fur alle i < r. Also [θ', θ⁺, [θ*, ζ, θ]] = ^rφ([[θ', θ⁺, θ*], ζ, [θ', θ⁺, θɑ]], ., [[θ', θ⁺, θ*], ζ, [θ',
θ⁺, θr-₁]]Γ = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, ^rφ(θo, ., θr-ʃ]] = [[θ', θ⁺, θ*], ζ, [θ', θ⁺, θ]].

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

<<   <   42   43   44   45   46   47   48   >   >>