Monadische Prädikatenlogik zweiter Stufe

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

Zu einer Signatur $σ$ betrachte die Sprache $L_{I I}^{σ}$ der Prädikatenlogik zweiter Stufe. Die Formeln der MSO sind genau diejenigen $L_{I I}^{σ}$ -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]

Beispiele

Prädikatenlogik erster Stufe

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

Induktionsaxiom

Die Peano-Arithmetik kann bekanntlich mit der Signatur $σ = {0, s}$ beschrieben werden, wobei 0 eine Konstante und $s$ ein Funktionssymbol ist. Die Konstante wird als Nullelement und s als Nachfolger-Funktion interpretiert. Das sogenannte Induktionsaxiom

\forall X ((X 0 \land \forall x (X x \to X s x)) \to \forall x X x)

ist offenbar ein MSO-Satz.

Zusammenhang von Graphen

Ist $σ = {E}$ für ein zweistelliges Relationssymbol $E$ , so ist jede $σ$ -Struktur ein Graph $G$ , wobei das $G$ das Universum, das heißt die Grundmenge, der Struktur ist und die Interpretation $E^{G}$ von $E$ die Kantenrelation auf $G$ ist. Dann ist

\forall X ((\exists x X x \land \exists x \neg X x) \to \exists x \exists y (X x \land \neg X y \land E x y))

ein syntaktisch korrekter MSO-Ausdruck, denn die einzige vorkommende Relationsvariable $X$ ist einstellig. Das zweistellige Relationssymbol $E$ gehört zur Signatur und ist daher keine Relationsvariable. Die Semantik dieses Ausdrucks lautet: Für jede Teilmenge ( $\forall X$ ) gilt: wenn die Teilmenge nicht leer ist ( $\exists x X x$ ) und auch ihr Komplement nicht leer ist ( $\exists x \neg X x$ ), dann gibt es zwischen ihr und ihrem Komplement eine Kante ( $\exists x \exists y (X x \land \neg X y \land E x y))$ ). 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 Elementen

Für $σ = \emptyset$ 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 $X$ gibt und eine bijektive Funktion von $X$ auf ihr Komplement:

\exists X \exists Y (^{″} Y {ist Funktion}^{″} \land^{″} X ist Definitionsbereich von Y^{″} \land^{″} \neg X ist Wertebereich von Y^{″} \land^{″} Y {ist bijektiv}^{″}}

,

wobei klar ist, dass die in Apostrophen eingeschlossenen Teilsätze sogar in der Prädikatenlogik erster Stufe formulierbar sind. Da hier die zweistellige Relationsvariable $Y$ 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

Modelle von Wörtern

Die monadische Prädikatenlogik zweiter Stufe eignet sich zur Formulierung von Aussagen über Wörtern über einem endlichen Alphabet $Σ$ . Dazu verwenden wir als Signatur $σ = {<, P_{a}, P_{b}, \dots}$ , wobei $a, b, \dots$ die Zeichen des Alphabets sind und wir formulieren, dass < eine lineare Ordnung auf dem Universum ist und die $P_{a}, P_{b} \dots$ eine Partition des Universums bilden.

\forall x \neg (x < x) \land \forall x \forall y \forall z (((x < y) \land (y < z)) \to (x < z)) \land \forall x \forall y ((x = y) \lor (x < y) \lor (y < x))

drückt die lineare Ordnung aus, und

\forall x ((P_{a} x \lor P_{b} x \lor P_{c} x) \land \neg (P_{a} x \land P_{b} x) \land \neg (P_{a} x \land P_{c} x) \land \neg (P_{b} x \land P_{c} x))

drückt die Partitionseigenschaft aus.

Ein endliches Universum können wir dann als isomorph zu ${1, 2, \dots, n}$ annehmen, wobei < als die natürliche Ordnung interpretiert wird und $P_{a} i$ als an $i$ -ter Stelle steht ein a, entsprechend für $P_{b} i$ und so weiter.

Ist etwa $Σ = {a, b, c}$ , so definiert das Wort $s = a a b c b c a$ eine ${<, P_{a}, P_{b}, P_{c}}$ -Struktur $M_{s}$ auf dem Universum ${1, 2, 3, 4, 5, 6, 7}$ mit den Interpretationen ${1, 2, 7}$ für $P_{a}$ , ${3, 5}$ für $P_{b}$ , ${2, 4}$ für $P_{c}$ 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 $L_{I I}^{σ}$ -Modelle.

MSO-Definierbarkeit

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

L (Φ) : = {s \in Σ^{*} | M_{s} ⊨ Φ}

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 $Σ = {a, b, c}$ , die eine gerade Anzahl $a$ 's enthält, wie folgt beschreiben:

Φ = \exists X \exists Y (\forall x ((P_{a} x \leftrightarrow (X x \lor Y x)) \land \neg (X x \land Y x))

\land \exists x (X x \land \forall y (y < x \to \neg P_{a} x))

\land \exists x (Y x \land \forall y (x < y \to \neg P_{a} x))

\land \forall x \forall y ((X x \land X y \land x < y) \to \exists z (Y z \land x < z \land z < y))

\land \forall x \forall y ((Y x \land Y y \land x < y) \to \exists z (X z \land x < z \land z < y)))

In Worten bedeutet das

Die

a

's verteilen sich auf zwei Mengen

X

und

Y

, die disjunkt sind,

und das erste

a

liegt in

X

und das letzte

a

liegt in

Y

und zwischen zwei verschiedenen Elementen aus

X

liegt eines aus

Y

und zwischen zwei verschiedenen Elementen aus

Y

liegt eines aus

X

.

Damit ist dann klar, dass $L (Φ)$ genau die die Menge der Zeichenketten ist, die eine gerade Anzahl von $a$ 's enthält, das heißt diese Sprache ist MSO-definierbar.

Satz von Büchi

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

\exists X_{1} \dots \exists X_{n} φ

auskommt, wobei $φ$ ein Ausdruck der Prädikatenlogik erster Stufe in einer um $X_{1}, \dots, X_{n}$ erweiterten Signatur ist. Die Menge dieser Ausdrücke nennt man $M Σ_{1}^{1}$ . Für Sprachen sind daher Regularität, MSO-Definierbarkeit und $M Σ_{1}^{1}$ -Definierbarkeit äquivalent.^[7]

Einzelnachweise

↑ 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

[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 automata, 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

[1]

[2]

[3]

[4]

[5]

[6]

[7]

Monadische Prädikatenlogik zweiter Stufe

Inhaltsverzeichnis

Definition

Beispiele

Prädikatenlogik erster Stufe

Induktionsaxiom

Zusammenhang von Graphen

Gerade Anzahl von Elementen

MSO auf Wörtern

Modelle von Wörtern

MSO-Definierbarkeit

Satz von Büchi

Einzelnachweise

Navigationsmenü

Monadische Prädikatenlogik zweiter Stufe

Definition

Beispiele

Prädikatenlogik erster Stufe

Induktionsaxiom

Zusammenhang von Graphen

Gerade Anzahl von Elementen

MSO auf Wörtern

Modelle von Wörtern

MSO-Definierbarkeit

Satz von Büchi

Einzelnachweise

Navigationsmenü

Suche