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 → Γ¹, 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 i < l ≤ 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.