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. The name is absent
2. The name is absent
3. The name is absent
4. The name is absent
5. Gerontocracy in Motion? – European Cross-Country Evidence on the Labor Market Consequences of Population Ageing
6. The name is absent
7. Orientation discrimination in WS 2
8. AGRICULTURAL TRADE IN THE URUGUAY ROUND: INTO FINAL BATTLE
9. Assessing Economic Complexity with Input-Output Based Measures
10. Draft of paper published in: