2. Der Kalkül BL

Den grundlegenden Kalkül der Begriffslogik gewinnt man nach einem einfachen Rezept:

Man nehme einen Kalkül, der genau der Struktur ,,Boolescher Verband`` entspricht und ergänze ihn durch verallgemeinerte Operationen $\prod$ und $\sum$, deren Regeln denjenigen von Infimum und Supremum in Vollständigen (Booleschen) Verbänden nachgebildet sind; dies ergibt den Kalkül VBV. Sodann gestatte man, daß die Variablen dieses Kalküls nicht nur für Terme, sondern auch für beliebige Formeln (siehe Abschnitt 2.1) stehen dürfen; ergibt BL (=Begriffslogik). Weiter füge man eine sog. Deduktions- und Abtrennungsregel hinzu; ergibt BL$^{\vdash }$.

Der Zusatz des sog. Urteilsprinzips liefert die (volle) Urteilslogik: den Kalkül BL $^{\vdash}_{\rm {u}}$. Dieser entspricht der Aussagen- und Prädikatenlogik (erster Stufe).

Andere Zusätze liefern natürlich andere ,,Abkömmlinge`` des ,,Stamm-Kalküls``. Entsprechend ergibt sich eine andere Hierachie, wenn man statt von VBV von einem anderen Kalkül ausgeht (siehe Abb. 1, die Übersicht, sowie insbesondere Abschitt 2.10 zum Übergang von VBV nach BL die Definition von Beziehungs- und Verknüpfungszeichen).

2.1 Das Vokabular

Es folgt nun zunächst die Beschreibung der sog. ,,Formalen Sprache`` (des ,,Vokabulars``, des ,,Wortschatzes``) für die Kalküle VBV, BL, etc.:

Grundzeichen	a   b   c   ...		Variablen
	A   B   C   ...
	0   1		Konstanten
	$\leq$   =		Beziehungszeichen
	$\overline{~}$   $\cdot$   +   $\prod$   $\sum$		Verknüpfungszeichen

Ausdrücke	Terme
	1. Zeichen des Alphabetes (Variablen und Konstanten), die auch (mehrfach) mit Indizes oder Exponenten (aus dem Alphabet) versehen sein dürfen; (sowie Ausdrücke der Gestalt $a(x)$, $b(x,y)$ etc., wobei $a$, $b$, $x$, $y$ Zeichen des Alphabetes sind.)
	2. Sind $s$ und $t$ Terme, so auch $s \cdot t$ und $s + t$; ist $s$ ein Term, so auch $\overline{s}$, $\prod_{\rm {i}}{s}$ und $\sum_{\rm {i}}{s}$ (i sei eine Variable).

	v-Formeln (=verbandstheoretische Formeln)
	Sind $s$ und $t$ Terme, so sind $s \leq t$ und $s = t$ v-Formeln.

	l-Formeln (=logische Formeln)
	1. wie Terme 1.
	2. Sind $a$ und $b$ l-Formeln, so auch $a \leq b$, $a = b$, $a \cdot b$, $a + b$; ist $a$ eine l-Formel, so auch $\overline{a}$, $\prod_{\rm {i}}{s}$ und $\sum_{\rm {i}}{s}$ (i sei eine Variable).

Die eindeutige Lesbarkeit der Ausdrücke wird nötigenfalls durch Setzen von Klammern gewährleistet.

Zwecks Anwendung der Kalküle darf die Formale Sprache durch geeignete Zeichen(-Kombinationen) erweitert werden, so daß etwa auch    $Hund \leq Tier$,    $a \; ^{\leq}_{\rm {x}}\; b$ (als Abkürzung für   $ax \leq b$) u.ä. zulässige Ausdrücke wären (cf. Computersprache PROLOG). Wir denken uns in einem solchen Falle die Ausdrucks-Definition entsprechend angepaßt.

2.2 Die Axiome

Es folgen die Axiome (=Grundformeln und Grundregeln) für die Kalküle VBV und BL:

(Ableitbare / beweisbare Formeln und Regeln nennen wir Theoreme bzw. Sätze.)

Grundformeln

Grundregeln

VBV, BL

1	$a \leq a$		5	$\begin{array}{c}\infer{a \leq c}{a \leq b & b \leq c}\end{array}$

