Die monadische Prädikatenlogik zweiter Stufe, nach dem englischen monadic second order logic auch kurz MSO genannt, ist ein Begriff aus dem Bereich der mathematischen Logik. Es handelt sich um dasjenige Fragment der Prädikatenlogik zweiter Stufe, das nur die einstelligen Prädikate betrachtet.
Definition Bearbeiten
Zu einer Signatur betrachte die Sprache der Prädikatenlogik zweiter Stufe. Die Formeln der MSO sind genau diejenigen -Formeln, bei denen alle vorkommenden Relationsvariablen einstellig sind. Damit ist die Syntax der MSO beschrieben. Die Semantik ist die Einschränkung der Semantik der Prädikatenlogik zweiter Ordnung.
Beachte, dass durchaus mehrstellige Relationen in der MSO vorkommen können, nur müssen diese dann Bestandteil der Signatur sein. Über diese kann nicht quantifiziert werden.
Da einstellige Relationen in jeder Interpretation Teilmengen der Grundmenge sind, kann man in der MSO also Aussagen über alle Teilmengen der zugehörigen -Strukturen aufstellen und über diese beliebig quantifizieren. Man kann nicht über Funktionssymbole oder mehrstellige Relationssymbole quantifizieren.
Beispiele Bearbeiten
Prädikatenlogik erster Stufe Bearbeiten
Jeder Ausdruck der Prädikatenlogik erster Stufe ist ein MSO-Ausdruck, denn ein solcher enthält überhaupt keine Relationsvariablen, insbesondere also keine mehrstelligen.
Induktionsaxiom Bearbeiten
Die Peano-Arithmetik kann bekanntlich mit der Signatur beschrieben werden, wobei 0 eine Konstante und ein Funktionssymbol ist. Die Konstante wird als Nullelement und s als Nachfolger-Funktion interpretiert. Das sogenannte Induktionsaxiom
ist offenbar ein MSO-Satz.
Zusammenhang von Graphen Bearbeiten
Ist für ein zweistelliges Relationssymbol , so ist jede -Struktur ein Graph , wobei das das Universum, das heißt die Grundmenge, der Struktur ist und die Interpretation von die Kantenrelation auf ist. Dann ist
ein syntaktisch korrekter MSO-Ausdruck, denn die einzige vorkommende Relationsvariable ist einstellig. Das zweistellige Relationssymbol gehört zur Signatur und ist daher keine Relationsvariable. Die Semantik dieses Ausdrucks lautet: Für jede Teilmenge () gilt: wenn die Teilmenge nicht leer ist () und auch ihr Komplement nicht leer ist (), dann gibt es zwischen ihr und ihrem Komplement eine Kante (). Das ist offenbar äquivalent zum Zusammenhang des Graphen und wir halten fest, dass man in der MSO den Zusammenhang von Graphen beschreiben kann. In der Prädikatenlogik erster Stufe ist das nicht möglich, siehe Lokalität (Logik), so dass sich MSO durch dieses Beispiel als echt ausdrucksstärker erweist.
Gerade Anzahl von Elementen Bearbeiten
Für gibt es keinen MSO-Satz, der auf einer als endlich vorausgesetzten Menge ausdrückt, dass diese geradzahlig ist. In der Prädikatenlogik zweiter Stufe ist das aber möglich, indem man zum Beispiel ausdrückt, dass es eine Teilmenge gibt und eine bijektive Funktion von auf ihr Komplement:
wobei klar ist, dass die in Apostrophen eingeschlossenen Teilsätze sogar in der Prädikatenlogik erster Stufe formulierbar sind. Da hier die zweistellige Relationsvariable verwendet wird, handelt es sich nicht um einen MSO-Satz. Dieses Beispiel zeigt, dass die Prädikatenlogik zweiter Stufe echt ausdrucksstärker als MSO ist.
MSO auf Wörtern Bearbeiten
Modelle von Wörtern Bearbeiten
Die monadische Prädikatenlogik zweiter Stufe eignet sich zur Formulierung von Aussagen über Wörtern über einem endlichen Alphabet . Dazu verwenden wir als Signatur , wobei die Zeichen des Alphabets sind und wir formulieren, dass < eine lineare Ordnung auf dem Universum ist und die eine Partition des Universums bilden.
drückt die lineare Ordnung aus, und
drückt die Partitionseigenschaft aus.
Ein endliches Universum können wir dann als isomorph zu annehmen, wobei < als die natürliche Ordnung interpretiert wird und als an -ter Stelle steht ein a, entsprechend für und so weiter.
Ist etwa , so definiert das Wort eine -Struktur auf dem Universum mit den Interpretationen für , für , für und der natürlichen Ordnung für <. Die Wörter aus , das heißt die endlichen Zeichenketten über dem Alphabet , sind in diesem Sinne genau die -Modelle.
MSO-Definierbarkeit Bearbeiten
Man kann nun mittels MSO-Ausdrücken Teilmengen solcher Zeichenketten beschreiben. Ist ein MSO-Satz, das heißt eine MSO-Formel ohne freie Variablen, so ist
die Menge (Sprache) aller Wörter, die Modell für sind, das heißt die erfüllen. Eine Sprache dieser Form heißt MSO-definierbar.
So können wir zum Beispiel die Sprache aller Zeichenketten über , die eine gerade Anzahl 's enthält, wie folgt beschreiben:
In Worten bedeutet das
Damit ist dann klar, dass genau die die Menge der Zeichenketten ist, die eine gerade Anzahl von 's enthält, das heißt diese Sprache ist MSO-definierbar.
Satz von Büchi Bearbeiten
Der Satz von Büchi, benannt nach Julius Richard Büchi, gibt Auskunft darüber, welche Sprachen MSO-definierbar sind:
- Eine Sprache ist genau dann MSO-definierbar, wenn sie regulär ist.
Dieser aus dem Jahre 1960 stammende Satz stellt somit eine sehr frühe Verbindung zwischen mathematischer Logik und theoretischer Informatik her, er gilt als erstes Resultat der deskriptiven Komplexitätstheorie. Der Satz wurde unabhängig auch von Boris Trakhtenbrot gefunden.
Eine Analyse des Beweises zeigt, dass man sogar mit MSO-Ausdrücken der Art
auskommt, wobei ein Ausdruck der Prädikatenlogik erster Stufe in einer um erweiterten Signatur ist. Die Menge dieser Ausdrücke nennt man . Für Sprachen sind daher Regularität, MSO-Definierbarkeit und -Definierbarkeit äquivalent.
Einzelnachweise Bearbeiten
- Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory, Springer-Verlag 1999, ISBN 3-540-28787-6, Kapitel 3.1: Second-Order Logic
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Satz 7.14 für eine genauere Aussage
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Satz 7.12
- J. R. Büchi: Weak second-order arithmetic and finite automata, Zeitschrift für mathematische Logik und Grundlagen der Mathematik (1960), Band 6, Seiten 66–92
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Satz 7.21
- B. Trahtenbrot: Finite automata and the logic of monadic predicates (russisch), Sibirskij Mat. Zhurnal (1962), Band 3, Seiten 103–131
- Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory, Springer Verlag 1999, ISBN 3-540-28787-6, Satz 6.2.3