Ein formales System ist ein System von Symbolketten und Regeln. Die Regeln sind Vorschriften für die Umwandlung einer Symbolkette in eine andere, also Produktionen einer formalen Grammatik. Die Anwendung der Regeln kann dabei ohne Kenntnis der Bedeutung der Symbole, also rein syntaktisch erfolgen. Formale Systeme werden in verschiedenen wissenschaftlichen Disziplinen wie der Logik, Mathematik, Informatik und Linguistik verwendet, insbesondere um neue Aussagen aus bereits bekanntem Wissen herzuleiten.

Kalkül wird oft in derselben Bedeutung wie formales System verwendet; manchmal wird unter einem Kalkül jedoch ein formales System mit bestimmten Einschränkungen verstanden.

Definition eines formalen Systems

Ein formales System lässt sich als Quadrupel ${\displaystyle F=\langle A,B,AU,R\rangle \quad }$ auffassen, das heißt, es wird von folgenden Bestimmungsstücken konstituiert:

• ${\displaystyle A\quad }$ ist ein Alphabet, das heißt eine Menge beliebiger Zeichen. Dies sind die Grundzeichen, aus denen sich die Symbolketten des formalen Systems zusammensetzen.
• ${\displaystyle B\quad }$ ist eine Teilmenge aller Wörter, die sich über dem Alphabet ${\displaystyle A}$ bilden lassen. Dies sind die „wohlgebildeten“ oder „wohlgeformten Formeln“ (englisch well-formed formulas, wff), also diejenigen unter den Symbolketten, die einen „Sinn“ ergeben. „Sinn ergeben“ bedeutet aber hier nichts anderes, als dass diese Zeichenreihen der Grammatik des formalen Systems entsprechen und deshalb für die weitere Untersuchung zugelassen werden sollen. ${\displaystyle B}$ ist damit eine formale Sprache über dem Alphabet ${\displaystyle A}$. In der Praxis wird die (meist unendliche) Satzmenge ihrerseits durch Formationsregeln festgelegt beziehungsweise induktiv definiert.
• ${\displaystyle AU\quad }$ ist eine Menge von Axiomen. Axiome müssen wffs sein. Das heißt, ${\displaystyle AU}$ muss eine Teilmenge von ${\displaystyle B}$ sein. Im Übrigen ist auch dieser Begriff ganz formal zu verstehen: Axiome sind die – grundsätzlich willkürlich gewählten – Ausgangsformeln für die Ableitungsrelation des formalen Systems.
• ${\displaystyle R\quad }$ ist eine Menge von mindestens zweistelligen Relationen über Wörtern aus ${\displaystyle B}$, durch die eine Ableitungsrelation definiert wird. ${\displaystyle R}$ enthält die Regeln für das Ableiten. Stehen zwei (oder mehr) wffs in einer dieser Relationen zueinander, so ist die letzte aus der oder den vorhergehenden ableitbar. Ausgehend von den Axiomen – die vorab als „ableitbar“ definiert werden – ergibt sich damit eine Menge von – gemäß der Relation ${\displaystyle R}$ – ableitbaren wffs.

Im Hinblick auf die Leistungsfähigkeit formaler Systeme sind vor allem die Axiome und die zuletzt genannte Relation zu betrachten. Durch diese wird die Ableitungsrelation definiert. Sie wird häufig mit ${\displaystyle \vdash }$ symbolisiert. Die Schreibweise ${\displaystyle a\vdash b}$ für zwei Wörter a und b aus der Menge B bedeutet also, dass sich b aus a formal ableiten lässt. Es gibt also eine Folge von Relationen in R, die a und b (möglicherweise unter Verwendung anderer ableitbarer Formeln) miteinander in eine formale Ableitungsbeziehung setzen.

Der Begriff „formales System“ ist sehr allgemein. Es kann gar keine oder auch unendlich viele Axiome geben. Mindestens eine Relation muss vorhanden sein, doch können auch dies unendlich viele sein. Immer gilt aber: Eine wff a gehört genau dann zu den (formal) ableitbaren Formeln, wenn sich eine „umgekehrt baumförmige“ Struktur von Ableitungsregeln angeben lässt, die von Axiomen ausgeht und deren „Stamm“ bei a endet. Hat das formale System keine Axiome, so stehen an den „Blattspitzen“ des Baumes lauter leere Zeichenreihen.

Ein solcher Ableitungsbegriff wird als syntaktisch bezeichnet. Es wird grundsätzlich nicht darauf reflektiert, wofür die ableitbare Formel a steht, sie steht im Prinzip zu keiner denkbaren Welt in Beziehung, hat keine Bedeutung, keine Semantik.

Interessant sind aber natürlich solche formalen Systeme, deren Ableitungsrelation einer semantischen Folgerungsrelation (möglicherweise insbesondere der menschlichen) möglichst nahekommt. D. h., man möchte möglichst alles, was man semantisch folgern kann, auch formal ableiten können. Damit wird jedoch der Rahmen formaler Systeme bereits überschritten. Nähere Informationen hierzu finden sich unter anderem im Artikel Wissensrepräsentation mit Logik.

Kalküle

Gelegentlich findet man für Kalküle die Einschränkung vor, dass die Menge der Relationen in ${\displaystyle R}$ endlich sein muss. Darüber hinaus werden an die Ableitungsrelation von Kalkülen häufig weitergehende Anforderungen gestellt, wie beispielsweise die Erfüllung der Hüllenaxiome und des Endlichkeitsaxioms. Ansonsten wird der Kalkülbegriff meist synonym zum Begriff des formalen Systems verwendet.

Formales System in der Mathematik

Die Mathematik bedient sich von jeher formaler Systeme. Die elementare Algebra, wie man sie in der Schule lernt, ist ein solches System. Sie bedient sich der Zahlen, Rechenzeichen für Addition, Subtraktion, Multiplikation und Division sowie der Buchstaben für Unbekannte. Die Rechenregeln sind die Umformungsregeln, die mechanisch angewendet werden können, wenn man sie einmal eingesehen hat. Beispielsweise kann man die

1. Algebraregel: ${\displaystyle a+0=a}$

interpretieren als

Jeder beliebige Ausdruck a kann um Null vermehrt werden, ohne das Ergebnis zu ändern.

Eine mechanische Regel könnte dann lauten:

Hat man einen Ausdruck „a“, so kann man die Symbolkette „+0“ (unter Beachtung der Klammerregeln) anfügen oder entfernen, ohne das Ergebnis zu ändern.

123+45
7+0
123456+666
1607+
23++56

Literatur

• Douglas R. Hofstadter: Gödel, Escher, Bach, ein endlos geflochtenes Band. DTV 1991, ISBN 3-423-30017-5.
• David Hilbert, W. Ackermann: Grundzüge der theoretischen Logik. 6. Aufl., Springer 1972, ISBN 3-540-05843-5.
• Logische Sprachregeln. Eine Einführung in die Logik. (Gemeinsam mit H. Wessel) - Berlin, 1975, München/Salzburg, 1975, 592 Seiten, ISBN 978-3-7705-1264-5.