| |
|
Die Grundrechenarten der Arithmetik bilden das erste formale System, das in der Grundschule gelernt wird. Auch die moderne Mathematik wäre ohne ein Formelsystem undenkbar. Mit den Unklarheiten natürlicher Sprachen wäre die exakte Darstellung und Ableitung mathematische Gesetzmäßigkeiten wohl unmöglich.
Ein formales System kann z.B. alle Kleinbuchstaben und das Leerzeichen als Symbole haben. Symbolketten können beliebige Folgen von – sinnvollen und sinnlosen
– Wörtern sein (es geht nur um die Symbole, also Buchstaben). Eine mögliche Symbolkette ist hier:
Verschlüsselungssysteme
er kam sah siegte
Als einzige Regel ersetzt man jeden Buchstaben durch seinen Nachfolger im Alphabet, also a durch b, b durch c und so fort. z wird durch a ersetzt. Aus der obenstehenden Symbolkette wird durch Anwendung der Regel:fs lbn tbi tjfhuf
Dieses System wurde zur Verschlüsselung von Nachrichten eingesetzt, wie es schon in ähnlicher Form von Julius Cäsar verwendet wurde. Zur Entschlüsselung benutzt man ein gleichwertiges formales System, das jeden Buchstaben durch seinen Vorgänger ersetzt:
er kam sah siegteMan kann die Regel auch mehrfach anwenden. Bei zweifacher Anwendung erhält man
gt mco ucj ukgivgDie Verschlüsselungssystem weisen die Merkmale formaler System auf:
Ein berühmtes Beispiel für ein formales System ist das MU Rätsel aus dem Buch Gödel, Escher, Bach:
Die Regeln dürfen in beliebiger Reihenfolge auf eine Symbolkette angewendet werden, auch mehrmals hintereinander.
(Die Lösung des MU-Rätsels wird am Ende des Artikels verraten)
Ein Satz kann wahr oder falsch sein.
{| border="1"
!style="background:#ffdead;" width="10%" align="center" | Symbol
!style="background:#ffdead;"| Beschreibung
|-
| a b c ...
| Symbolfolge. Ein Kleinbuchstabe kann durch eine Symbolfolge ersetzt werden. Gleiche Kleinbuchstaben in einer Folge müssen durch gleiche Symbolfolgen ersetzt werden.
|-
|
| kann ersetzt werden durch. Die Symbolfolge auf der linken Seite kann durch die Folge auf der rechten Seite ersetzt werden, ohne den Wahrheitsgehalt zu ändern. Ebenso kann die rechte Folge durch die linke ersetzt werden.
|-
|wahr falsch
|Symbole für eindeutig wahre und falsche Aussagen
|}
Symbole für Umwandlungsregeln (Beispiel)
Eine Umwandlungsregel könnte dann so aussehen:
{| border="0"
|Schlussregel1:
|.
|}
Dies bedeutet, dass man auf der linken Seite jedes Satzes entfernen oder hinzufügen darf. Umgangssprachlich entspricht dies der doppelten Verneinung:
Schlussregel1: Die Verneinung der Verneinung einer Aussage ist die Aussage selbst
Weitere Umwandlungsregeln sind z.B.
{| border="0"
|Schlussregel2:
|
|-
|Schlussregel3:
|
|-
|Schlussregel4:
|
|-
|Schlussregel5:
|
|-
|Schlussregel6:
|
|-
|Schlussregel7:
|
|-
|
|
|}
Die Punkte deuten an, dass noch viele weitere Umwandlungsregeln definiert werden können. Dies sind die Schlussfolgerungs-Regeln für die formale Logik. Sie können rein formal ohne Bezug zur Bedeutung der Symbole angewendet werden. Damit verhalten sich die Regeln wie Rechenregeln.
Trotzdem wurden die Regeln "sinnvoll" gewählt. Schlussregel3 bedeutet, dass eine wahre Aussage oder eine beliebige Aussage als Gesamtaussage immer wahr ist. Dagegen bedeutet die kompliziertere Schlussregel5 (Folgerung) übersetzt etwa:
Schlussregel5: aus a folgt b kann ersetzt werden durch die Aussage "Verneinung von Aussage a oder Aussage b".
Die Folgerung ist genau dann falsch, wenn a wahr, aber b dennoch falsch ist. Umgekehrt ist sie also wahr, wenn a falsch oder wenn b wahr ist. Dies entspricht formal (lies: nicht a oder b).
Der klassische Satz ex falsum quod libet (aus Falschem folgt Beliebiges) kann formal dargestellt und bewiesen werden. In unserem formalen System lautet er:
Zum Beweis wenden wir die Umformungsregel für die Folgerung an:
Im formalen System lassen sich Axiome durch Symbolfolgen darstellen. Im MU-Rätsel ist MI das Axiom. Mit Hilfe der Umwandlungsregeln lassen sich aus den Axiomen andere Symbolfolgen, also Sätze ableiten. Da sich der Wahrheitswert bei Anwendung dieser Regeln nicht ändert, sind die Sätze dann ebenfalls wahr. Schlussfolgerungs-Regeln, sind beliebige, formale Umformungsregeln für die Symbolketten.
Eine Symbolkette wird als Satz interpretiert. Kennt man eine Folge der Anwendung der Regeln, die einen Satz aus den Axiom-Symbolketten erzeugt, so ist dies der Beweis dieses Satzes.
Ein Satz ist beweisbar, wenn es prinzipiell möglich ist, ihn durch Umwandlung aus den Axiomen zu erzeugen. Das MU-Rätsel fragt nach der Beweisbarkeit des "Satzes" MU.
Symbole sind die Elemente der Menge und das Operatorsymbol. Mit Hilfe der Prädikatenlogik lassen sich Axiome und Sätze formal darstellen und beweisen. Die Prädikatenlogik erweitert die Aussagenlogik um
{| border="1"
!style="background:#ffdead;" width="10%" align="center" | Formales Axiom
!style="background:#ffdead;"| Beschreibung
|-
|
| Für alle a und b gibt es ein c, so dass a mit b multipliziert c ergibt.
|-
|
| Wird das Ergebnis der Multiplikation von a und b anschliessend multipliziert mit c, so erhält man dasselbe wie wenn zunächst b mit c und danach a mit dem Ergebnis multipliziert. Dies gilt für alle a, b, c.
|-
|
| Es existiert ein e, so dass für jedes b gilt: die Multiplikation von e mit b ergibt stets b, ebenso die Multiplikation von b mit e. e heisst neutrales Element.
|-
|
| Für jedes a gibt es ein b, das mit diesem zusammen multipliziert das neutrale Element ergibt.
|}
Darstellung der Axiome der Gruppentheorie mit Hilfe der Prädikatenlogik
Aus den Umwandlungsregeln der Prädikatenlogik lassen sich aus diesen Axiomen die Sätze der Gruppentheorie rein formal ableiten. Eine solche Regel ist z.B.
In der Sprache Pascal kann beispielsweise ein Unterprogramm über
Ein möglicher Ausschnitt der formalen Grammatik zur Syntaxdefinition in erweiterter Backus-Naur-Notation könnte dann sein:
...
procedure_call = identifier '(' actual_parameter_list ')' ';' ;
actual_parameter_list = expression { ',' expression } ;
Ein gegebener Programmtext ist syntaxfehlerfrei, wenn er durch die Umwandlungsregeln der formalen Grammatik auf ein einzelnes Symbol, z.B. program, reduziert werden kann.
Hätte man eine Sprache, die definiert wird durch
Schritt1:
Das MU-Rätsel
Das formale M,I,U-System
Das System besteht aus drei Symbolen‚ M, I und U. Symbolketten können durch die folgenden vier Regeln in andere Ketten verwandelt werden:
x in Regel2 steht für eine beliebige Symbolkette. xx bedeutet die Verdoppelung der Kette, diese wird also zweimal hinterander gesetzt.Das Rätsel
Die Aufgabe kann nicht durch einfaches Erzeugen aller möglichen Symbolketten (Brute Force-Suche) gelöst werden.Aussagen- und Prädikatenlogik
Logiksysteme wie die Aussagenlogik und ihre Erweiterung, die Prädikatenlogik können durch ein formales System definiert werden:Symbole zur Darstellung einer Logik
Die folgende Tabelle gibt Symbole wieder, die zu einer Definition der Aussagenlogik dienen können:
{| border="1"
!style="background:#ffdead;" width="10%" align="center" | Symbol
!style="background:#ffdead;"| Beschreibung
|-
| A B C ...
| Aussage. Eine Aussage wird durch einen Grossbuchstaben repräsentiert.
|-
|
| nicht. Verneinung einer Aussage ist genau dann wahr, wenn A falsch ist, und umgekehrt.
|-
|
| und. Die Gesamtaussage ist genau dann wahr, wenn sowohl A als auch B wahr sind.
|-
|
| oder. Die Gesamtaussage ist genau dann wahr, wenn entweder A oder B oder beide wahr sind.
|-
|
| ist gleichwertig zu. Die Gesamtaussage ist wahr, wenn A und B beide wahr oder beide falsch sind.
|-
|
| aus folgt. Die Folgerung ist falsch, wenn A wahr, aber B dennoch falsch ist. In allen anderen Fällen ist wahr.
|-
|( )
| Klammern. Klammern dienen dazu, die Ausführung einer Operation vor einer anderen zu erzwingen, wenn Unklarheiten bestehen.
|}Symbolfolgen sind Sätze
In formalen Systemen entspricht ein Satz genau einer Folge von Symbolen, also einer Symbolkette, etwa
Übersetzt heisst dies: Die Aussage "A und B" hat denselben Wahrheitswert wie die Verneinung der Aussage "nicht A oder nicht B".Umwandlungsregeln in einer Logik
Symbolfolgen kann man in formalen Systemen über Regeln in andere Symbolfolgen umformen. Zur Definition der zugelassenen Regeln kann man auch ein (einfacheres) formales System verwenden:Beweise
Ein Beweis besteht aus einer Behauptung und einer Schlussfolgerung. Im formalen System wird eine Behauptung b als Symbolfolge dargestellt, ebenso die Schlussfolgerung s. Der Beweis wird geführt, indem der Satz "aus der Behauptung folgt die Schlussfolgerung" in umgewandelt wird:
Beweis des Satzes: Aus Falschem folgt Beliebiges
Beweis:
Nicht falsch ist aber wahr:
Schliesslich ist eine wahre Aussage oder Beliebiges immer war.
Der Satz ist damit formal bewiesen. Der Beweis könnte durch ein Computerprogramm erfolgen, das nur die Symbole kennt und die Schlussregeln anwendet.Axiomensysteme
Axiome sind Sätze, die als wahr vorausgesetzt werden. In Axiomensystemen exisiteren meist nur einige wenige Axiome. Die euklidische Geometrie hat z.B. nur fünf Axiome. Mathematik
Algebra
Die Mathematik bedient sich seit 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 usw. und 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
interpretieren als:
Eine mechanische Regel könnte dann lauten:Gruppentheorie
Ein klassisches Beispiel für ein Axiomensystem in der Mathematik ist die Gruppentheorie. Eine Gruppe lässt sich über einer Menge und einer zugehörigen (Rechen-)Operation bilden. Mathematische Sätze lassen sich allein aus den vier Axiomen der Gruppe gewinnen. Die Sätze gelten dann für alle Mengen mit zugehöriger Operation, deren Eigenschaften sich auf die Gruppenaxiome abbilden lassen.
a, b, c, ... sind Platzhalter für die Elemente der vorgegebenen Menge, das Operatorsymbol. Die Operation wird im Folgenden Multiplikation genannt, obwohl jede beliebige Rechenoperation gemeint sein kann. Dann kann man die Axiome der Gruppentheorie formal so darstellen:
Hier die Übersetzung:Informatik
In der theoretischen Informatik dienen formale Systeme zur exakten Wiedergabe der inneren Logik eines Systems. Formale Sprachen, die aus einem Alphabet von Symbolen und zughörigen Worten als Symbolketten bestehen, sind ein Hilfsmittel hierzu. Die Syntax wird durch eine zugehörige Grammatik festgelegt, über die die Gültigkeit der Worte festgestellt werden kann. Die Semantik des formalen Systems ist damit aber noch nicht eindeutig definiert.Definition der Syntax von Programmiersprachen
Ein Untersuchungsgegenstand hierzu ist die Möglichkeit einer Definition von realen Programmiersprachen über ein formales System. Als Beispiel mag hier der Aufruf von Unterprogrammen mit Parametern dienen. Die Syntax für die Unterprogrammdefinition und den Programmaufruf kann über eine formale Sprache und die zugehörige formale Grammatik definiert werden. PROCEDURE example(A, B: integer; VAR C: result); BEGIN .. END;
definiert und später dann überexample(2*X,Y,W);
aufgerufen werden. procedure_declaration = PROCEDURE name
'(' formal_parameter_list ')' block ';'
block = BEGIN ... END
formal_parameter_list = parameter { ';' parameter } ;
parameter = [ VAR ] name ':' name ;Symbole sind hier procedure_declaration, identifier, formal_parameter_list, aber auch '(', ':', VAR usw. Eine Symbolkette auf der rechten Seite des Gleichheitszeichens wird, falls sie auftritt, durch das Symbol auf der linken Seite ersetzt. Die Symbolkette und damit das ersetzte Symbol kann wiederum Teil einer Symbolkette sein.program = PROGRAM declarations program_block
declarations = { procedure_declaration }
program_block = BEGIN { procedure_call } END '.'
so bestünde ein konkretes Programm nur aus Unterprogramm-Deklarationen und Aufrufen: Das reale ProgrammPROGRAM
PROCEDURE p1(a: integer; b: integer)
BEGIN ... END;
PROCDURE p2(VAR x: integer)
BEGIN ... END;
BEGIN
p1(0,1);
p2(y);
END.könnte man mit obenstehendem (unvollständigen) Grammatikausschnitt reduzieren:PROGRAM
PROCEDURE name(name: name; name: name)
block;
PROCEDURE name(VAR name: name)
block;
BEGIN
name(expression,expression);
name(expression);
END.Schritt2:
PROGRAM
PROCEDURE name(formal_parameter_list)
block;
PROCEDURE name(formal_parameter_list)
block;
BEGIN
name(actual_parameter_list);
name(actual_parameter_list);
END.Schritt3:
PROGRAM
procedure_declaration
procedure_declaration
BEGIN
procedure_call
procedure_call
END.Schritt4:
PROGRAM
declarations
program_block
Schritt5:
program
Das Programm ist damit syntaktisch korrekt. Es ist aber nicht die ganze Logik des Programms überprüft worden:
Diese Eigenschaften werden unter dem Begriff Semantik im Gegensatz zur Syntax zusammengefasst.Linguistik
In der Linguistik werden formale Systeme zur Definition von formalen Sprachen verwendet, deren Symbolbedeutung undefiniert ist und deren Anwendung allein aufgrund der Regeln erfolgt.
Lösung des MU-Rätsels
Die Symbolkette MU kann durch Anwendung der Regeln aus dem ersten Abschnitt des Artikels nicht aus der Kette MI erzeugt werden.Verkürzung und Verlängerung
Der Beweis kann aber nicht innerhalb des M,I,U-Systems geführt werden. Regel1 und Regel2 verlängern eine Kette, Regel3 und Regel4 verkürzen sie dagegen. Eine sehr lange Folge könnte also unter Umständen doch MU ergeben.Eigenschaften beweisbarer Sätze
Zur Lösung kann man die Eigenschaften der beweisbaren Sätze untersuchen. Eine solche Eigenschaft ist die Anzahl der I-Symbole in einer Kette, die ab jetzt I-Wert genannt werden soll. Der I-Wert des Axioms MI ist eins, da I einmal vorkommt. Der I-Wert des Satzes MU ist dagegen null.Eigenschaften des I-Werts
Die Umwandlungsregeln verändern den I-Wert wie folgt:
Den I-Wert kann man aus der Anzahl der Anwendungen von Regel2 und Regel3 berechnen. Der I-Wert des Axioms ist wie gesagt eins. Wendet man Regel2 an, so erhält man einen I-Wert von 2. Wendet man sie nochmals an, so ergibt sich 4,8,16, usw. n-malige Anwendung ergibt also einen I-Wert von . Jede Anwendung von Regel3 verringert den I-Wert eines Satzes um drei, m-malige Anwendung also um . Der I-Wert ist alsoBeweis
Da der zu beweisende Satz MU die I-Zahl null hat, muss die Gleichung
gelöst werden, wobei n und m ganze Zahlen sein müssen. Der Term auf der linken Seite ergibt nur die Zahlen 1, 2, 4, 5, 7, 8, 10, 11, usw. aber niemals 0, 3, 6, usw. Ein I-Wert von Null ist also nicht möglich. Damit ist der Satz MU wie jeder Satz mit dem I-Wert Null nicht beweisbar, die Lösung des Rätsels lautet