Transcript
Übersicht Teil 3
• Kapitel 3.1: Sequenzenkalkül
Logik Teil 3: Mehr zur Prädikatenlogik erster Stufe
• Kapitel 3.2: Rekursive Aufzählbarkeit, Kompaktheit und
Löwenheim-Skolem
• Kapitel 3.3: Ausdrucksstärke /
Grundlagen von Ehrenfeucht-Fraïssé-Spielen
• Kapitel 3.4: Ehrenfeucht-Fraïssé-Spiele: Anwendungen
2
Mehr zur Prädikatenlogik
Sequenzenkalkül
Wir betrachten einen Kalkül für Gültigkeit in der Prädikatenlogik. Motivation: ¨ • rekursive Aufzahlbarkeit nachweisen • einfacher Beweis fur ¨ das Kompaktheitstheorem in FO
Kapitel 3.1: Sequenzenkalkül
Im Prinzip könnten wir wieder Resolution verwenden (Grundlage für Theorembeweiser der Logik erster Stufe) Wir verwenden aber einen technisch einfacheren Ansatz: Gentzens Sequenzenkalkül Der Einfachheit halber verzichten wir auf das Gleichheitsprädikat
3
4
Sequenz
Sequenzenkalkül
Definition Sequenz Eine Sequenz ist ein Ausdruck der Form ) , ¨ wobei und endliche Mengen von Satzen sind. •
das Antezendenz und
•
das Sukzedenz.
Die Sequenz
Wir nennen
Offensichtlich: V
W
ist gultig, wenn |= , in Worten: ¨ V jedes Modell von macht auch mindestens einen Satz aus )
Ist eine Sequenz
)
Der Sequenzenkalkül erlaubt, alle gültigen Sequenzen abzuleiten.
gultig, so schreiben wir |= ¨
)
• FO-Satz ' ist Tautologie gdw. die Sequenz ; ) {'} gultig ist ¨
wahr
• FO-Satz ' ist unerfullbar gdw. die Sequenz {'} ) ; gultig ist ¨ ¨ W (denn ; ist unerfullbar) ¨
.
Man kann den Sequenzenkalkül also auch als Kalkül zum Ableiten
Beispiele für gültige Sequenzen:
aller Tautologien/unerfüllbaren Formeln ansehen.
• {8x P (x), Q(c)} ) {P (c) ^ Q(c), R(c, d)} • {P (c) _ Q(d)} ) {P (c), Q(d)} 5
6
Bestandteile des SK
Axiome des SK
Die zentralen Bestandteile des SK:
Zum Hervorheben von Formeln in Sequenzen schreiben wir ,' )
• Axiome
,
statt
[ {'} )
[{ }
Sequenzen, die man ohne Beweis/Herleitung als gültig voraussetzt Definition Axiome SK Die Axiome des Sequenzenkalkuls ¨ (SK) sind alle Sequenzen der Form , ) , .
• Schlussregeln Im Gegensatz zu Resolution/Hilbert hat das SK recht viele davon: 2 Stuck ¨ pro Operator ¬, ⇤, ⌅, , ⇥,
Axiome sind offensichtlich gültige Sequenzen
jeweils für die linke und die rechte Seite von Sequenzen (positive und negative Form der Regel)
7
8
Schlussregeln des SK (¬
)
)
,
(
,¬ (_ ))
(^ ))
(9 ))
(8 ))
,⇥ )
, ,⇥ _
, ⇥, ,⇥ ^
)
() _)
)
)
() ^)
)
, [c] ) ⇥ , 9x '(x) ) , [t] ) ⇥ , 8x '(x) )
¬)
c nicht in , ⇥, (x)
() 9)
() 8)
Ableitbarkeit im SK )
,
Definition ableitbar
,¬ )
, ⇥,
)
,⇥ _
)
,⇥ )
Die Menge der ableitbaren Sequenzen ist die kleinste Menge von Sequenzen, die ¨ und • alle Axiome des SK enthalt )
• abgeschlossen ist unter Regelanwendung: wenn Instanzen der Sequenzen in der oberen Zeile einer Schlussregel enthalten sind, so auch die entsprechende Instanz der unteren Zeile
,
,⇥ ^
Ist eine Sequenz
) ⇥, [t] )
)
Instanz bedeutet: , ⇥, ⇥,
, 9x '(x)
) ⇥, [c]
⇥ ableitbar, so schreiben wir ⇥
durch konkrete Formeln/Formelmengen ersetzen
Beispiel
c nicht in
, 8x '(x)
⇥.
, ⇥, (x) 9
10
SK-Beweise
SK-Beweise Zur Erinnerung:
Definition SK-Beweis
In der Sequenz ,
Ein SK-Beweis ist ein Baum, dessen Knoten auf folgende Weise mit Sequenzen beschriftet sind:
darf
auch
enthalten, muss aber nicht
Darum darf man bei Anwendung von (
• Jedes Blatt ist mit einem Axiom beschriftet
die verwendete Teilformel “behalten”:
• Jeder innere Knoten ist mit einer Instanz der unteren Zeile einer Schlussregel beschriftet
Beispiel (⇥
• die Kinder dieses Knotens sind dann genau mit den entsprechenden Instanzen der Sequenzen in der oberen Zeile der Regel beschriftet.
P (c)
):
(8 ))
P (c) ⇥ P (d)
8x P (x) ) P (c) ^ P (d)
Beachte:
• jeder innere Knoten hat ein oder zwei Kinder • eine Sequenz ist ableitbar gdw. sie als Knotenbeschriftung in einem
(ohne Behalten)
SK-Beweis auftritt.
⇤) und (⇥
) im SK-Beweis
, [t] ) ⇥ , 8x '(x) ) 8x P (x), P (c) ) P (c) ^ P (d) 8x P (x) ) P (c) ^ P (d)
(mit Behalten)
Das gilt im Prinzip fur ¨ alle Regeln, ist aber nur bei () 9) und (8 )) nutzlich (und notwendig!) ¨
Beispiel 11
12
Korrektheit SK
Vollständigkeit SK Theorem (Vollständigkeit SK)
Theorem (Korrektheit SK) Wenn ⇥
⇥, dann |=
Wenn |=
⇥ (jede ableitbare Sequenz ist gultig). ¨
⇥, dann ⇥
⇥ (jede gultige Sequenz ist ableitbar). ¨
Beweis:
Beweisstrategie:
Es reicht zu zeigen:
Man beweist das Kontrapositiv: wenn
1. alle SK-Axiome sind gultig ¨ offensichtlich gilt
|=
⇥
⇥ wenn es
⇥
⇤ ⇥ gibt
)
(Details im Grädel-Skript)
nicht ableitbar, dann
)
Also zu zeigen: es gibt Modell A fur ¨
2. wenn eine Sequenz ⇥ durch das Anwenden einer Schlussregel auf gultige Sequenzen entsteht, dann ist ⇥ gultig. ¨ ¨
nicht gultig, also ¨
[ ¬ , wobei ¬
V
6|=
W
= {¬' | ' 2
. }
¨ Im Prinzip mochten wir A einfach aus die Nicht-Ableitbarkeit von
Fallunterscheidung: ein Fall pro Regel.
)
ablesen“; ” soll sicherstellen, dass A |= ¬
13
Vollständigkeit SK
14
Mehr zur Prädikatenlogik
Theorem (Vollständigkeit SK) Wenn |= A aus ”
⇥, dann ⇥
⇥ (jede gultige Sequenz ist ableitbar). ¨
ablesen“: wenn z. B. = {Q1 (c), ¬Q2 (c), 9x P (x), P (c)}
dann ist klar, wie A aus
= {Q2 (c), ¬P (c)}
Kapitel 3.2: Rekursive Aufzählbarkeit, Kompaktheit und Löwenheim-Skolem
abgelesen wird und dass A |= ¬ .
Das geht aber nicht immer so einfach: = {Q1 (c) _ Q2 (c), 9x P (x)} Man muss darum
und
= {· · · }
¨ erst vervollstandigen.
Für später: das konstruierte Modell ist höchstens abzählbar unendlich. 15
16
Rekursive Aufzählbarkeit
Rekursive Aufzählbarkeit
Theorem (Rekursive Aufzählbarkeit)
Theorem (Rekursive Aufzählbarkeit)
¨ ¨ Fur Signatur ⌧ sind rekursiv aufzahlbar: ¨ jede rekursiv aufzahlbare
¨ ¨ Fur Signatur ⌧ sind rekursiv aufzahlbar: ¨ jede rekursiv aufzahlbare
• die Menge aller Tautologien aus FO(⌧ )
• die Menge aller Tautologien aus FO(⌧ )
¨ • die Menge aller unerfullbaren Satze aus FO(⌧ ) ¨
¨ • die Menge aller unerfullbaren Satze aus FO(⌧ ) ¨
Beweis:
Beweis:
¨ ¨ 1. Die Menge aller Satze uber Signatur ⌧ ist rekursiv aufzahlbar: ¨
¨ 2. Die Menge aller SK-Beweise uber Signatur ⌧ ist rekursiv aufzahlbar: ¨ ¨ ¨ • Erzeuge alle Baume mit max. binarer Verzweigung, deren Knoten mit Strings uber dem Alphabet ¨ {¬, ^, _, 9, 8, (, ), =} [ VAR [ ⌧ markiert sind
• Erzeuge alle Strings uber dem Alph. {¬, ^, _, 9, 8, (, ), =} [ VAR [ ⌧ ¨ • Gib diejenigen aus, die ein wohlgeformter FO-Satz sind
• Gib diejenigen aus, die SK-Beweise sind
17
18
Rekursive Aufzählbarkeit
Rekursive Aufzählbarkeit
Theorem (Rekursive Aufzählbarkeit)
Korollar
¨ ¨ Fur Signatur ⌧ sind rekursiv aufzahlbar: ¨ jede rekursiv aufzahlbare
¨ ¨ ist die Menge Wenn ⌧ mind. ein binares Relationssymbol enthalt, ¨ der erfullbaren FO(⌧ )-Formeln nicht rekursiv aufzahlbar. ¨
• die Menge aller Tautologien aus FO(⌧ ) ¨ • die Menge aller unerfullbaren Satze aus FO(⌧ ) ¨
Denn:
Beweis:
¨ Um Erfullbarkeit von ' zu prufen, zahle simultan ¨ ¨ die erfullbaren Formeln und die unerfullbaren Formeln auf: ¨ ¨
¨ 3. Die Menge aller Tautologien ist rekursiv aufzahlbar: • Erzeuge alle SK-Beweise
erfüllbar '1
• Fur ¨ alle darin vorkommenden Sequenzen ; ) {'} gib ' aus
unerfüllbar 1
Begrundung: ' ist Tautologie gdw. es SK-Beweis fur ¨ ¨ ; ) {'} gibt ¨ (Korrektheit und Vollstandigkeit des SK)
'2 .. .
2
.. . Nach endlicher Zeit findet man Eingabeformel '.
¨ analog fur Satze: {'} ) ; ¨ unerfullbare ¨
Beachte: entscheidend ist hier die Endlichkeit von SK-Beweisen
¨ ¨ Waren die erfullbaren Formeln rekursiv aufzahlbar, ¨ ¨ Erfullbarkeit so ware entscheidbar: ¨
19
20
Rekursive Aufzählbarkeit
Theorembeweiser
Über endlichen Strukturen kehrt sich die Situation um:
Rekursive Aufzählbarkeit liefert Semi-Entscheidbarkeit für Gültigkeit
(und Unerfüllbarkeit):
Theorem (Rekursive Aufzählbarkeit, endliche Modelle)
• wenn Eingabe Tautologie, dann terminiert der Algorithmus nach endlicher Zeit und antwortet gultig“; ¨ ” • anderenfalls terminiert der Algorithmus nicht
¨ Uber endlichen Modellen gilt: ¨ 1. die Menge der erfullbaren Formeln ist rekursiv aufzahlbar, ¨ ¨ fur Signatur ⌧ ¨ jede aufzahlbare ¨ 2. die Menge der unerfullbaren Formeln ist nicht rekursiv aufzahlbar, ¨ ebensowenig die Menge der Tautologien
Auf diesem Prinzip beruhen moderne Theorembeweiser wie Vampire, Paradox, Spass; allerdings wird ... • meist Resolution verwendet (mit aufwendigen Optimierungstechniken) ¨ ¨ • durch zusatzliche Verfahren in vielen Fallen“ auch Terminierung ” auf Nicht-Tautologien erreicht
Beweis in der Übung.
21
22
Theorembeweiser
Kompaktheit
Beachte:
Der Kompaktheitssatz für FO ist wie in der Aussagenlogik formuliert:
wenn eine FO-Theorie eine endliche Axiomatisierung ⇥ hat, dann kann ein Theorembeweiser auch fur verwendet werden: ¨
Theorem (Kompaktheitssatz)
'2
gdw.
V
¨ Fur ¨ alle Mengen von Satzen
⇧ ! ' Tautologie
Auch auf unendliche Axiomatisierungen können viele Beweiser
angepasst werden
¨ FO und Satze ' ⇥ FO gilt:
1.
ist erfullbar gdw. jede endliche Teilmenge von ¨
2.
|= ' gdw. endliches ⇥
erfullbar ist ¨
existiert mit ⇥ |= '
Dieser Satz hat verschiedene wichtige Anwendungen:
Man kann sie aber nicht verwenden, um zahlentheoretische Resultate
wie die Goldbachsche Vermutung zu beweisen, denn
• Nicht-Ausdruckbarkeitsbeweise von Eigenschaften in FO ¨ ¨ • fundamentale modelltheoretische Resultate wie die Satze ¨ von Lowenheim-Skolem
Th(N, +, ·, 0, 1)
ist ja nicht axiomatisierbar.
Sein Beweis verwendet eine Variation des Sequenzenkalküls 23
24
Erweitertes Sequenzenkalkül
Kompaktheit
Beweis von Kompaktheit erfordert Variation des Sequenzenkalküls:
Theorem (Kompaktheitssatz) ¨ Fur ¨ alle Mengen von Satzen
Anstatt fur von Sequenzen (|= ⇧ ) ) interessiert man ¨ die Gultigkeit ¨ sich nun fur ¨ die Folgerbarkeit von Sequenzen aus einer (eventuell unendlichen) Formelmenge : V W |= ⇧ ) steht fur |= ⇧ ! ¨
¨ ¨ man die -Erweiterung Fur ✓ FO erhalt ¨ eine Menge von Satzen des SK durch Hinzufugen der Regel ¨ ( -Regel)
⇧, ' ) ⇧)
1.
ist erfullbar gdw. jede endliche Teilmenge von ¨
2.
|= ' gdw. endliches ⇥
existiert mit ⇥ |= '
Es gibt SK-Beweis fur ¨ ⇧)
gdw.
|=
'2
in der -Erweiterung des SK ableitbar gdw.
erfullbar ist ¨
Beweis mittels -Erweiterung des Sequenzenkalkuls, ¨ in der also gilt: ^
⇧!
_
Beachte: es wird hier eine syntaktische Eigenschaft (Kalkül!)
Theorem (Korrektheit+Vollständigkeit erweiterter SK) ⇧)
¨ FO und Satze ' ⇥ FO gilt:
in eine rein semantische (Erfüllbarkeit, Konsequenz!) übertragen.
|= ⇧ ) 25
26
Kompaktheit
Unendliche Modelle
Wir nutzen die Kompaktheit zum Beweis einiger wichtiger modell-
Theorem (unbeschränkte endliche Modelle)
theoretischer Resultate
Wenn ein FO-Satz ' beliebig große endliche Modelle besitzt (d. h. fur ¨ jedes n 0 gibt es Modell A mit |A| n), dann hat ' auch ein unendliches Modell.
Diese beziehen sich einerseits auf die Größe von Modellen:
• Wie groß können die Modelle einer gegebenen Formel werden? Dieses Theorem impliziert eine Beschränkung der Ausdrucksstärke
• Gibt es Formeln, die nur in endlichen/unendlichen/abzählbaren/
von FO:
überabzählbaren Modellen erfüllbar sind?
Es gibt keinen FO-Satz ', so dass A |= ' gdw. |A| endlich.
Andererseits erlauben sie uns erste Beobachtungen bezüglich der Grenzen der Ausdrucksstärke von FO:
Das heißt: Endlichkeit ist nicht FO-ausdrückbar. ¨ Fur n“ aber naturlich leicht ausdruckbar: ¨ ein festes n ist Modellgroße ¨ ¨ ” W 8x0 · · · 8xn 0i n
W
0i 2k
i
Korollar Duplicator hat Gewinnstrategie fur ¨ Gk (Ak , Bk ). 51
52
Zusammenhang
Erreichbarkeit Für viele Anwendungen ist es nützlich,
Erreichbarkeit bezüglich einer binären Relation verwenden zu können. Beispiel SQL: Datenbank mit Direktverbindungen einer Fluggesellschaft
Mittels Erreichbarkeit bekommt alle Verbindungen, mit und ohne Umsteigen
Korollar Zusammenhang ist nicht FO-ausdruckbar, weder in der Klasse aller ¨ Strukturen noch in der Klasse aller endlichen Strukturen.
Wichtiges Resultat: Theorem ¨ Relation. Es gibt keine Formel '(x, y) 2 FO(⌧ ) Sei ⌧ = {E} mit E binare die Erreichbarkeit (entlang E) definiert, d.h. so dass fur ¨ alle Strukturen A = (A, E A ) gilt: A |= '[a, b] gdw. es einen Pfad in A von a nach b gibt 53
Nicht-Ausdrückbarkeit
Auch nicht FO-ausdruckbar z.B.: ¨ ¨ • Azyklizitat • Graphen, die ein Baum sind ¨ • Planaritat ¨ • k-Farbbarkeit fur ¨ beliebiges (fixes) k
2
• quasi jede algorithmisch interessante Eigenschaft von Graphen (wir werden in Teil 4 sehen, warum das so ist!)
55
54
