Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

3.2 Ableitungsbegriff und deduktive Konsequenzschaft 131

Definition 3-17. Identitatsbeseitigungsfunktion (IBF)

IBF = {(Я, X) | Я ∈ SEQ und X = {Я' | Es gibt θo, θɪ ∈ GTERM, ξ ∈ VAR und Δ ∈ FORM,
wobei FV(Δ) ⊆ {ξ}, so dass {^rθ₀ = θ₁^^l, [θ₀, ξ, Δ]} ⊆ VER(⅛) und
Я' = Я ∪ {(Dom(tf), ^rAlso [θ1, ξ, ΔΓ)}}}.

Vgl. Handlungsanleitung 3-17.

Im Folgenden wird nun die Menge der regelgemaβen Sequenzen, RGS (Definition
3-19), und dann das Ableitungspradikat: '.. ist eine Ableitung von .. aus ..' (Definition
3-20) definiert. Dabei soll RGS neben der leeren Sequenz alle und nur die Sequenzen
enthalten, zu denen sich die leere Sequenz nach den Regeln des Kalkuls fortsetzen lasst.
Unter Ruckgriff auf die soeben definierte Annahmefunktion und die soeben definierten
Einfuhrungs- und Beseitigungsfunktionen wird dementsprechend RGS so definiert, dass
RGS die Menge der Sequenzen ist, von denen jede ihrer nicht-leeren Beschrankungen
eine regelgemaβe Fortsetzung der nachst kleineren Beschrankung ist. Dazu wird zunachst
die Funktion RGF definiert:

Definition 3-18. Zuordnung der Menge der regelgemaβen Annahme- und Folgerungsfortset-
zungen einer Sequenz (RGF)

RGF = {(Я, X) | Я ∈ SEQ und X = U{AF(M SEF(⅛), SBF(⅛), KEF(^), KBF^), BEF(^),
BBF(⅛), AEF(⅛), ABF(⅛), NEF(⅛), NBF(⅛), UEF(⅛), UBF(⅛), PEF(⅛),
PBF(tf), IEF(M IBF(⅛)}}.

RGF ist also so definiert, dass ein Autor, der Я ∈ SEQ geauβert hat, Я genau dann zu Я'
fortsetzen darf, wenn Я' ∈ RGF(⅛). Vor der Definition der Menge der regelgemaβen Se-
quenzen, RGS, werden nun zunachst einige Theoreme zu RGF bewiesen.

Theorem 3-1. RGF-Fortsetzungen von Sequenzen sind nicht-leere Sequenzen

Wenn Я ∈ SEQ, dann ist RGF⅛) ⊆ SEQ∖{0}.

Beweis: Sei Я ∈ SEQ. Sei Я' ∈ КЄЕ(Я). Dann gilt Я' ∈ AF^) oder Я' ∈ SEF^) oder
Я' ∈ SBFφ) oder Я' ∈ KEFφ) oder Я' ∈ KBFφ) oder Я' ∈ BEFφ) oder Я' ∈ BBFφ)
oder Я' ∈ AEF^) oder Я' ∈ ABF^) oder Я' ∈ NEF^) oder Я' ∈ NBF^) oder Я' ∈
ІТТ(Я) oder Я' ∈ UBF^) oder Я' ∈ PEF^) oder Я' ∈ PBF^) oder Я' ∈ !БР(Я) oder
Я' ∈ IBF^). Dann ergibt sich aus Definition 3-1 bis Definition 3-17, dass Я' = Я ∪
{(Dom^), ∑)} fur ein Σ ∈ SATZ. In allen Fallen gilt mit Definition 1-23 und Definition
1-24 Я' ∈ SEQ∖{0}. ■

<<   105   106   107   108   109   110   111   >>

More intriguing information