4 Theoreme zur deduktiven Konsequenzschaft

Im Folgenden werden Theoreme zur deduktiven Konsequenzschaft bewiesen, die zum
einen aufzeigen, dass ubliche Eigenschaften wie etwa Reflexivitat, Monotonie, die Abge-
schlossenheit unter Einfuhrung und Beseitigung der Iogischen Operatoren und Transitivi-
tat fur diese gelten und die zum anderen als Vorbereitung auf den Nachweis der Vollstan-
digkeit in Kap. 6.2 dienen. Dazu sind zunachst einige Vorbereitungen zu erbringen (4.1).
Sodann werden die gewunschten Eigenschaften der deduktiven Konsequenzrelation ge-
zeigt (4.2).

4.1 Vorbereitungen

Zunachst werden Vorbereitungen getroffen, um zeigen zu konnen, dass die deduktive
Konsequenzschaft unter SE abgeschlossen ist. Dazu wird zunachst gezeigt, dass es zu
jeder Ableitung ft eine Ableitung ft* mit VAN(ft*) ⊆ VAN(ft) und K(ft*) = K(ft) gibt,
in der keine der angenommenen Aussagen an zwei Stellen verfugbar ist (Theorem 4-1).
Theorem 4-2 zeigt dann, dass es zu jeder Ableitung ft und jedem Γ ∈ GFORM eine Ab-
leitung ft* mit VAN(ft*) ⊆ VAN(ft) und K(ft*) = K(ft) gibt, so dass Γ wenn uberhaupt
nur als letzte Annahme verfugbar ist. Dieses Theorem bildet die Basis fur die Abge-
schlossenheit unter SE.

Die restlichen Theoreme zielen auf die Abgeschlossenheit unter Einfuhrungen und Be-
seitigungen ab, bei denen die Antezedentia der Abgeschlossenheitsklauseln (vgl.
Theorem 4-18) die Form X0 H Α₀, ..., X_n-₁ H Α_n.ι haben. Hier ist es nicht einfach mog-
lich, beliebige Ableitungen einfach zu verketten, da es unter Umstanden durch die Entste-
hung geschlossener Abschnitte oder durch Verletzung von Parameterbedingungen zu
Problemen kommen kann. Daher muss gezeigt werden, dass sich Ableitungen durch die
Hinzufugung von blockierenden Gliedern, die Substitution von Parametern und die mehr-
fache Anwendung von UE und UB so umformen lassen, dass die gewunschten Verket-
tungen moglich sind.

Hierzu wird zunachst gezeigt, dass sich parameterfremde Ableitungen unter Einschub
einer die Entstehung von geschlossenen Abschnitten blockierenden Annahme (Theorem
4-3) miteinander verbinden lassen (Theorem 4-4), wobei die blockierende Annahme wie-
der entfernt werden kann (Theorem 4-7). Sodann wird gezeigt, dass die einfache Substitu-
tion eines neuen Parameter fur einen moglicherweise bereits verwendeten Parameter

<<   130   131   132   133   134   135   136   >>

More intriguing information