2	$a \cdot b \leq a$		6	$\begin{array}{c}\infer{a = b}{a \leq b & b \leq a}\end{array}$		$\begin{array}{c}\infer{a \leq b}{a = b}\end{array}$		$\begin{array}{c}\infer{b \leq a}{a = b}\end{array}$
	$a \cdot b \leq b$

3	$a \leq a + b$		7	$\begin{array}{c}\infer{a \leq b \cdot c}{a \leq b & a \leq c}\end{array}$
	$b \leq a + b$

4	$0 \leq a$		8	$\begin{array}{c}\infer{a + b \leq c}{a \leq c & b \leq c}\end{array}$
	$a \leq 1$

			9	$\begin{array}{c}\infer{a \cdot \overline{b} \leq 0}{a \leq b}\end{array}$		$\begin{array}{c}\infer{a \leq \overline{b}}{a \cdot b \leq 0}\end{array}$
				$\begin{array}{c}\infer{a \cdot b \leq 0}{a \leq \overline{b}}\end{array}$		$\begin{array}{c}\infer{a \leq b}{a \cdot \overline{b} \leq 0}\end{array}$

2'

$\begin{array}{c}\displaystyle{\prod_{\rm {i}}{a_{\rm {i}} \; \leq a_{\rm {k}}}}\end{array}$

7'

$\begin{array}{c}\infer[{\rm iNFa}]{a \leq \; \displaystyle{\prod_{\rm {i}}{b_{\rm {i}}}}}{a \leq b_{i}}\end{array}$

3'

$\begin{array}{c}a_{k} \leq \displaystyle{\sum_{\rm {i}}{a_{\rm {i}}}}\end{array}$

8'

$\begin{array}{c}\infer[{\rm iNFb}]{\displaystyle{\sum_{\rm {i}}{a_{\rm {i}}}} \leq b}{a_{i} \leq b}\end{array}$

2''

$\begin{array}{c}\displaystyle{\prod_{\rm {x}}{a(x) \leq a(y)}}\end{array}$

7''

$\begin{array}{c}\infer[{\rm xNFa}]{a \leq \displaystyle{\prod_{\rm {x}}{b(x)}}}{a \leq b(x)}\end{array}$

3''

$\begin{array}{c}a(y) \leq \displaystyle{\sum_{\rm {x}}{a(x)}}\end{array}$

8''

$\begin{array}{c}\infer[{\rm xNFb}]{\displaystyle{\sum_{\rm {x}}{a(x)}} \leq b}{a(x) \leq b}\end{array}$

2.3 Der NF-Kalkül

Es folgt ein Kalkül, der die Bedeutung von ,,$x$ kommt nicht frei in ...  vor`` ($x$NF$\ldots$ ) festlegt:

NF - Kalkül5		$x$, $y$  Variablen;		$a$, $b$ Ausdrücke
$x$NF$0$		$x$NF$a$, $x$NF$b$	$\vdash$	$x$NF$a \leq b$, $x$NF$a = b$,
$x$NF$1$				$x$NF$a \cdot b$, $x$NF$ab$, $x$NF$a + b$
$x$NF $${\prod_{\rm {x}}{a}}$$		$x$NF$a$	$\vdash$	$x$NF$\overline{a}$,
$x$NF $${\sum_{\rm {x}}{a}}$$				$x$NF $${\prod_{\rm {y}}{a}}$$, $x$NF $${\sum_{\rm {y}}{a}}$$

2.4 Bemerkungen zur Axiomatik

1)

Die Axiome wurden einerseits möglichst verbandstheoretisch gewählt, andererseits so, daß sich bei begriffslogischer Deutung möglichst einleuchtende umgangssprachliche Formulierungen ergeben: Eine der Negationsregeln wäre etwa zu lesen ,,Aus 'Kein $a$ ist $b$ bzw. $a$ und $b$ schließen sich aus' ($ab \leq 0$; wegen   $c \leq 0$  $\dashv\vdash$  $c = 0$   auch durch   $ab = 0$   ausdrückbar) ergibt sich 'Alle $a$ sind nicht-$b$'``.

Läßt man eine der vier Negationsregeln (9) weg, so ergibt sich eine schwächere Negation,    $\overline{\overline{a}} \leq a$   ist nicht mehr beweisbar.

