26    1 Zum grammatischen Rahmen

1.2 Substitution

Fur die metalogische Arbeit sind nun Substitutionsbegrifflichkeiten zu etablieren. Dabei
wird die ubliche Substitutionskonzeption eingeschrankt: Die Substituenda durfen nur
atomare Terme sein und von den Substituentia wird Geschlossenheit verlangt. Dies macht
es auch uberflussig, gebundene Umbenennungen vorzunehmen, um Variablenkollisionen
zu verhindern, da die Substituentia eben geschlossen sind. Die Aufgaben, die in vielen
Kalkulen und in der Modelltheorie ublicherweise von freien Variablen ubernommen wer-
den, leisten im Redehandlungskalkul und in der hier entwickelten Modelltheorie die Pa-
rameter - welche geschlossene Terme sind (siehe Definition 1-14). Sodann konnen nicht
nur Terme und Formeln Substitutionsorte sein, sondern auch Satze und Sequenzen (Klau-
sel (ix) und (x) von Definition 1-31).

Definition 1-31. Substitution von geschlossenen Termen fur atomare Terme in Termen, For-
meln, Satzen und Sequenzen⁹

Die Substitution ist eine 3-stellige Funktion auf {<<θ'o, ., θ'_ku>, <θ_o, ., θ_ku>, μ> | k ∈ N∖{0},
<θ'o, ..., θ'k-ɪ) ∈ ^kGTERM, <θo, ..., θk-ɪ) ∈ ^kATERM und μ ∈ TERM ∪ FORM ∪ SATZ ∪
SEQ}. Als Substitutionsoperator wird '[.., .., ..]' verwendet. Die Werte werden wie folgt zuge-
ordnet:

(i)   Wenn θ⁺ ∈ ATERM und θ⁺ = θk-ɪ, dann [<θ'o, ., ‰>, <θo, ., θku>, θ⁺] = θ'k-ɪ,

(ii)   Wenn θ⁺ ∈ ATERM, θ⁺ ≠ θk-ɪ und k = ɪ, dann [<θ'o, ., θ'_fc-₁>, <θo, ., θku>, θ⁺] = θ⁺,

(iii)  Wenn θ⁺ ∈ ATERM, θ⁺ ≠ θk-ɪ und k ≠ ɪ, dann

[<θ'o, ., ‰>, <θo, ., θkU>, θ⁺] = [<θ'o, ., θ'k-2>, <θo, ., θk-2>, θ⁺],

(iv) Wenn ^rφ(θ*_o, ., θ*_l-ι)ⁿ ∈ FTERM, dann

[<θ'o, ., Θ'm>, <θo, ., θku>, ^rφ(θ*o, ., θ*M)η

= ^rφ([<θ'o, ., Θ'm>, <θo, ., θku>, θ*o], ., [<θ'o, ., Θ'm>, <θo, ., θku>, θ*∣)'-

(v) Wenn ^rΦ(θ_o, ., θ_l-∣)^π ∈ AFORM, dann

[<θ'o, ., Θ'm>, <θo, ., θku>, ^rΦ(θ*o, ., θ*M)4

= ^rΦ([<θ'o, ., Θ'm>, <θo, ., θkU>, θ*o], ., [<θ'o, ., Θ'm>, <θo, ., θkU>, "*])■-

(vi) Wenn ^r—Δ^π ∈ JFORM, dann

[<θ'o, ., Θ'_m>, <θo, ., θku>, ' TI = ^r-[<θ'o, ., ‰>, <θo, ., θk-ɔ, ΔΓ,

(vii) Wenn ^r(Δ_o ψ ʌʃ ∈ JFORM, dann

[<θ'o, ., Θ'm>, <θo, ., θkU>, ^r(Δo ψ Δi)-]

= ^r([<θo, ., θ'_jw>, <θo, ., θku>, Δo] ψ [<θ'o, ., ‰>, <θo, ., θkU>, Δ₁]Γ ,

⁹ Es gelte ^XY = {f | f ∈ Pot(X × Y) und f ist Funktion auf X und Ran(f) ⊆ Y}. Fur die Verwendung des
Tupeloperators gelte: <α_o, ., ak,ɪ) = {(i, a_i) | i < k}. Bei der Angabe von Substitutionen werden im Fol-
genden fur t-Tupel einfach deren Werte notiert. Also etwa [θ'_o, θ_o, Δ] statt [<θ'_o>, <θ_o>, Δ].

<<   28   29   30   31   32   33   34   >>

More intriguing information