Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 181

Theorem 4-9. Einfache Substitution eines neuen Parameters fur eine Individuenkonstante ist
RGS-treu

Wenn 3 ∈ RGS, α ∈ KONST und β ∈ PAR∖TTSEQ(3), dann gibt es ein 3⁺ ∈ RGS∖{0}, so
dass

(i) α ∉ TTSEQ(3⁺),

(ii) TTSEQ(3⁺) ⊂ TTSEQ(3) и {β},

(iii) VAN(3) = {[α, β, Β] | Β ∈ VAN(3⁺)} und

(iv) Wenn 3 ≠ 0, dann K(3) = [α, β, K(3⁺)].

Beweis: Sei 3 ∈ RGS, α ∈ KONST und β ∈ PAR∖TTSEQ(3). Sei nun 3⁺ wie folgt defi-
niert:

a) 3⁺ = {(0, ^rAlso β = β")}^[β, α, 3].

Zunachst gelten dann (i) und (ii) und es gilt auch, dass 3⁺ ≠ 0. Fur 3⁺ kann nun mittels
Induktion uber Dom(3) gezeigt werden, dass 3' ∈ RGS und

b) Dom(VERS(3⁺)) = {(l+1 11 ∈ Dom(VERS(3))} и {0}.

Mit a) und b) folgen dann auch (iii) und (iv). Zu (iii): Sei Δ ∈ VAN(3). Dann gibt es ein i
∈ Dom(VERS(3)), so dass 3i = ^rSei Δ^^l. Also ist mit b) i+1 ∈ Dom(VERS(3⁺)) und mit
a) 3⁺i₊₁ = rSei [β, α, Δ]^η. Also ist [β, α, Δ] ∈ VAN(3⁺) und damit [α, β, [β, α, Δ]] ∈ {[α,
β, Β] | Β ∈ VAN(3⁺)}. Nun ist β ∉ TTSEQ(3) und damit β ∉ TT(Δ) und mit Theorem
1-24-(ii) [α, β, [β, α, Δ]] = [α, α, Δ] = Δ. Also Δ ∈ {[α, β, Β] | Β ∈ VAN(3⁺)}. Sei nun Δ
∈ {[α, β, Β] | Β ∈ VAN(3⁺)}. Dann gibt es ein Δ* ∈ VAN(3⁺), so dass Δ = [α, β, Δ*].
Wegen Δ* ∈ VAN(3⁺) gibt es dann mit a) ein i+1 ∈ Dom(VERS(3⁺)) mit 3⁺_i+ι = rSei
Δ*^^l. Nun ist mit b) i ∈ Dom(VERS(3)) und mit a) 3⁺_i+ι = [β, α, 3i] und damit [β, α, 3i]
= rSei Δ*^^l und weiter [α, β, [β, α, 3i]] = [α, β, rSei Δ*^^l ] = rSei [α, β, Δ*]^^l = rSei Δ^^l.
Wie zuvor ist mit Theorem 1-24-(iii) und β ∉ TTSEQ(3) [α, β, [β, α, 3i]] = [α, α, 3i] =
3i und damit 3i = rSei Δ^^l und A(3_i) = Δ. Damit ist Δ ∈ VAN(3). Damit gilt (iii).

Zu (iv): Angenommen 3 ≠ 0. Wegen β ∉ TTSEQ(3) ist mit a) und Theorem 1-24-(ii)
[α, β, K(3⁺)] = [α, β, A(3+Dom(3+)-1)] = [α, β, [β, α, A(3Dom(3+)-2)]] = [α, α, A(3Dom(3+)-2)] =
A(3D_om(₃+)-₂). Nun ist Dom(3⁺) = Dom(3)+1. Damit gilt weiter [α, β, K(3⁺)] =
A(3Dom(3⁺)-2) = A(3Dom(3)-1) = K(3).

Nun zum Induktionsbeweis: Gelten nun 3⁺ ∈ RGS und b) fur alle k < Dom(3). Sei
Dom(3) = 0. Dann ist 3 = 0 = {(l+1 | l ∈ Dom(VERS(3))}. Mit a) und Definition 3-16
ist 3⁺ = {(0, rAlso β = β^π)} ∈ IEF(0) ⊂ RGS. Offenbar gilt Dom(VERS(3⁺)) = {0} =

<<   154   155   156   157   158   159   160   >>

More intriguing information