Vortragsfolien - tdi.informatik.uni

¨ hrung
Logik in der Informatik - Einfu
in die formale Logik
Sommersemester 2015
Prof. Dr. Isolde Adler
Ehrenfeucht-Fra¨ıss´
e-Spiele
Inhalt
4. Ehrenfeucht-Fra¨ıss´e-Spiele
4.1
4.2
4.3
4.4
4.5
4.6
Isolde Adler
Das m-Runden EF-Spiel
Der Satz von Ehrenfeucht
Logische Reduktionen
Der Satz von Hanf
Die Hanf-Lokalit¨
at der Logik erster Stufe
Der Satz von Fra¨ıss´e
Logik – SoSe 2015
2/12
Ehrenfeucht-Fra¨ıss´
e-Spiele
Bemerkung 4.22 (Gewinnstrategie fu
¨r Spoiler)
Seien A und B zwei σ-Strukturen. Sei ϕ ein FO[σ]-Satz s. d. A |= ϕ und
B 6|= ϕ. Sei m := qr(ϕ).
Gem¨aß Satz 4.21 und Satz 4.8 hat dann Spoiler eine Gewinnstrategie im
Spiel Gm (A, B).
Der Satz ϕ gibt sogar direkt einen Gewinnstrategie f¨
ur Spoiler an. Er
gewinnt, indem er Elemente in A w¨ahlt, die den ∃-Quantoren in ϕ
entsprechen, und Elemente in B, die den ∀-Quantoren in ϕ entsprechen.
Beispiel
– Siehe Tafel –
Isolde Adler
Logik – SoSe 2015
3/12
Ehrenfeucht-Fra¨ıss´
e-Spiele
Bemerkung 4.23 (≡m hat nur endlich viele
¨
Aquivalenzklassen)
Sei m ∈ N und sei σ eine funktionenfreie, endliche Signatur. Dann gilt:
¨
(a) ≡m hat nur endlich viele Aquivalenzklassen
auf der Klasse aller
σ-Strukturen.
¨
(b) Die ≡m -Aquivalenzklasse,
zu der die Struktur A geh¨ort, wird durch
m
ϕA definiert.
(c) F¨
ur alle FO[σ]-S¨atze ψ mit qr(ψ) = m gilt:
{A : A ist eine σ-Struktur, A |= ψ}
¨
ist eine endliche Vereinigung von Aquivalenzklassen
bzgl. ≡m .
(d) Es gibt nur endlich viele paarweise nicht ¨aquivalente Formeln vom
Quantorenrang h¨
ochstens m.
Beweis.
– Siehe Tafel –
Isolde Adler
Logik – SoSe 2015
4/12
Ehrenfeucht-Fra¨ıss´
e-Spiele
Korollar 4.24
Sei σ eine endliche, funktionenfreie Signatur. Ist S eine Klasse von
Strukturen und C ⊆ S eine Klasse von σ-Strukturen, so sind folgende
Aussagen ¨aquivalent:
(a) C ist nicht FO-definierbar in S.
(b) F¨
ur jedes m ∈ N gibt es σ-Strukturen Am ∈ C und Bm ∈ S \ C , so
dass Am ≈m Bm .
Beweis.
– Siehe Tafel –
Isolde Adler
Logik – SoSe 2015
5/12
Ehrenfeucht-Fra¨ıss´
e-Spiele
Inhalt
4. Ehrenfeucht-Fra¨ıss´e-Spiele
4.1
4.2
4.3
4.4
4.5
4.6
Isolde Adler
Das m-Runden EF-Spiel
Der Satz von Ehrenfeucht
Logische Reduktionen
Der Satz von Hanf
Die Hanf-Lokalit¨
at der Logik erster Stufe
Der Satz von Fra¨ıss´e
Logik – SoSe 2015
6/12
Ehrenfeucht-Fra¨ıss´
e-Spiele
Satz 4.25 (Graphzusammenhang und Erreichbarkeit sind
nicht FO-definierbar)
(a) Sei UGraphs die Klasse aller endlichen ungerichteten Graphen.
D. h. aller σGraph -Strukturen A = (A, E A ), ss dass E A irreflexiv und
symmetrisch ist.
Sei Conn die Klasse aller endlichen ungerichteten
zusammenh¨angenden Graphen.
Es gilt: Conn ist nicht FO-definierbar in UGraphs.
(b) Sei σ := {E , s, t} mit einem zweistelligen Relationssymbol E und
zwei Konstantensymbolen s und t. Sei RGraphs die Klasse aller
σ-Strukturen, und sei Reach die Klasse aller σ-Strukturen A, in
denen es einen Pfad von s A nach t A gibt.
Es gilt: Reach ist nicht FO-definierbar in RGraphs.
Beweis.
– Siehe Tafel –
Isolde Adler
Logik – SoSe 2015
7/12
Ehrenfeucht-Fra¨ıss´
e-Spiele
Bemerkung 4.26 (logische Reduktion)
Die Vorgehensweise im Beweis von Satz 4.26 ist unter dem Begriff
logische Reduktion (bzw. logische Interpretation) bekannt.
Im Beweis von Satz 4.26 wurde das Problem, einen FO-Satz zu finden,
der ausdr¨
uckt, dass einen lineare Ordnung gerade Kardinalit¨at hat, auf
das Problem reduziert, einen FO-Satz zu finden, der
Graph-Zusammenhang definiert.
Dazu haben wir innerhalb einer linearen Ordnung einen geeigneten
Graphen simuliert“ (bzw. interpretiert“), indem wir die Kantenrelation
”
”
des Graphen durch eine FO-Formel beschrieben haben.
Diese Methode der logischen Reduktion ist oft n¨
utzlich, um bereits
bekannte Nicht-Definierbarkeits-Resultate auf neue
Nicht-Definierbarkeits-Resultate zu u
¨bertragen.
Isolde Adler
Logik – SoSe 2015
8/12
Ehrenfeucht-Fra¨ıss´
e-Spiele
Inhalt
4. Ehrenfeucht-Fra¨ıss´e-Spiele
4.1
4.2
4.3
4.4
4.5
4.6
Isolde Adler
Das m-Runden EF-Spiel
Der Satz von Ehrenfeucht
Logische Reduktionen
Der Satz von Hanf
Die Hanf-Lokalit¨
at der Logik erster Stufe
Der Satz von Fra¨ıss´e
Logik – SoSe 2015
9/12
Ehrenfeucht-Fra¨ıss´
e-Spiele
Der Satz von Hanf
Der Satz von Hanf liefert ein hinreichendes Kriterium f¨
ur die
¨
m-Aquivalenz
zweier Strukturen, so dass man durch die Anwendung
dieses Satzes leicht zeigen kann, dass A ≡m B, ohne daf¨
ur explizit eine
Gewinnstrategie f¨
ur Duplicator im m-Runden EF-Spiel konstruieren zu
m¨
ussen.
Isolde Adler
Logik – SoSe 2015
10/12
Ehrenfeucht-Fra¨ıss´
e-Spiele
Definition 4.27 (Gaifman-Graph; Distanzfunktion;
Nachbarschaft). . .
Sei σ eine funktionenfreie Signatur und sei A eine σ-Struktur.
(a) Der Gaifman-Graph G(A) von A ist der ungerichtete Graph mit
Knotenmenge V G(A) = A und Kantenmenge
E G(A) := {u, v } : u 6= v und es gibt ein R ∈ σ und ein
Tupel (a1 , . . . , ar ) ∈ R A sodass u, v ∈ {a1 , . . . , ar }
Isolde Adler
Logik – SoSe 2015
11/12
Ehrenfeucht-Fra¨ıss´
e-Spiele
. . . Definition 4.27 (Gaifman-Graph; Distanzfunktion;
Nachbarschaft)
(b) Die Distanzfunktion DistA : A × A → N ∪ {∞} ist definiert durch:
DistA (u, v ) := min{` ∈ N : es gibt einen Pfad der L¨ange `
in G(A) von u nach v }.
Falls es in G(A) keinen Pfad von u nach v gibt, ist DistA (u, v ) := ∞.
Ist v ∈ A und U ⊆ A, so setzen wir
DistA (v , U) := min{DistA (v , u) : u ∈ U}.
Isolde Adler
Logik – SoSe 2015
12/12

Download Report