130 3 Der Redehandlungskalkul
Definition 3-13. Universalquantorbeseitigungsfunktion (UBF)
UBF = {(й, X) | й ∈ SEQ und X = {й' | Es gibt θ ∈ GTERM, ξ ∈ VAR und Δ ∈ FORM,
wobei FV(Δ) ⊆ {ξ}, so dass rΛξΔπ ∈ VER(⅛) und й' = й ∪ {(Dom(φ),
rAlso [θ, ξ, ΔΓ)}}}.
Vgl. Handlungsanleitung 3-13.
Definition 3-14. Partikularquantoreinfuhrungsfunktion (PEF)
PEF = {(й, X) | й ∈ SEQ und X = {й' | Es gibt ξ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξ},
und θ ∈ GTERM, so dass [θ, ξ, Δ] ∈ VER⅛) und й' = й ∪ {(Dom^), rAlso
VξΔπ)}}}.
Vgl. Handlungsanleitung 3-14.
Definition 3-15. Partikularquantorbeseitigungsfunktion (PBF)
PBF = {(й, X) | й ∈ SEQ und X = {й' | Es gibt β ∈ PAR, ξ ∈ VAR, Δ ∈ FORM, wobei
FV(Δ) ⊆ {ξ}, Γ ∈ GFORM und i ∈ Dom^), so dass
(i) А(йі) = ' V -\ ■ und (i, йг) ∈ VERS(S),
(ii) A‰) = [β, ξ, Δ] und (i+1, йг+1) ∈ VANS(S),
(iii) A‰mtt>>1) = Г,
(iv) β ∉ TTFM({Δ, Г}),
(v) Es kein j ≤ i gibt, so dass β ∈ TT(Sj),
(vi) Es kein m mit i+1 < m ≤ Dom^)-1 gibt, so dass (m, Sm) ∈ VANS(S), und
(vii) й' = й ∪ {(Dom(S), rAlso Г1)}}}.
Vgl. Handlungsanleitung 3-15.
Definition 3-16. Identitatseinfuhrungsfunktion (IEF)
IEF = {(й, X) | й ∈ SEQ und X = {й' | Es gibt θ ∈ GTERM, so dass
й' = й ∪ {(Domφ), rAlso θ = θπ)}}}.
Vgl. Handlungsanleitung 3-16. Da die Menge der geschlossenen Terme nicht leer ist,
ergibt sich als Korollar, dass wie AF(^) auch IEF(^) fur keine Sequenz й leer ist. Dieser
Sachverhalt schlagt sich weiter unten in Theorem 3-2 nieder.