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