Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

128 3 Der Redehandlungskalkul

Definition 3-2. Subjunktoreinfuhrungsfunktion (SEF)

SEF = {(⅛, X) | Й ∈ SEQ und X = {⅛' | Es gibt Δ, Γ ∈ GFORM und i ∈ Dom(⅛), so dass

(ι) A(⅛) = Δ und (i, ⅛) ∈ VANS(M

(ii) A‰m(^1) = Γ,

(iii) Es kein l mit i < l ≤ Dom(⅛)-1 gibt, so dass (l, ⅛_l) ∈ VANS(⅛), und

(iv) ⅛^, = ʃɔ ∪ {(Dom(⅛), ^rAlso Δ → Γ∣)}}}.

Vgl. Handlungsanleitung 3-2.

Definition 3-3. Subjunktorbeseitigungsfunktion (SBF)

SBF = {(⅛ X) | ʃɔ ∈ SEQ und X = {⅛' | Es gibt Δ, Γ ∈ GFORM, so dass {Δ, r∆ → Γ∣} ⊆
VER(Ej) und ⅛^, = Ej ∪ {(Dom(⅛), rAlso Γ∣)}}}.

Vgl. Handlungsanleitung 3-3.

Definition 3-4. Konjunktoreinfuhrungsfunktion (KEF)

KEF = {(⅛ X) | Ej ∈ SEQ und X = {⅛' | Es gibt Δ, Γ ∈ VER(Ej), so dass
⅛' = ⅛ ∪ {(Dom(⅛), rAlso Δ ∧ Γ∣)}}}.

Vgl. Handlungsanleitung 3-4.

Definition 3-5. Konjunktorbeseitigungsfunktion (KBF)

KBF = {(Д X) | Й ∈ SEQ und X = {# | Es gibt Δ, Γ ∈ GFORM, so dass

{r∆ ∧ Γ∣, T ∧ Δ∣} ∩ VER(Ej) ≠ 0 und ⅛' = ⅛ ∪ {(Dom(⅛), rAlso Γ∣)}}}.

Vgl. Handlungsanleitung 3-5.

Definition 3-6. Bisubjunktoreinfuhrungsfunktion (BEF)

BEF = {(⅛ X) | Ej ∈ SEQ und X = {⅛' | Es gibt Δ, Γ ∈ GFORM, so dass {r∆ → Γ∣,
T → Δ∣} ⊆ VER(Ej) und ⅛' = ⅛ ∪ {(Dom(⅛), rAlso Δ θΓ∣)}}}.

Vgl. Handlungsanleitung 3-6.

Definition 3-7. Bisubjunktorbeseitigungsfunktion (BBF)

BBF = {(⅛, X) | Ej ∈ SEQ und X = {⅛' | Es gibt Δ ∈ VER(Ej) und Γ ∈ GFORM, so dass

{r∆ θ Γ∣, T θ Δ∣} ∩ VER(⅛) ≠ 0 und ^' = Й ∪ {(Dom(⅛), rAlso Γ∣)}}}.

Vgl. Handlungsanleitung 3-7.