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 Г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.



More intriguing information

1. Importing Feminist Criticism
2. The name is absent
3. The name is absent
4. Heterogeneity of Investors and Asset Pricing in a Risk-Value World
5. Explaining Growth in Dutch Agriculture: Prices, Public R&D, and Technological Change
6. Backpropagation Artificial Neural Network To Detect Hyperthermic Seizures In Rats
7. The name is absent
8. The name is absent
9. The name is absent
10. Federal Tax-Transfer Policy and Intergovernmental Pre-Commitment