2)

,,Bekanntlich`` lassen sich zum Kalkül VBV äquivalente Gleichungskalküle angeben, bei denen dann die Relation $a \leq b$ durch $ab = a$ ausgedrückt werden kann. Man erhielte so etwa einen Kalkül VBA (= Vollständige Boolsche Algebra ) oder einen Kalkül VBR (= Vollständiger Boolscher Ring ). Bei Aufstellung des letzteren wäre zu überlegen, ob man die verbandstheoretische Operation $\sum$ beibehält oder stattdessen als Verallgemeinerung der Ring-Addition $\oplus$ eine andere Operation $\sum{}^{\hspace{-1mm} \oplus}$ einführt.

3)

Greift man aus den Grundregeln und -Formeln von VBV einige heraus, so können Kalküle entstehen, die allgemeineren Strukturen entsprechen, wie etwa Quasi-Ordnung, Halb-Ordnung, Halb-Verband etc.

Auch sind nicht nur Abwandlungen der Negationsregeln von Interesse, sondern auch solche, bei denen etwa die Distributiv-Gesetze nicht mehr gelten (cf. Quanten-Physik) u.ä.

4)

Die Index-Schreibweise bei $\prod$ und $\sum$ wurde speziell für den Vergleich mit der Prädikatenlogik 1. Stufe gewählt (siehe Abschnitte 3.3 und 4). $A_{xy}$   etwa entspricht dann   $A(x,y)$   bzw.   $Axy$   etc.

2.5 Terme

Beim verbandstheoretischen Kalkül VBV (= Vollständiger Boolescher Verband) steht

$a$, $b$, $c$		jeweils für einen beliebigen Term ,
$a_{\rm {i}}$		für einen Term, der (gegebenenfalls) den variablen Index $i$ frei enthält;
$a_{\rm {k}}$		für einen Term, der (gegebenenfalls) den konstanten bzw. variablen Index $k$ frei enthält;
$a(x)$		für einen Term, der (gegebenenfalls) die freie Variable $x$ enthält;
$a(y)$		für einen Term, der (gegebenenfalls) den Term $y$ enthält.

(,,gegebenenfalls`` soll jeweils heißen: Index bzw. Variable brauchen in dem betreffenden Ausdruck überhaupt nicht vorkommen, oder sie kommen nur nicht-frei vor, so daß etwa    $\prod_{\rm {i}}{0\leq 0}$   ein Spezialfall von 2' ist etc.)

Für die logischen Kalküle BL (= Begriffslogik), BL$^{\vdash }$ etc. gilt dasselbe, wenn man statt ,,Term`` überall ,,l-Formel`` sagt.

2.6 Beweise

Zwei Beispiele sollen andeuten, was man unter einem Beweis bzw. einer Ableitung in obigen Kalkülen zu verstehen hat:

$a \leq b, c \leq d \vdash ac \leq bd$

$\infer[7]{ac \leq bd}{\infer[5]{ac \leq b}{\deduce[2]{ac \leq a}{} & a \leq b} & \infer[5]{ac \leq d}{\deduce[2]{ac \leq c}{} & c \leq d}}$

$a_{i} \leq b_{i} \vdash \prod_{\rm {i}}{a_{\rm {i}}} \leq \prod_{\rm {i}}{b_{\rm {i}}}$

$\infer[7' ~~ i{\rm NF}\prod_{i}{a_{i}}]{\prod_{i}{a_{i}} \leq \prod_{i}{b_{i}}}... ...i}} \leq b_{i}}{\deduce[2']{\prod_{i}{a_{i} \leq a_{i}}}{} & a_{i} \leq b_{i}}}$

Dabei ist ,,$A$, $B$, ... $\vdash$ $K$`` zu lesen als: ,,Aus den Prämissen/Annahmen $A$, $B$, ... ist beweisbar/ableitbar (in dem betreffenden Kalkül) die Konklusion $K$``, und zwar unter Verwendung von Grundformeln und -Regeln bzw. bereits bewiesenen Formeln und Regeln dieses Kalküls.

$A$, $B$	$\vdash$  $C$, $D$	steht als Abkürzung für die beiden Beweise
		$A$, $B$  $\vdash$  $C$ und $A$, $B$  $\vdash$  $D$, und
