Syntax und Semantik der Prädikatenlogik Flashcards
(23 cards)
Definition Signatur
Eine Signatur tau ist eine Menge von Funktions und Relationssymbolen. Jedes dieser Symbole hat eine feste endliche Stelligkeit. Eeine Signatur heisst relational, wenn sie nur Relationssymbole enthält bzw. funktional oder algebraisch, wenn sie ausschliesslich Funktionssymbole enthält. Nullstellige Funktionssymbole heissen auch Konstantensymbole.
Wie wird eine Struktur festgelegt?
Allgemeine durch Angabe ihres Universums und der Interpretation der Relations- und Funktionssymbole über diesem Universum. Eine Struktur mit funktionaler Signatur tau heisst auch eine tau-Algebra.
Definition Substruktur / Erweiterung
Seine A~ und B~ tau-Strukturen. A~ ist Substruktur von B~, wenn:
- A Teilmenge von B (auch wenn A = B)
- für alle Relationssymbole R element tau gilt:
R^A~ = R^B~ schnitt A^n (n ist Stelligkeit von R, also sind nurnoch Elemente in R^A~, die in A vorkommen)
- für alle Funktionssymbole f element tau gilt: f_A = f^B~|_A, d.h. f^A~ ist die Restriktion von f^B~ auf A
Wenn A~ eine Substruktur der tau-Struktur B~ ist, dann ist A tau-abgeschlossen. D.h. für alle n-stelligen f element tau und alle a1,…,an element A ist f^B~(a1,..,an) element A
(Also können nur Substrukturen erzeugt werden, die unter den gegebenen Funktionen abgeschlossen sind)
Umgekehrt gilt auch: Sei B~ eine tau-Struktur. Zu jeder nicht-leeren, tau-abgeschlossenen Teilmenge A von B gibt es genau eine Substruktur von B~ mit Träger A. Wir nennen sie die von A in B~ induzierte Substruktur.
Wenn A Substruktur von B, so heisst B Erweiterung von A
Definition Redukt / Expansion
Seien sigma Teilmenge von tau Signaturen, und sei B eine tau-Struktur. Das sigma-Redukt B|~ sigma von B ist die sigma-Struktur, die wir aus B erhalten, wenn wir die Relationen und Funktionen in tau\sigma einfach weglassen. Ist A Redukt einer tau-Struktur B, so nennen wir B eine tau-Expansion von A.
Definition tau-Term
die Menge T(tau) der tau-Terme ist induktiv wie folgt definiert:
- VAR Teilmenge T(tau), d.h. jede Variable ist ein tau-Term
- sind t1, … , tn tau-Terme und ist f ein n-stelliges Funktionssymbol aus tau, so ist auch ft1, … tn ein tau-Term.
Ein Grundterm ist ein Term, in dem keine Variablen auftreten (also Konstanten und Funktionen auf Konstanten)
Definition Menge FO(tau) der tau-Formeln der Prädikatenlogik
Induktiv wie folgt definiert:
(1) Sind t1, t2 tau-Terme, dann ist t1 = t2 eine tau-Formel
(2) Sind t1, … , tn tau-Terme und ist P element tau ein n-stelliges Relationssymbol, dann ist Pt1,…,tn eine tau-Formel
(3) Wenn psi eine tau-Formel ist, dann auch nicht psi
(4) wenn psi und phi tau-Formeln sind, dann ach phi und psi, phi oder psi und phi impliziert psi.
(5) Wenn psi eine tau-Formel ist und x element VAR eine Variable, dann sind “Es existiert x”psi und “Für alle x”psi tau-Formeln
Eine Formel die nur nach Regeln (1) und (2) definiert ist heisst atomar, Atom-Formel oder einfach Atom.
Formeln die nur nach Regeln (1) - (4) definiert sind heissen quantorenfrei.
Definition 2.7 freie Variablen \ Menge Variablen einer Formel
sei t element T(tau) ein Term und psi element FO(tau) eine Formel. Mit var(t) bzw. var(psi) bezeichnen wir die Menge aller in t bzw. psi auftretenden Variablen. Die Menge frei(psi) der freien Variablen von psi ist induktiv wie folgt definiert:
- für atomare Formeln psi ist frei(psi) := var(psi)
- frei(nicht psi) := frei(psi)
- frei(psi * phi) := frei(psi) vereinigt frei(phi)
- frei(ex.x psi) = frei(Alle.x psi) := frei(psi) \ {x}
Ein tau-Satz ist eine tau-Formel ohne freie Variablen
Mächtigkeit von T(tau) und FO(tau)
Wenn tau abzählbar ist, dann auch das Alphabet Alph(tau). Es folgt dann, dass auch Alph(tau)*, und damit insbesondere T(tau) und FO(tau) abzählbar sind. Andererseits sind T(tau) und FO(tau) auch bei endlicher Signatur (sogar leerer Signatur) unendlich. In der Tat enthält T(tau) alle Variablen und FO(tau) alle Formeln x=y für x,y element VAR.
Definition 2.8 Modellbeziehung
Sei tau eine Signatur. Eine tau-Interpretation ist ein Paar I = (A~, beta) wobei A~ eine tau-Struktur und beta: X -> A eine Belegung von Variablen durch Elemente von A ist. Dabei ist X = dom(beta) Teilmenge von VAR. Eine tau-Interpretation I = (A~, beta) ordnet:
Jedem Term t element T(tau) mit var(t) teilmenge von dom(beta) einen Wert [t]^I element von A zu, und
jeder Formel psi element FO(tau) mit frei(psi) teilmenge von dom(beta) einen Wahrheitswert [psi]^I element {0,1}.
Lemma 2.9 Koinzidenzlemma
Sei psi element FO(sigma SCHNITT tau), (A~, beta) eine sigma-Interpretation und (A~’, beta’) eine tau-Interpretation, so dass folgendes gilt:
i) A~ und A~’ haben dasselbe (sigma SCHNITT tau)-Redukt: A~ |~ (sigma SCHNITT tau) = A~’ |~ (sigma SCHNITT tau)
ii) frei(psi) teilmenge von (dom(beta) schnitt dom(beta’)) und beta(x) = beta’(x) fuer alle x element von frei(psi).
Dann gilt A~ |= psi[beta] genau dann, wenn A~’ |= psi[beta’]
Definition existenzieller bzw. universeller Abschluss,
Aussagen über Erfüllbarkeit und allgemeine Gültigkeit
Sei psi eine Formel mit freien Variablen x1, … , xk. Dann nennen wir die Sätze ex.x1. ex.x2 … ex.xk psi und fA.x1… fA.xk. psi den existenziellen bzw universellen Abschluss von psi.
Lemma 2.14:
eine formel ist genau dann erfüllbar, wenn ihr existentieller Abschluss erfüllbar ist
eine Formel ist genau dann allgemeingültig, wenn ihr universeller Abschluss allgemeingültig ist.
Definition reduzierte Formel
Eine Formel, in der die Symbole ‘und’, ‘impliziert’ und ‘für Alle’ nicht vorkommen, heisst reduziert.
(Also bleiben nicht, oder, existenz)
Zu jeder FO-Formel kann man effektiv eine logisch äquivalente reduzierte Formel konstruieren.
Definition Negationsnormalform
Eine Formel ist in Negationsnormalform, wenn sie aus Literalen (d.h. atomare Formeln und Negationen atomarer Formeln) nur mit Hilfe der Junktoren ‘oder’, ‘und’ und der Quantoren ‘es existiert’ und ‘für alle’ aufgebaut ist.
Jede Formel aus FO ist logisch äquivalent zu einer Formel in Negationsnormalform.
Definition termreduzierte Formeln
Eine Formel heisst termreduziert, wenn sie nur Atome der Form Rx, fx = y und x = y enthält (also insbesondere keine Terme der Tiefe >= 2)
Zu jeder Formel gibt es eine logisch äquivalente termreduzierte Formel.
Definition Pränex-Normalform
Eine Formel ist in Pränex-Normalform (PNF), wenn sie bereinigt ist und die Form Q1x1…. Qrxr psi hat, wobei psi quantorenfrei und Qi element {‘es ex.’, ‘für alle’}. Das Anfangsstück Q1x1…Qrxr nennt man das Quantoren-Präfix der Formel.
Jede Formel psi element FO(tau) lässt sich ein eine logisch äquivalente Formel in Pränex-Normalform transformieren.
(Eine Formel ist bereinigt, wenn keine Variable in psi sowohl frei, wie gebunden auftritt, und wenn keine Variable mehr als einmal quantifiziert ist)
Satz über die Skolemnormalform
Im Gegensatz zur Pränex Normalform ist die Skolem-Normalform einer Formel im Allgemeinen nicht zur ursprünglichen Formel logisch äquivalent; sie ist jedoch erfüllbarkeitsäquivalent (also gdw erfüllbar, wenn die ursprüngliche Formel erfüllbar ist)
Satz 2.23: Zu jedem Satz psi element FO(sigma) lässt sich ein Satz phi element FO(tau) mit sigma teilmenge von tau konstruieren, so dass gilt:
i) phi = fA.y1. … fA.ys.psi’, wobei psi’ quantorenfrei ist
ii) phi |= psi
iii) zu jedem Modell psi existiert eine Expansion, welche Modell von phi ist.
Die letzten beiden Punkte implizieren insbesondere, dass psi und phi über den selben Universen erfüllbar sind.
Satz 2.24 Für jeden Satz psi element FO(tau):
Was bedeutet es, wenn die Verifiziererin eine Gewinnstrategie in einem Spiel MC(A~, psi) von Position psi hat?
Für jeden Satz psi element FO(tau):
A~ |= psi gdw. die Verifiziererin hat eine Gewinnstrategie für das das Spiel MC(A~, psi) von der Anfangsposition psi
Satz 2.25 Laufzeit Algorithmus zum finden von Gewinnregionen endlicher Spiele?
(Für Problem GAME = { (G,v) : Spieler 0 hat eine Gewinnstrategie für G von Position v}
Defition: Gewinnregion, Gewinnstrategie, determiniertes Spiel
Die Gewinnregionen von endlichen Spielen kann man in Linearzeit berechnen.
Definition Gewinnregion: W_sigma = {v: Spieler sigma hat eine Gewinnstrategie von Position v}
Definition Gewinnstrategie: Wenn Spieler sigma jede Partie mit Anfangsposition v_0 gewinnt, wenn er mit Strategie f spielt, dann ist f eine Gewinnstrategie.
(f ordnet jeder nicht-terminalen Poisition von Spieler sigma, also wenn sigma im Spielgraphen ziehen darf, einen Zug zu einer beliebigen Spielposition V zu)
Ein Spiel ist determiniert, wenn von jeder Position aus einer der beiden Spieler eine Gewinnstrategie hat. d.h. Wenn W_0 vereinigt W_1 = V
Definition von axiomatisierbarkeit von Strukturklassen
Skript Seite 73
Sei (tau) die Klasse aller tau-Strukturen. Eine Strukturklasse K teilmenge (tau) ist FO-Axiomatisierbar (oder einfach axiomatisierbar), wenn eine Satzmenge PHI teilmenge FO(tau) existiert, so dass K = Mod(PHI).
Wenn das Axiomensystem PHI für K endlich ist, dann können wir die Konjunktion psi = UND{phi: phi element PHI} bilden und damit K durch einen einzigen Satz axiomatisieren. Wir sagen in diesem Fall, K ist elementar oder endlich axiomatisierbar.
Definition: Relation ist elementar definierbar (Skript Seite 75)
Eine Relation teilmenge A^r auf dem Universum einer tau-Struktur A~ ist (elementar) definierbar in A~, wenn R = psi^(A~) für eine Formel psi element FO(tau). Eine Funktion f: A^r -> A heisst elementar definierbar, wenn ihr Graph R_f elementar definierbar ist. (Der Graph ist eine Relation).
Insbesondere ist also eine Konstante a elementar definierbar, wenn eine Formel phi(x) element FO(tau) existiert, so dass A~ |= phi(a) und A~ |= nicht(phi(b)) für alle b != a.
Wir sagen, a ist termdefinierbar in A~, wenn ein Grundterm t element T(tau) existiert (also a als Konstante c, oder Ziel einer Funktion auf einer Konstanten f(c) =a in der Signatur vorhanden ist), so dass t^(A~) = a. Jede termdefinierbare Konstante ist insbesondere elementar definierbar durch eine Formel der form x=t.
Definition Isomorphismus (Skript Seite 78)
A~ und B~ seien tau-Strukturen. Ein Isomorphismus von A~ nach B~ ist eine bijektive Abbildung pi: A -> B, so dass folgende Bedingungen erfüllt sind:
(1) Für jedes n-stellige Relationssymbol R element tau und alle a1, …, an element A gilt:
(a1, … , an) element R^A~ gdw. (pi a1, …, pi an) element R^B~
(2) Für jedes n-stellige Funktionssymbol f element tau und alle a1, …, an element A gilt:
pi f^A~(a1, …, an) = f^B~(pi a1, …, pi an)
Lemma 3.9 Isomorphielemma (Skript Seite 79)
Sei pi: A~ -~> B~ ein Isomorphismus von tau-Strukturen. Dann gilt für alle psi(x1, …, xn) element FO(tau) und alle a1, …, an element A:
A~ |= psi(a1, …, an) gdw. B~ |= psi(pi a1, …, tau an)
Lemma 3.10 über Automorphismen und expandierte Strukturen (Skript Seite 80)
Sei pi ein Automorphismus einer tau-Struktur A~, und sei psi element FO(tau). Dann ist pi auch ein Automorphismus der expandierten Struktur (A~, psi^A~)
(psi~A~ ist elementar definierbar in A~. Kann benutzt werden in Beweisen zur elementaren Definierbarkeit. Z.b. wähle expandierte Struktur, wo psi elementar definierbar ist, aber ein Automorphismus im Redukt der Struktur kein Automorphismus in der expandierten Struktur mehr ist)
