2.2 Bemerkungen zum Hintergrundkalkül

Ganz unwillkürlich sind in den vorherigen Abschnitten Schlüsse gezogen worden, Ausdrücke für andere eingesetzt, und anderes, über das man eigentlich reflektieren müßte. Im Hintergrund steht offenbar ein weiterer Kalkül, in den die Verbandstheorie eingebettet ist. Dieser Kalkül wird aber teilweise nur in umgangssprachlicher Form benutzt.

Da gibt es Zeichen, wie z.B. $\Leftrightarrow$, $\Rightarrow$, $\Leftarrow$, ,,,``, $\wedge$, $\forall$, aber auch Formulierungen wie z.B. ,,Wenn ...dann ...``, ,,...genau dann, wenn ...``, ,,und``, ,,für alle``, ,,es gibt``, usw.

Und da gibt es offenbar einige Regeln, nach denen geschlossen wird. Im allgemeinen nennt man soetwas ,,Logik``. In späteren Kapiteln werden wir sehen, daß die Grundlage der bedeutenden Logiken ebenfalls Boolesche Verbände sind. D.h., wenn man es genau nimmt, dann haben wir Sätze der Verbände/Booleschen Verbände mit Hilfe von Sätzen der Booleschen Verbände bewiesen. Die Konsequenzen dieser Tatsache überschreiten jedenfalls die Vorgaben dieser Arbeit, und werden demzufolge nicht weiter behandelt, man sollte sich ihrer aber bewußt sein.

In einem Beweis ist vollständige Induktion verwendet worden, in einem anderen wurde ein Ergebnis der Kombinatorik verwendet. Insgesamt scheint dieser logische Hintergrundkalkül sehr stark zu sein, stärker jedenfalls als die Verbandstheorie.

Eines ist auffällig: Der Boolesche Gleichungskalkül ( Axiome V1 - V4 + Zusätze ) verfügt über keine explizit aufgeschriebenen Grundregeln, nur über Grundformeln. Ununterbrochen wird allerdings zumindest eine Regel angewendet, nämlich die Einsetzungs- oder auch Substitutionsregel. Die über den Gleichheitszeichen gesetzten Anmerkungen in den vorherigen Abschnitten bedeuten daher auch nur, daß die jeweilige Formel bei der Anwendung der Einsetzungs regel verwendet wurde. Diese Regel erlaubt es, beide Seiten einer Gleichung wechselseitig und füreinander in andere Gleichungen einzusetzen. Die Einsetzungsregel läßt sich so formulieren:

Sei $G$ eine Formel in der der Term $A$ vorkommt. Weiß man außerdem noch $A = B$, oder $B = A$ (Bem. 2.1), so darf man auch die Gleichung $G'$ schreiben, in der (mindestens) ein Vorkommen von $A$ durch $B$ ersetzt worden ist.

Im Booleschen Gleichungskalkül BV$^{=}$ ist diese Regel in ihrer allgemeinen Form nicht zu formulieren, sie ist im Hintergrundkalkül eingebettet. Sie hätte aber für den im letzten Abschnitt vorgenommenen Vergleich von Gleichungskalkül und Halbordnungskalkül im Halbordnungskalkül bewiesen werden müssen, wenn man annimmt, daß sie nicht auch im Hintergrund von BV $^{\sqsubseteq}$ zur Verfügung steht. Das könnte man annehmen, denn sie wurde für die bisherigen Beweise im Kalkül BV $^{\sqsubseteq}$ nicht benutzt.

Tatsächlich wird die Substitutionsregel aber meistens zum axiomatischen Hintergrund jedes dieser Kalküle gehörig betrachtet, obwohl ein Beweis der Regel für den Halbordnungskalkül (zuzgl. einiger formaler Erweiterungen, sowie vollständiger Induktion) möglich ist. Dieser Beweis findet sich erst in Abschnitt 4.1.2.