Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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 Г¹)}}}.

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.

<<   104   105   106   107   108   109   110   >>

More intriguing information