$A$, $B$  $\dashv$	$\vdash$  $C$, $D$	etwa steht entsprechend für einen Beweis in beiden Richtungen. $\vdash$  A bedeutet: Beweisbar nur aus Grund- oder bereits bewiesenen Formeln.

2.7 Sätze

Wichtige Sätze der Kalküle VBV und BL, auf deren Beweis wir hier verzichten:

1)

$ab \leq c$  $\dashv\vdash$   $a \leq \overline{b} + c$

2)

$ab \leq c$  $\dashv\vdash$   $a\overline{c} \leq \overline{b}$

3)

$( ab \leq 0 ) , ( a\overline{b} \leq 0 )$  $\vdash$  $a \leq 0$

2.8 Meta-Kalküle

Die Definitionen der verschiedenen Arten von Kalkül-Ausdrücken lassen sich ihrerseits noch etwas kalkülmäßiger notieren: Man könnte Begriffe wie Var, Konst, Alph, Term etc. einführen und die entsprechenden Definitionen regelartig schreiben, z.B.:

Term($s$),	Term($t$)	$\vdash$   Term($st$), v-Formel($s \leq t$)
	Var($a$)	$\vdash$   Term($a$)    etc.

Ein Kalkül K bestünde dann u.a. aus drei Teilen:

1)

dem ,,Wort``- oder Ausdrucks-Kalkül. Dieser erzeugt alle Ausdrücke (Terme, Formeln etc.) von K;

2)

dem Schluß- oder Beweis-Kalkül, der die in K beweisbaren Formeln und Regeln produziert, sowie

3)

einem oder mehreren Hilfskalkülen, wie NF-Kalkül u.a.

Auf den Wortkalkül stützt sich die (Meta-)Beweismethode der Induktion nach der Länge/Komplexität der Ausdrücke, während sich die Methode der Induktion nach der Länge/Komplexität von Beweisen auf den Beweiskalkül bezieht.

Die Prüfung etwa, ob ein bestimmter Ausdruck ein Term ist, wenn gewisse andere Ausdrücke Terme sind o.ä., verliefe dann ähnlich wie z.B. der Nachweis im Schlußkalkül, daß eine bestimmte Formel aus gewissen Annahmen beweisbar ist etc.

Übrigens könnte man die Ausdrucksdefinitionen, die Axiome und den NF-Kalkül klammerreicher formulieren, etwa so:

Sind $s$ und $t$ Terme, so auch    $( s )\cdot ( t )$,   $( s ) ( t )$,    $( s ) + ( t )$   etc.

Sind $a$ und $b$ l-Formeln, so auch   $(a) \leq (b)$   etc.

$( a ) ( b ) \leq b$;   $a \leq b$,   $a \leq c$  $\vdash$   $a \leq ( b ) ( c )$   etc.

$x$NF$a$, $x$NF$b$  $\vdash$  $x$NF $(a) \leq (b)$, ...  $x$NF$( a ) ( b )$   etc.

Für den Alltagsgebrauch wird dann festgelegt, in welcher Reihenfolge bestimmte Zeichen ,,binden`` bzw. ,,trennen`` und welche Klammern demnach wegfallen können.

2.9 Syntax und Semantik

Es heißt gelegentlich, die Ausdrücke eines Kalküls (,,Syntax``) seien bedeutungslos, es müßte ihnen eine Bedeutung erst mit Hilfe einer ,,Semantik`` oder ,,Modelltheorie`` zugeordnet werden. In einem einfachen Falle ist die Lage etwa folgende:

Man arbeitet mit drei Systemen S$_{\rm {1}}$, S$_{\rm {2}}$ und S$_{\rm {3}}$. S$_{\rm {1}}$ ist voll oder weitgehend formalisiert: der bedeutungslose, syntaktische Kalkül (K$_{\rm {1}}$). S$_{\rm {2}}$ ist weniger, S$_{\rm {3}}$, der Meta-Kalkül, der als Grundlage zum Vergleich von S$_{\rm {1}}$ und S$_{\rm {2}}$ dient, meist am wenigsten formalisiert.

$\underbrace{K_{\rm {1}}~~~~~~~S_{\rm {2}}}_{\textstyle S_{\rm {3}}}$

