Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 175

Nun ist [β*, β, A(^i)] = A(^*i) = ^rVζΔ^π und [β*, β, A(‰)] = Aφ*,+₁) = [β⁺, ζ, Δ]. Da
Operatoren durch die Substitution nicht verandert werden, gilt damit wegen [β*, β, A(⅛i)]
= ^rVζΔ^^l: A(⅛i) = ^rVζΔ^+π fur ein Δ⁺ ∈ FORM, wobei β* ∉ TT(Δ⁺) und FV(Δ⁺) ⊆ {ζ}.
Damit ist ^rVζΔ^π = [β*, β, A(^_i)] = [β*, β, ^rVζΔ^+π] = ^rVζ[β*, β, Δ⁺]^π und somit Δ = [β*, β,
Δ⁺]. Damit gilt wiederum: [β*, β, A(‰)] = [β⁺, ζ, Δ] = [β⁺, ζ, [β*, β, Δ⁺]] und β⁺ ∉
TT([β*, β, Δ⁺]). Sodann gilt β* = β⁺ oder β* ≠ β⁺.

Erster Fall: Sei β* = β⁺. Dann ist β* ∉ TT([β*, β, Δ⁺]) und damit β ∉ TT(Δ⁺). Dann ist
Δ = [β*, β, Δ⁺] = Δ⁺ und wegen β* = β⁺ ist dann [β*, β, A(^_i+ι)] = [β⁺, ζ, Δ] = [β*, ζ, Δ⁺].
Sodann ist β* ∉ TT(Δ⁺) und β* ∉ TT(A(,‰₁)) und damit gilt mit Theorem 1-23 wegen
[β*, β, A(‰)] = [β*, ζ, Δ⁺], dass A(‰) = [β, ζ, Δ⁺]. Ware nun β ∈ TTFM({Δ⁺,
A(‰0_m(⅛)-2)}) oder gabe es ein j ≤ i, so dass β ∈ TT(⅛j). Dann ergabe sich mit b) und β*
= β⁺, dass β⁺ ∈ TTFM({[β*, β, Δ⁺], [β*, β, A(‰>m(⅛>2)]}) oder dass es j ≤ i gabe, so dass
β⁺ ∈ TT(⅛*j). Widerspruch! Also ist A(⅛i) = ^rVζΔ⁺^^l und A(‰₁) = [β, ζ, Δ⁺] und β ∉
TTFM({Δ⁺, A(^Do_m(⅛)_-2)}) und es gibt kein j ≤ i, so dass β ∈ TT(⅛j) und somit insgesamt
£ ∈ PBF(⅛ΓDom(⅛)-1).

Zweiter Fall: Angenommen, β* ≠ β⁺. Dann lassen sich mit β⁺ ∈ TT([β*, β, A(⅛i₊₁)])
und β⁺ ∉ TT([β*, β, A(‰₁)]) zwei Unterfalle unterscheiden. Erster Unterfall: Ange-
nommen β⁺ ∈ TT([β*, β, A(‰₁)]). Dann ist β⁺ ≠ β und damit β ∉ TT(β⁺). Dann ist mit Δ
= [β*, β, Δ⁺] und Theorem 1-25-(ii): [β*, β, A(‰)] = [β⁺, ζ, Δ] = [β⁺, ζ, [β*, β, Δ⁺]] =
[β*, β, [β⁺, ζ, Δ⁺]]. Sodann ist β* ∉ TT(Λ(A ∣)) und wegen β* ≠ β⁺ und β* ∉ TT(Δ⁺)
auch β* ∉ TT([β⁺, ζ, Δ⁺]) und damit mit Theorem 1-20 A(‰₁) = [β⁺, ζ, Δ⁺]. Ware nun β⁺
∈ TTFM({Δ⁺, A(⅛D_om(⅛)_-2)}) oder gabe es ein j ≤ i, so dass β⁺ ∈ TT(A ). Dann ware we-
gen β⁺ ≠ β mit b) auch β⁺ ∈ TTFM({[β*, β, Δ⁺], [β*, β, A‰m_w,₂)]}) oder es gabe j ≤ i,
so dass β⁺ ∈ TT(⅛*j). Widerspruch! Also ist im ersten Unterfall die Parameterbedingung
fur β⁺ auch in ⅛ΓDom(⅛)-1 erfullt und damit wiederum insgesamt A ∈
PBF(⅛ΓDom(⅛)-1).

Zweiter Unterfall: Sei nun β⁺ ∉ TT([β*, β, A(⅛i₊₁)]). Dann gilt mit [β*, β, A(⅛i₊₁)] =
[β⁺, ζ, [β*, β, Δ⁺]], dass ζ ∉ FV([β*, β, Δ⁺]). Dann ist [β*, β, A(‰)] = [β⁺, ζ, [β*, β, Δ⁺]]
= [β*, β, Δ⁺] und damit mit β* ∉ TT(A(‰₁)) ∪ TT(Δ⁺) wiederum mit Theorem 1-20
A(⅛i₊₁) = Δ⁺, wobei mit ζ ∉ FV([β*, β, Δ⁺]) auch ζ ∉ FV(Δ⁺). Sei nun в§ ∈
PAR∖TTSEQ(⅛ΓDom(⅛)-1). Dann gilt mit ζ ∉ FV(Δ⁺), dass A‰) = Δ⁺ = [β≡, ζ, Δ⁺]
und es gilt: в§ ∉ TTFM({Δ⁺, A(‰_om(,⅛)_-2)}) und es gibt kein j ≤ i, so dass в§ ∈ TT(⅛j).

<<   <   148   149   150   151   152   153   154   >   >>