2.3 Eine Erweiterung des Hintergrundkalküls

Was dem Hintergrundkalkül noch fehlt, bzw. bisher noch nicht verwendet wurde, logisch aber durchaus machbar ist, ist die Möglichkeit, die Ausdrücke des Logikkalküls zu negieren (komplementieren). Dann gibt es in dem Kalkül die Möglichkeit zu kontraponieren, es gilt $( A \Rightarrow B ) \Leftrightarrow ( \overline{B} \Rightarrow \overline{A} )$, wenn $A$ und $B$ Ausdrücke des Objektkalküls sind. Die Kontraposition beruht auf der zweimaligen Anwendung der Transportationsregel von Peirce, die ebenfalls im logischen Hintergrundkalkül gilt.

Setzt man für die Terme des Hintergrundkalküls Formeln der Booleschen Verbände ein, so erhält man $\overline{a \sqsubseteq b}$ oder in anderer Schreibweise $a \not\sqsubseteq b$ und $\overline{a = b}$ bzw. $a \not = b$.

Diese Negation der Booleschen Formeln macht Sinn, denn es ist durchaus legitim, sich Gedanken über die Beziehungen ,,$a$ ist nicht kleiner-gleich $b$`` bzw. ,,$a$ ungleich $b$`` zu machen, bzw. über die Verbindungen zu den unnegierten Beziehungen.

Einige Beispiele sollen nun zeigen, wie diese Technik angewendet werden kann:

Satz 2.32  

Es gilt: $a \sqcup b \not\sqsubseteq 0, a \sqsubseteq 0 ~ \Rightarrow ~ b \not\sqsubseteq 0$.

Beweis: Durch zweimalige Anwendung der Transportationsregel des Hintergrundkalküls auf $a \sqcup b \not\sqsubseteq 0, a \sqsubseteq 0 ~ \Rightarrow ~ b \not\sqsubseteq 0$ erhält man $a \sqsubseteq 0, b \sqsubseteq 0 ~\Rightarrow ~ a \sqcup b \sqsubseteq 0$. Diese Folgerung ergibt sich unmittelbar aus Satz 2.10.

Satz 2.33  

Es gilt: $a \not\sqsubseteq 0 ~ \Rightarrow ~ (a \sqcap b) \sqcup (a \sqcap \overline{b}) \not\sqsubseteq 0$.

Beweis: Durch Kontraposition ergibt sich, daß $a \sqsubseteq 0$ aus $(a \sqcap b) \sqcup (a \sqcap \overline{b}) \sqsubseteq 0$ folgen müßte. Es ist $(a \sqcap b) \sqcup (a \sqcap \overline{b}) \stackr... ...el{\rm (Bem.\ \ref{BEM4})}{=} a \sqcap 1 \stackrel{\rm (Def.\ \ref{DEF5})}{=} a$. Daher folgt aus $(a \sqcap b) \sqcup (a \sqcap \overline{b}) \sqsubseteq 0$ daß gilt: $a \sqsubseteq 0$.

Satz 2.34  

Es gilt: $a \not\sqsubseteq b ~ \Leftrightarrow ~ a \sqcap \overline{b} \not\sqsubseteq 0$.

Beweis: Durch Kontraposition erhält man: $a \sqsubseteq b ~ \Leftrightarrow ~ a \sqcap \overline{b} \sqsubseteq 0$. Das ist bereits in Satz 2.22 bewiesen worden.

Satz 2.35  

Es gilt: $a \sqsubseteq b, a \not\sqsubseteq 0 ~\Rightarrow~ a \sqcap b \not\sqsubseteq 0$.

Beweis: Durch Transportation im Hintergrundkalkül erhält man $a \sqsubseteq b, a \sqcap b \sqsubseteq 0 ~\Rightarrow ~ a \sqsubseteq 0$, was bereits in Satz 2.12 bewiesen wurde.

Sätze, die negierte Beziehungen enthalten, werden also zunächst mittels Kontraposition oder Transportation in Sätze transformiert, die keine solchen negierten Beziehungen enthalten. Diese Sätze können dann mit den üblichen Methoden der Booleschen Verbände behandelt werden.