Den als bedeutungslos angenommenen Ausdrücken von K$_{\rm {1}}$ wird nun vermöge einer homomorphen (d.h. in einem bestimmten Sinne Struktur-erhaltenden) Abbildung (,,Interpretation``) je eine Bedeutung aus dem System S$_{\rm {2}}$ zugeordnet, etwa durch eine Formel der Gestalt h(A) = B o.ä.

Was aber ist mit den Ausdrücken der Systeme S$_{\rm {2}}$ und S$_{\rm {3}}$?

Besitzen sie - weil gar nicht bzw. weniger formal - ,,von Natur aus`` gewisse Bedeutung(en) und bedürfen also keiner besonderen Bedeutungszuordnung?

Man könnte nun versuchen, S$_{\rm {2}}$ und S$_{\rm {3}}$ ihrerseits (weitgehend) zu formalisieren. Gesetzt, das sei gelungen, so ergibt sich genau genommen:

Es werden zwei Kalküle K$_{\rm {1}}$ und K$_{\rm {2}}$ auf dem Hintergrund eines Meta-Kalküls K$_{\rm {3}}$ miteinander verglichen.

Letzterer ist meist ziemlich stark, umfaßt Aussagen- und Prädikatenlogik nahezu beliebiger Stufe, Vollständige Induktion, Mengenlehre u.ä.

Ein Beispiel mag dieses illustrieren:

K$_{\rm {1}}$ sei ein (syntaktischer) aussagenlogischer Formalismus; S$_{\rm {2}}$, die zugehörige Semantik, sei gegeben durch den Apparat der ,,Wahrheitstafeln`` oder die zweielementige Boolesche Algebra über $\{0,1\}$.

Wir denken uns nun S$_{\rm {2}}$ hinreichend kalkülisiert durch K$_{\rm {2}}$ (etwa einen Gleichungskalkül) und ebenso S$_{\rm {3}}$ durch K$_{\rm {3}}$.

Die bekannten Sätze über die semantische Widerspruchsfreiheit und Vollständigkeit der Aussagenlogik scheinen nun folgende Beweise zu erfordern:

Widerspruchsfreiheit:	$\vdash_{K_{\rm {3}}}$  ( $\vdash_{K_{\rm {1}}}$ $A$ $\longrightarrow$  $\vdash_{K_{\rm {2}}}$ $h(A)$ = T (bzw. =$1$))
Vollständigkeit:	$\vdash_{K_{\rm {3}}}$  ( $\vdash_{K_{\rm {1}}}$ $A$ $\longleftarrow$  $\vdash_{K_{\rm {2}}}$ $h(A)$ = T (bzw. =$1$))

Genaugenommen wurden hier lediglich die Kalküle K$_{\rm {1}}$ und K$_{\rm {2}}$ miteinander verglichen und als in einem bestimmten Sinne äquivalent (siehe Abschnitt 4) erwiesen. (Es kann im allgemeinen Fall übrigens auch vorkommen, daß der ,,Urbild-Kalkül`` schwächer ist als der ,,Bild-Kalkül``; man spricht dann von Unvollständigkeit.)

Es scheint also nicht zu gelingen, die Zeichenebene, die ,,Welt der Kalküle`` zu verlassen, um die ,,Bedeutungen selbst`` zu erreichen. In diesem Zusammenhang könnte man noch fragen, ob der Kalkül K$_{\rm {2}}$ ein reiner Gleichungskalkül sein kann oder ob man nicht Teile der Aussagenlogik, also des Kalküls K$_{\rm {1}}$, wie etwa die Negation u.a. zu seinem Funktionieren benötigt.

Auch wird auf dem Hintergrund der soeben skizzierten Ansicht der gelegentlich behauptete Vorrang der semantischen vor der syntaktischen Darstellung (der Aussagenlogik) zweifelhaft.

Weiterhin ließe sich im Sinne obiger Sichtweise nach der syntaktischen Widerspruchsfreiheit von K$_{\rm {1}}$ und K$_{\rm {2}}$ fragen (also nach der Unmöglichkeit von   $\vdash$  $A$,   $\vdash$  $\neg A$).

Gesetzt, sie sei bewiesen, dann fragt sich weiter, mit welchen Beweis-Mitteln?

