Lokalität ist ein Begriff aus der mathematischen Logik, mit dem Grenzen der Ausdrucksstärke gewisser Logiken aufgezeigt werden können. Die Grundidee besteht darin, dass gewisse Logiken wie die Prädikatenlogik erster Stufe nur lokale Eigenschaften von Strukturen beschreiben können, aber andere Eigenschaften solcher Strukturen diese Lokalitätseigenschaft nicht haben, letztere sind also nicht in dieser Logik formulierbar. Man unterscheidet zwei Arten von Lokalität, die nach William Hanf benannte Hanf-Lokalität und die nach Haim Gaifman benannte Gaifman-Lokalität.
Einführung Bearbeiten
Wir betrachten endliche Strukturen wie die eines Graphen. Ein Graph besteht aus einer endlichen Menge und einer zweistelligen Relation auf dieser Menge. Das Bestehen der Relation bedeutet, dass es eine Kante von nach gibt. Der Buchstabe E erinnert an das englische Wort edge für Kante. Damit lassen sich Graphen in der Prädikatenlogik erster Stufe beschreiben, wobei die Signatur nur aus der Relation besteht, also . Wir stellen nun die Frage, welche Eigenschaften von Graphen sich in der Prädikatenlogik erster Stufe ausdrücken lassen. Ein einfaches Beispiel ist:
- „Der Graph ist vollständig“ wird ausgedrückt durch
Interessanter ist die Untersuchung von Wegen in einem Graphen:
- „Es gibt einen Weg von nach der Länge “ wird ausgedrückt durch
- „Es gibt einen Weg von nach der Länge “ wird ausgedrückt durch
- „Es gibt einen Weg von nach der Länge “ wird ausgedrückt durch
- „Es gibt einen Weg von nach der Länge “ wird ausgedrückt durch
Indem man diese Kette in offensichtlicher Weise fortsetzt, erhält man für jedes feste einen -Ausdruck , der die Existenz eines Weges von nach der Länge ausdrückt. Zu anderen Eigenschaften finden sich keine Ausdrücke der Prädikatenlogik erster Stufe:
- „Es gibt einen Weg von nach “: ?
- „Der Graph ist zusammenhängend“: ?
Könnte man die Existenz eines Weges von nach durch einen Ausdruck ausdrücken, so würde den Zusammenhang ausdrücken. Das scheint nicht gelingen zu wollen, da man hierzu Wege immer größerer Länge und letztlich eine unendlich lange oder-Verknüpfung zulassen müsste. Für beliebige Graphen kann es tatsächlich keinen -Satz geben, der den Zusammenhang ausdrückt. Um das einzusehen, erweitern wir die Sprache um zwei Konstanten und betrachten die unendlich vielen Sätze
Jede endliche Teilmenge dieser Sätze enthält nur endlich viele Sätze der Form und damit keine Sätze mit für ein geeignetes, endliches . Daher ist diese endliche Teilmenge durch den zyklischen Graphen erfüllbar, wenn man und durch gegenüberliegende Punkte interpretiert. Nach dem Kompaktheitssatz wäre dann die Gesamtheit obiger Sätze erfüllbar und man erhielte einen Graphen, der wegen zusammenhängend ist und keinen Weg endlicher Länge von nach hat. Dieser Widerspruch zeigt, dass es einen -Satz , der den Zusammenhang ausdrückt, nicht geben kann.
An dieser Argumentation ist die Anwendung des Kompaktheitssatzes unbefriedigend, denn dazu muss man auch unendliche Modelle zulassen. Da man die Endlichkeit eines Modells in der Prädikatenlogik erster Stufe bekanntlich nicht formulieren kann, ist nicht ausgeschlossen, dass es einen -Satz geben könnte, der für endliche Graphen den Zusammenhang ausdrückt. Um zu zeigen, dass auch das nicht möglich ist, betrachten wir Längen von Wegen zwischen zwei Punkten als Abstandsbegriff. Damit sagt aus, dass in einer gewissen Umgebung von liegt. Es scheint nun so zu sein, dass -Ausdrücke prinzipiell nicht zwischen Punkten in beliebig großen Entfernungen unterscheiden können, also nur zu lokalen Aussagen fähig sind. Die Präzisierung dieser Überlegungen führt zu den im Folgenden vorgestellten Lokalitätsbegriffen, mit denen unter anderem die Nichtformulierbarkeit des Zusammenhangs in der Prädikatenlogik erster Stufe gezeigt werden kann.
Eigenschaften von Strukturen Bearbeiten
Eine Struktur zu einer Signatur besteht bekanntlich aus einer Menge , dem sogenannten Universum der Struktur, und einer Interpretation eines jeden Symbols aus . Einem k-stelligen Relationssymbol wird vermöge eine Teilmenge zugeordnet, das heißt eine k-stellige Relation über dem Universum. Ist wie in obiger Einführung mit einer zweistelligen Relation , so ist eine -Struktur nichts anderes als ein Graph. Ein Isomorphismus zwischen -Strukturen ist eine bijektive Abbildung zwischen den unterliegenden Universen, die die Interpretationen der Struktur erhält. Im Falle von Graphen, also -Strukturen und , heißt das einfach, dass die Abbildung, etwa , bijektiv ist, aus stets folgt und dass für die Umkehrabbildung dasselbe gilt. Hat die Struktur ein Konstanten-Symbol, etwa , das in den Strukturen durch bzw. interpretiert ist, so bedeutet die Erhaltung der Struktur unter nichts anderes als .
Wir interessieren uns im Folgenden für k-stellige Eigenschaften, die unter Isomorphismen invariant sind. Eine solche Eigenschaft, auch Query genannt, ordnet jeder Struktur eine Teilmenge zu, so dass für jeden Isomorphismus gilt, dass .
Ein Beispiel für eine 2-stellige Eigenschaft von Graphen ist die transitive Hülle, die der Kantenrelation ihre transitive Hülle in zuordnet.
Für setzt man . Für eine 0-stellige Eigenschaft gibt es dann nur zwei Möglichkeiten, oder , was man dann als falsch bzw. wahr interpretieren kann. Statt von 0-stelligen Eigenschaften spricht man daher auch von booleschen Eigenschaften. Ein typisches Beispiel ist der Zusammenhang von Graphen: Ein Graph hat diese Eigenschaft oder nicht und diese Eigenschaft bleibt bei Isomorphie erhalten.
Ist ein logischer Ausdruck mit freien Variablen , so ist durch
eine k-stellige Eigenschaft gegeben, ist die Menge aller Tupel, für die der Ausdruck in der Struktur wahr wird. Im Falle k=0 ist das wieder als falsch bzw. wahr zu interpretieren, dann wird die Eigenschaft durch einen Satz als logischen Ausdruck definiert und statt schreibt man auch .
Es geht im Folgenden um die Frage, welche solcher Eigenschaften durch Ausdrücke gewisser Logiken nicht definiert werden können. Das beschreibt Grenzen der Ausdrucksstärke solcher Logiken.
Gaifman-Graph Bearbeiten
Wir betrachten Signaturen, die nur aus Relationen bestehen, sogenannte relationale Signaturen. Funktionen können mit ihren Funktionsgraphen und somit ebenfalls als Relationen aufgefasst werden, allerdings mit einer um 1 erhöhten Stelligkeit, Konstanten können oft als einelementige, einstellige Relationen betrachtet werden. Um den oben erwähnten Abstandsbegriff zu erhalten, ordnen wir jeder Struktur einer relationalen Signatur einen Graphen , den sogenannten Gaifman-Graphen zu. Seine Punkte sind die Elemente aus dem zugehörigen Universum . Zwei verschiedene Punkte und sind genau dann durch eine Kante verbunden, wenn sie in einer Relation zueinander stehen, genauer, wenn es ein n-stelliges und gibt mit und . Dabei ist die Interpretation von in der Struktur .
In der in gegebenen Definition werden alle Paare zum Gaifman-Graphen hinzugenommen, das heißt, dass die Gleichheit wie die anderen Relationen behandelt wird. Das hat zur Folge, dass an jedem Punkt des Graphen eine Schleife hängt. Die hier verwendete Definition aus dem unten angegebenen Lehrbuch von Ebbinghaus und Flum schließt genau das aus, der Gaifman-Graph soll schleifenfrei sein. Für den hier einzuführenden Abstandsbegriff ist das unerheblich.
Besteht beispielsweise aus einer zweistelligen Relation < und ist , wobei die Relation als die übliche Größenrelation zwischen natürlichen Zahlen interpretiert, so ist der vollständige Graph mit Punkten , denn je zwei verschiedene Elemente stehen bzgl. < in Relation, das heißt sind der Größe nach vergleichbar.
Ein weiteres Beispiel ist mit einer zweistelligen Relation , so dass jede endliche -Struktur ein gerichteter Graph ist. Der Gaifman-Graph ist dann der zugehörige ungerichtete, schleifenfreie Graph. Dieses Beispiel ist prototypisch für die folgenden Überlegungen.
Kugeln in Gaifman-Graphen Bearbeiten
Da wir jeder Struktur ihren Gaifman-Graphen zugeordnet haben, können wir vom Abstand zweier Elemente des zugehörigen Universums sprechen, wir setzen
falls die Punkte überhaupt durch einen Weg verbunden sind, sonst ist der Abstand unendlich. Insbesondere können wir von -Kugeln bzgl. eines Tupels sprechen:
Da der Abstand nur ganzzahlige Werte oder annehmen kann, genügt es, ganzzahlige Radien zu betrachten. Die Grundidee besteht darin, zu untersuchen, wie weit gewisse logische Sätze der betrachteten Logik bzgl. dieses Abstandes reichen, das wird unten als Hanf-Lokalität bzw. Gaifman-Lokalität präzisiert. Aus diesem Grunde wollen wir die relative -Struktur auf den -Kugeln betrachten. Da wir in nur Relationen und keine Funktionen haben, ist das einfach die Einschränkung der Relationen . Dabei sind folgende zwei Dinge zu beachten.
Enthält die Signatur Konstanten , so genügt es nicht, diese als einstellige, einelementige Relationen zu betrachten, da die Einschränkung auf eine Teilmenge von , das heißt der Durchschnitt mit dieser Teilmenge, leer sein kann. Von Substrukturen verlangt man aber, dass sie die Konstanten ebenfalls enthalten. In diesem Fall muss man obige Definition durch
ersetzen. Das erweist sich lediglich als eine technische Ergänzung dieser Überlegungen.
Zweitens wollen wir die Zentren , zu denen Abstände gemessen werden, im Blick behalten. Dazu nehmen wir eine passende Konstantenexpansion vor, das heißt wir erweitern um neue Konstanten zu , die durch zu interpretieren sind, und setzten .
Zu jeder -Kugel um definieren wir nun die eingeschränkte -Struktur durch
- Das Universum ist .
- Jede k-stellige Relation wird als interpretiert.
- Jede Konstante wird als interpretiert.
Zwei Strukturen mit Universen und sowie vorgegebenen Tupeln heißen -äquivalent, in Zeichen
falls es eine Bijektion gibt, so dass für jedes
Dabei steht für den um verlängerten Vektor, das heißt , falls , und genauso . Die Isomorphiebeziehung bezieht sich auf -Strukturen, es gilt also insbesondere und . Es wird nicht verlangt, dass eine entsprechende Einschränkung von ein Isomorphismus sein soll, sondern nur, dass es irgendeinen Isomorphismus zwischen den -Strukturen geben soll, für einen solchen gilt allerdings wegen der zu berücksichtigenden Konstanten .
Für hat man keine vorgegebenen Tupel und . In diesem Fall schreibt man einfach , was dann die Existenz einer bijektiven Abbildung mit für alle bedeutet.
Hanf-Lokalität Bearbeiten
Eine -stellige Eigenschaft von relationalen -Strukturen heißt Hanf-lokal, falls es gibt, so dass folgendes gilt:
Sind und -Strukturen, , mit , so folgt .
Das kleinste , für das dies gilt, heißt der Rang der Hanf-Lokalität und wird mit bezeichnet. steht für die englische Bezeichnung Hanf local rank.
Zwei Strukturen stimmen also bzgl. der Eigenschaft bereits dann überein, wenn sie bzgl. aller -Kugeln ihrer Gaifman-Graphen übereinstimmen.
Gaifman-Lokalität Bearbeiten
Eine -stellige Eigenschaft von relationalen -Strukturen heißt Gaifman-lokal, falls es gibt, so dass folgendes gilt:
Ist eine -Struktur und sind mit so folgt .
Das kleinste , für das dies gilt, heißt der Rang der Gaifman-Lokalität und wird mit bezeichnet.
Gaifman-Lokalität ist der schwächere Begriff, es besteht die Beziehung . Beachte, dass sich Gaifman-Lokalität auf eine Struktur bezieht, während Hanf-Lokalität zwei Strukturen vergleicht.
Anwendungen Bearbeiten
In den Anwendungen weist man zunächst nach, dass alle durch bestimmte logische Ausdrücke definierten Eigenschaften Hanf- bzw. Gaifman-lokal sind, aber gewisse Eigenschaften nicht diese Lokalitätsbedingung erfüllen. Daraus folgt dann, dass nicht durch einen solchen logischen Ausdruck beschrieben werden kann, was eine Grenze der Ausdrucksstärke der betrachteten Logik markiert.
Lokalität der Prädikatenlogik erster Stufe Bearbeiten
Bezeichnet man mit alle logischen Ausdrücke der Prädikatenlogik erster Stufe, deren Quantoren eine Verschachtelungstiefe von höchstens haben, so gilt
für alle Eigenschaften , die durch einen -Ausdruck definiert werden können.
FO steht hierbei als Abkürzung für die englische Bezeichnung first order logic. Da jeder Ausdruck der Prädikatenlogik erster Stufe ein -Ausdruck für irgendein ist, sind alle durch Ausdrücke der Prädikatenlogik erster Stufe definierten Eigenschaften Hanf-lokal.
Zusammenhang von Graphen Bearbeiten
Es sei die boolesche Eigenschaft eines Graphen, das heißt einer -Struktur, zusammenhängend zu sein. Um zu zeigen, dass sich Zusammenhang auch für als endlich vorausgesetzte Graphen nicht in der Prädikatenlogik erster Stufe formulieren lässt, genügt es zu zeigen, dass nicht Hanf-lokal ist. Wäre Hanf-lokal, etwa mit , so wähle ein und betrachte den zyklischen Graphen mit Knoten und den Graphen , der aus der disjunkten Vereinigung zweier zyklischer Graphen mit je Knoten besteht. Die Gaifman-Graphen dieser Strukturen sind die Graphen selbst. In jedem dieser Graphen besteht eine -Kugel nach Wahl von aus einer Kette der Länge mit Mittelpunkt , und die sind als Untergraphen mit vorgegebenem Mittelpunkt alle untereinander isomorph. Jede Bijektion (beide Graphen haben Knoten) zeigt daher und aus der angenommenen Hanf-Lokalität folgte . Das kann aber nicht sein, denn ist zusammenhängend, aber nicht.
Transitive Hülle Bearbeiten
Nun beschreibe die transitive Hülle einer -Struktur, das heißt ist die Menge aller Paare , so dass es und gibt mit für alle und . Um zu zeigen, dass die transitive Hülle nicht durch einen Ausdruck der Prädikatenlogik erster Stufe beschrieben werden kann, genügt es zu zeigen, dass nicht Gaifman-lokal ist. Wäre Gaifman-lokal, etwa mit , so betrachte als -Struktur eine Kette mit . Kette bedeutet, dass die Relation als interpretiert wird. Die transitive Hülle dieser Relation ist dann nichts anderes als die natürliche Ordnung < auf . Der Gaifman-Graph ist ein linearer Graph der Länge . Auf Grund der Wahl von kann man zwei Knoten wählen, die von den Rändern den Abstand und untereinander den Abstand haben. Dann bestehen und beide aus je zwei disjunkten Teilketten der Länge mit Mittelpunkten . Daraus folgt und aus der angenommenen Gaifman-Lokalität ergäbe sich . Das kann aber nicht sein, denn von den Relationen und ist genau eine wahr.
Weitere Logiken Bearbeiten
Im Lichte obiger Beispiele stellt sich die Frage, ob es Erweiterungen der Prädikatenlogik erster Stufe gibt, für die jeder Ausdruck ebenfalls eine lokale Eigenschaft definiert. Derartige Erweiterungen wären immer noch nicht ausdrucksstark genug, um Graphenzusammenhang oder die transitive Hülle in endlichen Strukturen zu beschreiben.
Das Universum einer endlichen Struktur kann immer als linear geordnet angenommen werden. Diese Ordnung sei mit < bezeichnet, sie ist nicht Bestandteil der Signatur. Man kann zeigen, dass es von dieser Ordnung unabhängige Eigenschaften gibt, die sich aber mittels dieser Ordnung beschreiben lassen. Die Menge dieser Eigenschaften nennt man , das heißt wird um < erweitert und man beschränkt sich dann auf Eigenschaften, die nicht von < abhängen, was durch den Index inv (invariant) angedeutet wird. Dadurch erhält man eine echt größere Menge von Eigenschaften (Satz von Gurewich) und man kann zeigen, dass jede -Eigenschaft Gaifman-lokal ist (Satz von Grohe-Schwentick).
Bestimmte Ausdrücke infinitärer Logiken, die um Möglichkeiten des Zählens erweitert sind, können ebenfalls als Hanf- bzw. Gaifman-lokal nachgewiesen werden.
Siehe auch Bearbeiten
Einzelnachweise Bearbeiten
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Definition 2.7
- Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory, Springer-Verlag 1999, ISBN 3-540-28787-6, Kapitel 2.4
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag 2004, ISBN 3-540-21202-7, Definition 4.1
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Definition 4.2
- Grädel, Kolaitis, Libkin, Marx, Spencer, Vardi, Venema, Weinstein: Finite Model Theory and Its Applications, Springer-Verlag (2007), ISBN 978-3-540-00428-8, Definition 2.3.24, hier hat abweichend das Universum .
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Definition 4.6
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Definition 4.7
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Theorem 4.11
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Theorem 4.12
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Seite 48
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Seite 49
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Theorem 5.2
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Theorem 5.8
- Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Theorem 8.4