Monadische Prädikatenlogik zweiter Stufe

Begriff aus dem Bereich der mathematischen Logik

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.

DefinitionBearbeiten

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.[1]

BeispieleBearbeiten

Prädikatenlogik erster StufeBearbeiten

Jeder Ausdruck der Prädikatenlogik erster Stufe ist ein MSO-Ausdruck, denn ein solcher enthält überhaupt keine Relationsvariablen, insbesondere also keine mehrstelligen.

InduktionsaxiomBearbeiten

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 GraphenBearbeiten

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.[2] 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 ElementenBearbeiten

Für   gibt es keinen MSO-Satz, der auf einer als endlich vorausgesetzten Menge ausdrückt, dass diese geradzahlig ist.[3] 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örternBearbeiten

Modelle von WörternBearbeiten

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-DefinierbarkeitBearbeiten

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

Die  's verteilen sich auf zwei Mengen   und  , die disjunkt sind,
und das erste   liegt in  
und das letzte   liegt in  
und zwischen zwei verschiedenen Elementen aus   liegt eines aus  
und zwischen zwei verschiedenen Elementen aus   liegt eines aus  .

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üchiBearbeiten

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.[4][5]

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.[6]

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.[7]

EinzelnachweiseBearbeiten

  1. Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory, Springer-Verlag 1999, ISBN 3-540-28787-6, Kapitel 3.1: Second-Order Logic
  2. Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Satz 7.14 für eine genauere Aussage
  3. Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Satz 7.12
  4. J. R. Büchi: Weak second-order arithmetic and finite automota, Zeitschrift für mathematische Logik und Grundlagen der Mathematik (1960), Band 6, Seiten 66–92
  5. Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Satz 7.21
  6. B. Trahtenbrot: Finite automata and the logic of monadic predicates (russisch), Sibirskij Mat. Zhurnal (1962), Band 3, Seiten 103–131
  7. Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory, Springer Verlag 1999, ISBN 3-540-28787-6, Satz 6.2.3