Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie



3.2 Ableitungsbegriff und deduktive Konsequenzschaft 129

Definition 3-8. Adjunktoreinfuhrungsfunktion (AEF)

AEF = {(й, X) | й ∈ SEQ und X = {й' | Es gibt Δ, Г GFORM, so dass
{Δ, Γ}
VER(^) ≠ 0 und й' = й и {(Dom(M rAlso Δ v Г)}}}.

Vgl. Handlungsanleitung 3-8.

Definition 3-9. Adjunktorbeseitigungsfunktion (ABF)

ABF = {(й, X) | й SEQ und X = {й' | Es gibt Β, Δ, Г GFORM, so dass {rB v Δ,
B Γ1, rΓ} VER^) und й' = й U {(Dom(M rAlso Г)}}}.

Vgl. Handlungsanleitung 3-9.

Definition 3-10. Negatoreinfuhrungsfunktion (NEF)

NEF = {(й, X) | й ∈ SEQ und X = {й' | Es gibt Δ, Г GFORM und i, j ∈ Dom($), so dass

(i)     i j,

(ii)   А(йі) = Δ und (i, йг) VANS(M

(iii) A(¾∙) = Г und A‰mw>1) = r-Γ
oder

A() = r-Γund A‰mω)-1) = Г,

(iv) (j, йО ∈ VERS(S),

(v) Es kein l mit il Dom($)-1 gibt, so dass (l, йі) VANS($), und

(vi) й' = й и {(Dom« rAlso -Δ)}}}.

Vgl. Handlungsanleitung 3-10.

Definition 3-11. Negatorbeseitigungsfunktion (NBF)

NBF= {(й, X) | й ∈ SEQ und X = {й' | Es gibt Г GFORM, so dass r--Γ∣ ∈ VER($) und
й' = й и {(Dom($), rAlso Γ)}}}.

Vgl. Handlungsanleitung 3-11.

Definition 3-12. Universalquantoreinfuhrungsfunktion (UEF)

UEF = {(й, X) | й ∈ SEQ und X = {й' | Es gibt β PAR, ξ VAR und Δ FORM, wobei
FV(Δ)
{ξ}, so dass

(i)    [β, ξ, Δ] VER(S),

(ii) β TTFM({Δ} и VAN(£)) und

(iii) й' = й и {(Dom(£), rAlso ΛξΔ)}}}.

Vgl. Handlungsanleitung 3-12.



More intriguing information

1. The name is absent
2. Ongoing Emergence: A Core Concept in Epigenetic Robotics
3. Examining Variations of Prominent Features in Genre Classification
4. Campanile Orchestra
5. The name is absent
6. The name is absent
7. Recognizability of Individual Creative Style Within and Across Domains: Preliminary Studies
8. The name is absent
9. Detecting Multiple Breaks in Financial Market Volatility Dynamics
10. Technological progress, organizational change and the size of the Human Resources Department