Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 173

ft* ∈ RGS∖{0}, so dass VAN(ft*) = VAN(ft⁺) ⊆ VAN(ft)∖{^rα = α^π } und Α, Β ∈
VER(ft*) und K(ft*) = Β. ■

Theorem 4-8. Einfache Substitution eines neuen Parameters fur einen Parameter ist RGS-treu
Wenn ft ∈ RGS, und β* ∈ PAR∖TTSEQ(ft) und β ∈ PAR∖{β*}, dann ist [β*, β, ft] ∈ RGS
und Dom(VERS([β*, β, ft])) = Dom(VERS(ft)).

Beweis: Durch Induktion uber Dom(ft). Sei ft ∈ RGS, und β* ∈ PAR∖TTSEQ(ft) und β
∈ PAR∖{β*} und gelte die Behauptung fur alle k < Dom(ft). Sei Dom(ft) = 0. Dann ist ft
= 0 = [β*, β, ft] und damit [β*, β, ft] ∈ RGS und es ist Dom(VERS([β*, β, ft])) = 0 =
Dom(VERS(ft)). Sei nun 0 < Dom(ft). Dann ist ft ∈ RGS∖{0}. Dann ist mit Theorem 3-6
ft ∈ RGF(ftΓDom(ft)-1). Dann ist nach I.V.:

a) ft* = [β*, β, ftfDom(ft)-1]   ∈ RGS und Dom(VERS(ft*))   =

Dom(VERS(ftf Dom(ft)-1)).

Sodann ergibt sich mit ft ∈ RGF(ftΓDom(ft)-1) mit Definition 3-18, dass ft ∈
AF(ftΓDom(ft)-1) oder ft ∈ SEF(ftΓDom(ft)-1) oder ft ∈ SBF(ftΓDom(ft)-1) oder ft ∈
KEF(ftΓDom(ft)-1) oder ft ∈ KBF(ftβDom(ft)-1) oder ft ∈ BEF(ftΓDom(ft)-1) oder ft ∈
BBF(ftΓDom(ft)-1) oder ft ∈ AEF(ftΓDom(ft)-1) oder ft ∈ ABF(ftΓDom(ft)-1) oder ft ∈
NEF(ftΓDom(ft)-1) oder ft ∈ NBF(ftΓDom(ft)-1) oder ft ∈ UEF(ftβDom(ft)-1) oder ft ∈
UBF(ftΓDom(ft)-1) oder ft ∈ PEF(ftβDom(ft)-1) oder ft ∈ PBF(ftΓDom(ft)-1) oder ft ∈
IEF(ftβDom(ft)-1) oder ft ∈ IBF(ftβDom(ft)-1).

Da sich Operatoren durch die Substitution nicht verandern, gilt nun zunachst:

b) Fur alle i ∈ Dom(ft)-1: A(ft*_i) = [β*, β, A(ft_i)] und ft*_i = ^rΞ [β*, β, A(ft_i)]^π, wobei ft_i
= ^rΞ A(ft_i)^^l, fur ein Ξ ∈ PERF.

Sodann gilt mit β* ∈ PAR∖TTSEQ(ft) und β ∈ PAR∖{β*}:

c) Fur jedes i ∈ Dom(ft): β* ∉ TT(A(ft_i)) und β ∉ TT([β*, β, A(ft_i)]),

da sonst im Gegensatz zur Voraussetzung β* ∈ TTSEQ(ft) oder β = β*. Sodann sei ver-
einbart:

d) ft⁺ = ft* U {(Dom(ft)-1, [β*, β, ftDom(ft)-1])}.

<<   146   147   148   149   150   151   152   >>

More intriguing information