Nach Voraussetzung mit den Mitteln von K$_{\rm {3}}$.

K$_{\rm {3}}$ jedoch ist beträchtlich stärker als etwa K$_{\rm {1}}$, und so hätte man die Widerspruchsfreiheit des schwächeren, also weniger der Widersprüchlichkeit verdächtigen Kalküls mit den Mitteln des stärkeren, also eher verdächtigen bewiesen (cf. auch Gödels Zweiten Satz).

Wie aber beweist man die Widerspruchsfreiheit von K$_{\rm {3}}$ etc. ?

Und was bedeuten all solche Beweise, was zeigen sie ,,eigentlich``?

In den üblichen Darstellungen sind semantisches (S$_{\rm {2}}$) und Meta-System (S$_{\rm {3}}$) i.a. - soweit ich sehe - halbformal und werden anscheinend als ,,unbedenklich`` betrachtet.

2.10 Logische- und Nicht-logische Kalküle

Vor dem weiteren Ausbau der Kalküle VBV und BL wollen wir noch der Frage nachgehen, ob man ohne Rückgriff auf irgendeine Deutung rein Kalkül-intern Beziehungszeichen von Verknüpfungszeichen unterscheiden kann.

Hierbei hilft folgende Beobachtung weiter: In einem (halbformalen) arithmetischen Beweis wird man nie Ausdrücke der Gestalt   $a + b$,   $a \cdot b$   o.ä. allein antreffen, wohl aber solche der Form   $a = b$   zum Beispiel. Andererseits kommen etwa Ausdrücke der Gestalt   $a = ( b = c )$   überhaupt nicht vor. Dies ,,legt`` folgende Definition ,,nahe``:

1)

Ein Zeichen B ist (innerhalb eines Kalküls K) ein Beziehungszeichen (Relationszeichen), wenn eine Formel der Gestalt   xBy   bzw.   By   (o.ä. bei Suffix-, Superfix-, Circumfix- oder anderer Notation) als selbstständiges Glied eines Beweises im Kalkül K auftreten kann.

2)

Ein Zeichen V ist (innerhalb eines Kalküls K) ein Verknüpfungszeichen (Operationszeichen), wenn es in einer Formel der Gestalt   xBy   bzw.   By   innerhalb von x oder y auftreten kann, wobei B ein Beziehungszeichen ist. (Klammern, Variablen, Konstanten seien hier ausgeschlossen.)

Der Leser möge nun folgendes nachprüfen:

1)

In VBV und BL sind   $\leq$   und   $=$   Beziehungszeichen im Sinne dieser Definitionen; $\overline{~}$, $\cdot$, $+$, $\prod$, $\sum$  sind entsprechend Verknüpfungszeichen.

2)

Obwohl obige Definitionen den Fall zulassen, daß ein Zeichen sowohl Beziehungs- als auch Verknüpfungszeichen ist, herrscht in VBV eine strenge Trennung: Kein Beziehungszeichen ist Verknüpfungszeichen und umgekehrt.

Für (noch-)nichtlogische Kalküle scheint eine solche Trennung charakteristisch zu sein (cf. die Unterscheidung von v-Formeln und l-Formeln).

3)

Beim Kalkül BL dagegen sind   $\leq$   und   $=$   zugleich auch Verknüpfungszeichen; z.B. ist hier    $( a \leq b ) \leq ( a \leq b )$   beweisbar.

Dies entspricht dem Umstand, daß in der Logik die Beziehung von Grundobjekten wiederum ein Grundobjekt ist, d.h. die Beziehung von Begriffen ist wieder ein Begriff, die Beziehung von Urteilen ist wieder ein Urteil. Dagegen ist z.B. die Beziehung etwa zweier Zahlen keine Zahl.

4)

Je mehr man sich der Urteilslogik (Abschnitt 3.3) nähert, desto mehr Verknüpfungszeichen werden zu Beziehungszeichen (z.B. die Negation - im Kalkül BL$^{\vdash }$) bis schließlich alle Verknüpfungszeichen zu Beziehungszeichen geworden sind.

D.h. obige Definition bietet eine Handhabe zur Unterscheidung von (noch-)nichtlogischen und logischen, sowie von begriffs- und urteilslogischen Kalkülen auf rein syntaktischer Ebene.