Logik für Informatiker^{1}

Sätze und Definitionen

Martin Ziegler Freiburg 2006/2007

1version1.5-1-g570cfb7, Sat Oct 29 18:16:49 2016 +0200

Inhaltsverzeichnis

1 Aussagenlogik 2 1.1 Grundbegriffe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Äquivalente Formeln und Normalformen . . . . . . . . . . . . . . 5 1.3 Boolesche Algebren . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.4 Die Resolutionmethode . . . . . . . . . . . . . . . . . . . . . . . . 9 1.5 Der Satz von Cook . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.6 Der Kompaktheitsatz der Aussagenlogik . . . . . . . . . . . . . . 11

2 Prädikatenlogik 12 2.1 Strukturen und Formeln . . . . . . . . . . . . . . . . . . . . . . . 12 2.2 Semantik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.3 Allgemeingültige Formeln . . . . . . . . . . . . . . . . . . . . . . 20 2.4 Der Gödelsche Vollständigkeitssatz . . . . . . . . . . . . . . . . . 21 2.5 Der Herbrandsche Satz und automatisches Beweisen . . . . . . . 24

3 Unentscheidbarkeit der Prädikatenkalküls 26 3.1 Registermaschinen . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.2 Codierung von Registermaschinen . . . . . . . . . . . . . . . . . . 28 3.3 Turingmaschinen . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

Änderungen  31

Kapitel 1

Aussagenlogik

1.1 Grundbegriffe

Definition (Syntax…). Aussagenlogische Formeln sind Zeichenreihen, die sich aus den Variablen A_{0}, A_{1}, …, den Junktoren ∧, ∨ und ¬ und den beiden Klammern ( und ) nach den folgenden Regeln aufbauen.

• Variable sind Formeln.

• Wenn F_{1} und F_{2} Formeln sind, dann ist auch (F_{1} ∧ F_{2}) eine Formel (Konjunktion).

• Wenn F_{1} und F_{2} Formeln sind, dann ist auch (F_{1} ∨ F_{2}) eine Formel (Disjunktion).

• Wenn F eine Formel ist, dann ist auch ¬F eine Formel (Negation).

Man liest ∧ als „und“, ∨ als „oder“ und ¬ als „nicht“. Wir verwenden die folgenden Abkürzungen:

(F → G)  = (¬F ∨ G)  (Implikation)
(F ↔ G)  = ((F → G) ∧ (G → F))  (Äquivalenz)
⋀_{i<n} F_{i} = (F_{0} ∧ … ∧ (F_{n−2} ∧ F_{n−1}) …)
⋁_{i<n} F_{i} = (F_{0} ∨ … ∨ (F_{n−2} ∨ F_{n−1}) …)
⊤  = (A_{0} ∨ ¬A_{0})  (Wahr)
⊥  = (A_{0} ∧ ¬A_{0})  (Falsch)

Man liest → als „impliziert“ und ↔ als „äquivalent“. Gelegentlich fassen wir ⊤ und ⊥ als nicht–zusammengesetzte Formeln auf. Die leere Konjunktion ⋀_{i<0} F_{i} wird mit ⊤, die leere Disjunktion mit ⊥ identifiziert.

KAPITEL 1. AUSSAGENLOGIK 3

Wir könnten auf ∨ als Grundsymbol verzichten und (F ∨ G) als Abkürzung für ¬(¬F ∧ ¬G) auffassen. In der Prädikatenlogik (Kapitel 2) werden wir so verfahren. Hilfssatz. Eine Formel kann kein echtes Anfangsstück einer anderen Formel sein. Lemma 1.1.1 (Eindeutige Lesbarkeit von Formeln). Jede Formel ist entweder eine

• eine Variable,

• eine Konjunktion (F_{1} ∧ F_{2}),

• eine Disjunktion (F_{1} ∨ F_{2})

• oder eine Negation ¬F Die Formeln F_{1}, F_{2} bzw. F sind jeweils eindeutig bestimmt.

Wenn keine Mißverständnisse auftreten können, lassen wir gelegentlich Klammern weg. Definition. Die Wahrheitswerte 0 und 1 stehen für „falsch“ und „wahr“. Sei D eine Menge von Variablen. Eine Belegung ist eine Funktion A : D → {0, 1}.

Wir lassen die Junktoren auf den Wahrheitswerten wie folgt operieren:

w_{1} ∧ w_{2} = \begin{cases}1 & wenn w_{1} = 1 und w_{2} = 1 \\ 0 & sonst \end{cases}
w_{1} ∨ w_{2} = \begin{cases}1 & wenn w_{1} = 1 oder w_{2} = 1 \\ 0 & sonst \end{cases}
¬w = \begin{cases}1 & wenn w = 0 \\ 0 & wenn w = 1 \end{cases}

Mit Wahrheitstafeln drückt sich das so aus:

\begin{matrix}∧ & 0 & 1 \\ 0 & 0 & 0 \\ 1 & 0 & 1 \end{matrix}  \begin{matrix}∨ & 0 & 1 \\ 0 & 0 & 1 \\ 1 & 1 & 1 \end{matrix}  \begin{aligned}¬ & 0 & 1 \\ & 1 & 0 \end{aligned}

Definition (… und Semantik). Sei A eine Belegung der Variablen von F, dann ist der Wahrheitswert A(F) von F

• A(B), wenn F = B eine Variable ist,

• A(F_{1}) ∧ A(F_{2}), wenn F = (F_{1} ∧ F_{2}),

• A(F_{1}) ∨ A(F_{2}), wenn F = (F_{1} ∨ F_{2}), KAPITEL 1. AUSSAGENLOGIK 4

• ¬A(F′), wenn F = ¬F′.

Wenn A(F) = 1, sagen wir dafür auch „A erfüllt F “, „A ist Modell von F “ oder wir schreiben A ⊧ F. Definition. Eine Formel F heißt allgemeingültig oder (aussagenlogische) Tautologie, wenn alle Belegungen F erfüllen. F heißt erfüllbar, wenn es eine Belegung gibt, die F erfüllt. Lemma 1.1.2.

• F genau dann eine Tautologie, wenn ¬F nicht erfüllbar ist.

• F ist genau dann erfüllbar, wenn ¬F keine Tautologie ist.

1.2 Äquivalente Formeln und Normalformen

Definition. Zwei Formeln F und G heißen äquivalent, wenn sie dieselben Modelle haben. Wir schreiben dafür

F ≡ G

• F ≡ G genau dann, wenn F ↔ G allgemeingültig ist.

• F ist genau dann allgemeingültig, wenn F ≡ ⊤.

• F ist genau dann erfüllbar, wenn F ≢ ⊥.

• ≡ ist eine Äquivalenzrelation. Definition. Sei F eine Formel, aufgebaut aus ∧, ∨, ¬, ⊤ und ⊥. Die duale Formel F^{∗} entsteht aus F durch Vertauschen von ∧ und ∨ und von ⊤ und ⊥. Lemma 1.2.1. F ≡ G genau dann, wenn F^{∗} ≡ G^{∗}. Satz 1.2.2. Es gelten die folgenden grundlegenden Äquivalenzen und ihre Duale. (A, B, C sind Variable.)

(A ∧ A) ≡ A  (Idempotenz)
(A ∧ B) ≡ (B ∧ A)  (Kommutativität)
((A ∧ B) ∧ C) ≡ (A ∧ (B ∧ C))  (Assoziativität)
(A ∧ (A ∨ B)) ≡ A  (Absorption)
(A ∧ (B ∨ C)) ≡ ((A ∧ B) ∨ (A ∧ C))  (Distributivität)
(⊥ ∧ A) ≡ ⊥
(A ∧ ¬A) ≡ ⊥

A ∨ ¬A ≡ ⊤, das duale der letzten Äquivalenz heißt Tertium non datur. Definition. Seien F und H Formeln und A eine Variable. Dann bezeichnen wir mit F (H/A) die Formel, die aus F dadurch entsteht, daß wir jedes Vorkommen von A in F durch H ersetzen. Lemma 1.2.3 (Ersetzungslemma). F ≡ G impliziert F (H/A) ≡ G(H/A) und H(F/A) ≡ H(G/A).

Es gelten die de Morganschen Regeln

¬(A ∧ B) ≡ (¬A ∨ ¬B)
¬(A ∨ B) ≡ (¬A ∧ ¬B)
¬¬A ≡ A

Definition. Eine Literal ist ein Variable oder eine negierte Variable. Ein Formel der Form

⋁_{i<m} ⋀_{j<n_{i}} L_{ij}

für Literale L_{ij} hat disjunktive Normalform. Eine Formel der Form

⋀_{i<m} ⋁_{j<n_{i}} L_{ij}

hat konjunktive Normalform.

Satz 1.2.4. Jede Formel ist zu einer Formel in disjunktiver Normalform und zu einer Formel in konjunktiver Normalform äquivalent.

Folgerung 1.2.5. Jede Äquivalenz F ≡ G läßt sich mit Hilfe des Ersetzungslemmas 1.2.3 aus den Grundäquivalenzen von Satz 1.2.2 formal ableiten.

1.3 Boolesche Algebren

Definition. Eine Boolesche Algebra (B, 0, 1, ⊓, ⊔,^{c}) eine Menge B mit zwei ausgezeichneten Elementen 0 und 1 und Operationen ⊓, ⊔ : B^{2} → B und ^{c} : B → B, für die folgende Gleichungen gelten:

a ⊓ a = a  a ⊔ a = a  (1.1)
a ⊓ b = b ⊓ a  a ⊔ b = b ⊔ a  (1.2)
(a ⊓ b) ⊓ c = a ⊓ (b ⊓ c)  (a ⊔ b) ⊔ c = a ⊔ (b ⊔ c)  (1.3)
a ⊓ (a ⊔ b) = a  a ⊔ (a ⊓ b) = a  (1.4)
a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)  a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)  (1.5)
0 ⊓ a = 0  1 ⊔ a = 1  (1.6)
a ⊓ a^{c} = 0  a ⊔ a^{c} = 1  (1.7)

Die Axiome entsprechen den grundlegenden Äquivalenzen von Satz 1.2.2. Das zweite Distributivitätsaxiom ist überflüssig. In Booleschen Algebren gelten die de Morganschen Regeln.

Eine Struktur (V, ⊓, ⊔), in der (1.1), (1.2), (1.3) und (1.4) gelten, ist ein Verband. Wenn (P, ≤) eine partielle Ordnung ist, in der je zwei Element ein Supremum und ein Infimum haben, ist (P, inf, sup) ein Verband. Jeder Verband hat diese Gestalt, wenn man a ≤ b durch a ⊓ b = a oder, äquivalent, durch a ⊔ b = b definiert. Die Gleichungen (1.6) bedeuten, daß 0 und 1 kleinstes und größtes Element sind; (1.7) drückt aus, daß a^{c} ein Komplement von a ist. In einem distributiven Verband, d.h. in einem Verband, in dem (1.5) gilt, gibt es immer nur höchstens ein Komplement. Eine Boolesche Algebra ist also nichts anderes als ein „komplementärer distributiver Verband“.

Beispiel 1: Sei X eine Menge. Dann ist die Potenzmenge 𝔓(X) zusammen mit den ausgezeichneten Elementen ∅ und X und den Operationen Durchschnitt, Vereinigung und Komplement A^{c} = X \ A eine Boolesche Algebra, die Potenzmengenalgebra von X.

Satz 1.3.1. Endliche Boolesche Algebren sind isomorph zu Potenzmengenalgebren. Jede unendliche Boolesche Algebra ist isomorph zu einer Unteralgebra einer Potenzmengenalgebra.

Beispiel 2: Die Elemente der Lindenbaumalgebra LA_{n} sind Äquivalenzklassen F/≡ von Formeln F, die höchstens die Variablen A_{0}, …, A_{n−1} enthalten. Wenn man definiert

0 = ⊥/≡
1 = ⊤/≡
(F/≡) ⊓ (G/≡) = (F ∧ G)/≡
(F/≡) ⊔ (G/≡) = (F ∨ G)/≡
(F/≡)^{c} = ¬F/≡,

KAPITEL 1. AUSSAGENLOGIK 8 wird LA_{n} zu einer Booleschen Algebra. LA_{n} ist isomorph zur Potenzmengenalgebra einer Menge mit 2^{n} Elementen. LA_{n} wir von den A_{i}/≡ „frei“ erzeugt.

1.4 Die Resolutionmethode

Definition. Eine Klausel C ist eine endliche Menge von Literalen.

Eine Belegung A der Variablen erfüllt die Klausel C, wenn A(L) = 1 für ein L ∈ C. Anders ausgedrückt, wenn A ⊧ ⋁_{L∈C} L. Sei C eine Menge von Klauseln. A erfüllt C, wenn A alle C ∈ C erfüllt. Das kann man auch schreiben als

A ⊧ ⋀_{C∈C} ⋁_{L∈C} L.

Definition. Sei A eine Variable, C = {A}∪P und D = {¬A}∪Q zwei Klauseln. Dann ist P ∪ Q eine Resultante von C und D.

Satz 1.4.1 (Die Resolutionsmethode). Eine endliche Menge C von Klauseln ist genau dann erfüllbar, wenn sich aus C durch sukzessives Bilden von Resultanten niemals die leere Klausel ergibt.

Der Beweis beruht auf folgender Beobachtung: Sei mit C|A = 1 die Menge der Klauseln bezeichnet, die man aus C erhält, wenn man A = 1 setzt. Das heißt, daß man alle Klauseln, in denen A vorkommt, wegläßt und in den verbleibenden Klauseln alle Vorkommen von ¬A streicht. Entsprechend sei C|A = 0 definiert. Dann gilt das folgende Lemma.

Lemma 1.4.2.

• Sei A eine Belegung der Variablen von C und A(A) = w. Dann ist A ein Modell von C von A genau dann, wenn A ein Modell von C|A = w ist.

• Aus C ergibt sich durch sukzessives Bilden von Resultanten genau dann die leere Klausel, wenn das gleiche für C|A = 1 und für C|A = 0 gilt.

1.5 Der Satz von Cook

Definition. Sei 𝔸 ein endliches Alphabet und W ⊂ 𝔸^{∗} eine Menge von Wörtern. W heißt polynomial, wenn es eine Maschine M mit polynomialer Laufzeit^{1} gibt, die für jedes w entscheidet, ob w ∈ W. Wir schreiben dann

W ∈ P.

Definition. W heißt nicht–deterministisch polynomial , wenn es eine nicht– deterministische^{2} Maschine mit polynomialer Laufzeit gibt, sodaß w ∈ W genau dann, wenn M mit Input w einen Lauf hat, der w akzeptiert. Wir schreiben

W ∈ NP

Es ist klar, daß P eine Teilmenge von NP ist.

Um aussagenlogische Formeln in einem endlichen Alphabet zu schreiben, verwenden wir statt der Variablen A_{0}, A_{1}, … nicht–leere Wörter über einem vernünftigen Alphabet, zum Beispiel {A, B, …, Z}. Es ist klar, daß die Menge aller Formeln zu P gehört. Die Menge

SAT

aller erfüllbaren Formeln gehört zu NP.

Satz 1.5.1 (Cook). SAT ist NP-vollständig. Das heißt: Sei W ∈ NP. Dann läßt sich jedes Wort w in polynomialer Zeit in eine Formel F umwandeln, sodaß

w ∈ W ⇔ F ∈ SAT.

Folgerung 1.5.2. NP = P ist äquivalent zu SAT ∈ P.

Das Erfüllbarkeitsproblem einer Formel in konjunktiver Normalform ist ebenfalls NP-vollständig:

Proposition 1.5.3. Zu jeder Formel läßt sich in polynomialer Zeit eine Menge von Klauseln angeben, die genau dann erfüllbar ist, wenn F erfüllbar ist.

1Es gibt ein Polynom p(x), sodaß die Maschine bei Input w nach höchstens p(|w|) vielen Schritten stoppt.

2Das Programm einer solchen Maschine enthält Befehle, die nicht zwingend ausgeführt werden müssen.

1.6 Der Kompaktheitsatz der Aussagenlogik

Satz 1.6.1 (Kompaktheitssatz). Eine (unendliche) Menge von Formeln ist genau dann erfüllbar, wenn jede endliche Teilmenge erfüllbar ist.

Der Satz gilt auch, wenn man überabzählbar viele Variablen zuläßt. Man braucht dazu

Hilfssatz (Zorns Lemma). Sei (P, ≤) eine partiell geordnete Menge. Wenn jede linear geordnete Teilmenge von P eine obere Schranke hat, hat P ein maximales Element.

Definition. Sei T eine Menge von Formeln. Eine Formel F folgt aus T, wenn jedes Modell von T auch ein Modell von F ist.

Wir schreiben dafür

T ⊢ F.

Folgerung 1.6.2. Wenn F aus T folgt, dann folgt F schon aus einer endlichen Teilmenge von T.

Die nächste Proposition ist ein Anwendungsbeispiel. Ein Graph ist f–färbbar, wenn man jeder seiner Ecken eine der Farben 1, 2, …, f so zuordnen kann, daß verbundene Ecken verschiedene Farben haben.

Proposition 1.6.3. Sei f eine natürliche Zahl. Ein Graph G ist genau dann f–färbbar, wenn jeder endliche Teilgraph von G f–färbbar ist.

Prädikatenlogik

2.1 Strukturen und Formeln

Definition. Eine Sprache L ist eine Menge von Konstanten, Funktionszeichen und Relationszeichen. Funktionszeichen und Relationszeichen haben eine (positive) Stelligkeit.

Definition. Sei L eine Sprache. Eine L–Struktur ist ein Paar

𝔄 = (A, (Z^{𝔄})_{Z∈L}),

wobei

A  eine nicht–leere Menge (die Grundmenge von 𝔄 ) ist,
Z^{𝔄} ∈ A,  wenn Z eine Konstante ist,
Z^{𝔄} : A^{n} ⟶ A, wenn Z ein n–stelliges Funktionszeichen ist und
Z^{𝔄} ⊂ A^{n},  wenn Z ein n–stelliges Relationszeichen ist.

Definition. Zwei L–Strukturen 𝔄 und 𝔅 heißen isomorph, 𝔄 ≅ 𝔅, wenn es einen Isomorphismus F : 𝔄 ⟶ 𝔅 gibt, eine Bijektion F : A ⟶ B, die mit den Interpretationen der Zeichen aus L kommutiert:

F (Z^{𝔄})  = Z^{𝔅}  (Z eine Konstante aus L)

F (Z^{𝔄}(a_{1}, …, a_{n})) = Z^{𝔅}(F (a_{1}), …, F (a_{n})) (Z ein n–stelliges Funktionszeichen aus L, a_{1}, …, a_{n} ∈ A)

R^{𝔄}(a_{1}, …, a_{n}) ⇔ R^{𝔅}(F (a_{1}), …, F (a_{n})) (Z ein n–stelliges Relationszeichen aus L, a_{1}, …, a_{n} ∈ A)

Ein Isomorphismus von 𝔄 mit sich selbst heißt Automorphismus.

Das Inverse eines Isomorphismus und die Verknüpfung von Isomorphismen sind wieder Isomorphismen. Daraus folgt, daß

Aut(𝔄), KAPITEL 2. PRÄDIKATENLOGIK 13

die Menge aller Automorphismen von 𝔄, eine Gruppe ist. Wir fixieren ein Folge von Variablen v_{0}, v_{1}, . . .. Definition. Ein L–Term ist eine Zeichenfolge, die nach den folgenden Regeln gebildet ist: T1 Jede Variable ist ein L–Term. T2 Jede Konstante aus L ist ein L–Term. T3 Wenn f ein n–stelliges Funktionszeichen aus L ist und wenn t_{1}, …, t_{n} L–

Terme sind, dann ist auch ft_{1} ⋯ t_{n} ein L–Term.

Um Terme besser lesbar zu machen, schreiben wir häufig f(t_{1}, …, t_{n}) statt ft_{1} ⋯ t_{n}. Wenn f einstellig ist, auch t_{1}f, wenn f zweistellig ist, auch t_{1}ft_{2}. Zum Beispiel steht (x + y) · (z + w) für · + xy + zw und (x ∘ y)^{−1} für ^{−1} ∘ xy. Lemma 2.1.1 (Eindeutige Lesbarkeit von Termen). Für jeden L–Term t tritt genau einer der folgenden drei Fälle ein:

1. t ist eine Variable,

2. t ist eine Konstante,

3. t = ft_{1} ⋯ t_{n}, wobei f ein n–stelliges Funktionszeichen und t_{1}, …, t_{n} L– Terme sind.

Im letzten Fall sind f und t_{1}, …, t_{n} eindeutig bestimmt.

Das Lemma folgt aus den nächsten Hilfsatz Hilfssatz. Kein L–Term ist echtes Anfangsstück eines anderen L–Terms.

L–Formeln sind Zeichenreihen, die aus den Zeichen aus L, den Klammern ( und ) als Hilfszeichen und den folgenden logischen Zeichen gebildet ist:

Variable  v_{0}, v_{1}, …
Gleichheitszeichen =^{.}
Junktoren  ¬ (Negation), ∧ (Konjunktion)
Existenzquantor  ∃

Man liest =^{.} als „gleich“, ¬ als „nicht“, ∧ als „und“ und ∃ als „es gibt ein“. Definition. Eine L–Formel ist F1 t_{1} =^{.} t_{2} , wenn t_{1}, t_{2} L–Terme sind,

F2 Rt_{1} …, t_{n}  , wenn R ein n–stelliges Relationszeichen aus L und t_{1}, …, t_{n} L–Terme sind,

F3 ¬ψ , wenn ψ eine L–Formel ist, F4 (ψ_{1} ∧ ψ_{2}) ,wenn ψ_{1} und ψ_{2} L–Formeln sind,

F5 ∃x ψ ,wenn ψ eine L–Formel und x eine Variable ist.

Formeln der Form F1 und F2 heißen Primformeln.

Wir verwenden folgende Abkürzungen:

(ψ_{1} ∨ ψ_{2}) = ¬(¬ψ_{1} ∧ ¬ψ_{2})
(ψ_{1} → ψ_{2}) = ¬(ψ_{1} ∧ ¬ψ_{2})
(ψ_{1} ↔ ψ_{2}) = ((ψ_{1} → ψ_{2}) ∧ (ψ_{2} → ψ_{1}))
∀x ψ = ¬∃x¬ψ
(ψ_{0} ∧ ⋯ ∧ ψ_{n}) = \underbrace{(⋯ (}_{n -mal} ψ_{0} ∧ ψ_{1}) ∧ ⋯ ψ_{n})
(ψ_{0} ∨ ⋯ ∨ ψ_{n}) = \underbrace{(⋯ (}_{n -mal} ψ_{0} ∨ ψ_{1}) ∨ ⋯ ψ_{n})

Die Disjunktion ∨ liest man als „oder“, die Implikation → als „impliziert“, die Äquivalenz ↔ als „genau dann, wenn“ und den Allquantor ∀ als „für alle“.

Statt Rt_{1}t_{2} schreiben wir auch t_{1}Rt_{2} und statt ∃x_{1} ⋯ ∃x_{n} schreiben wir ∃x_{1} … x_{n} (ebenso für ∀). Zur besseren Lesbarkeit der Formeln gebrauchen wir überflüssige Klammern. Wir lassen auch Klammern weg und lesen die Formeln gemäß der Bindungsstärke der logischen Zeichen:

Höchste Bindungsstärke:  ¬ ∃ ∀
∧
∨
Niedrigste Bindungsstärke:  → ↔

Zum Beispiel steht ¬ϕ ∧ ψ → χ für

((¬ϕ ∧ ψ) → χ) = ¬((¬ϕ ∧ ψ) ∧ ¬χ).

Lemma 2.1.2 (Eindeutige Lesbarkeit von Formeln). Für jede L–Formel ϕ tritt genau einer der folgenden Fälle ein.

1. ϕ = t_{1} =^{.} t_{2} für L–Terme t_{1}, t_{2}

2. ϕ = Rt_{1} ⋯ t_{n}  für ein n–stelliges Relationszeichen R aus L und L–Terme t_{1}, …, t_{n}

3. ϕ = ¬ψ für eine L–Formel ψ

4. ϕ = (ψ_{1} ∧ ψ_{2}) für L–Formeln ψ_{1} und ψ_{2}

5. ϕ = ∃x ψ für eine L–Formel ψ und eine Variable x

In jedem der Fälle sind die Terme t_{i}, das Relationszeichen R, die Formeln ψ, ψ_{1}, ψ_{2} und die Variable x jeweils eindeutig bestimmt.

KAPITEL 2. PRÄDIKATENLOGIK 15

Zum Beweis braucht man den folgenden Hilfssatz. Hilfssatz. Keine L–Formel ist echtes Anfangsstück einer anderen L–Formel.

KAPITEL 2. PRÄDIKATENLOGIK 16

2.2 Semantik

Definition. Sei 𝔄 eine L–Struktur. Eine Belegung ist eine Funktion

β : {v_{0}, v_{1} … } ⟶ A

von der Menge der Variablen in die Grundmenge von 𝔄. Definition. Für L–Terme t, L–Strukturen 𝔄 und Belegungen β definieren wir t^{𝔄}[β] durch

v_{i}^{𝔄}[β] = β(v_{i})
c^{𝔄}[β] = c^{𝔄}
ft_{1} ⋯ t_{n}^{𝔄}[β] = f^{𝔄}(t_{1}^{𝔄}[β], …, t_{n}^{𝔄}[β]).

Lemma 2.2.1. Wenn die Belegungen β und γ auf den Variablen, die in t vorkommen übereinstimmen, ist t^{𝔄}[β] = t^{𝔄}[γ].

Wenn wir einen Term in der Form t(x_{1}, …, x_{n}) schreiben, meinen wir:

1. daß die x_{i} paarweise verschiedene Variable sind,

2. daß in t nur Variable aus {x_{1}, …, x_{n}} vorkommen. Wenn dann a_{1}, …, a_{n} Elemente der Struktur 𝔄 sind, ist wegen 2.2.1

t^{𝔄}[a_{1}, …, a_{n}]

durch t^{𝔄}[β] für eine Belegung β mit β(x_{i}) = a_{i} wohldefiniert.

Die folgende rekursive Definition der Semantik von Formeln ist sinnvoll, wegen 2.1.2. Definition. Sei 𝔄 eine L–Struktur. Wir definieren für Belegungen β und L– Formeln ϕ die Relation

𝔄 ⊧ ϕ[β]

— ϕ trifft in 𝔄 auf β zu— durch Rekursion über den Aufbau von ϕ:

𝔄 ⊧ t_{1} =^{.} t_{2} [β] ⇔ t_{1}^{𝔄}[β] = t_{2}^{𝔄}[β]
𝔄 ⊧ Rt_{1} ⋯ t_{n} [β] ⇔ R^{𝔄}(t_{1}^{𝔄}[β], …, t_{n}^{𝔄}[β])
𝔄 ⊧ ¬ψ [β] ⇔ 𝔄 |̸= ψ [β]
𝔄 ⊧ (ψ_{1} ∧ ψ_{2}) [β] ⇔ 𝔄 ⊧ ψ_{1} [β] und 𝔄 ⊧ ψ_{2} [β]
𝔄 ⊧ ∃xψ [β] ⇔ es gibt ein a ∈ A mit 𝔄 ⊧ ψ [β \frac{a}{x}].

Dabei ist β \frac{a}{x}(y) = \begin{cases}β(y) & , wenn y ≠ x \\ a & , wenn y = x. \end{cases}

KAPITEL 2. PRÄDIKATENLOGIK 17

Definition. Die Variable x kommt frei in der Formel ϕ vor, wenn sie an einer Stelle vorkommt, die nicht im Wirkungsbereich eines Quantors ∃x liegt. Präzis definiert durch Rekursion nach dem Aufbau von ϕ:

x frei in t_{1} =^{.} t_{2} ⇔ x kommt in t_{1} oder in t_{2} vor
x frei in Rt_{1} ⋯ t_{n} ⇔ x kommt in einem der t_{i} vor.
x frei in ¬ψ ⇔ x frei in ψ
x frei in (ψ_{1} ∧ ψ_{2}) ⇔ x frei in ψ_{1} oder x frei in ψ_{2}
x frei in ∃y ψ ⇔ x ≠ y und x frei in ψ

Satz 2.2.2. Wenn β und γ an allen Variablen, die frei in ϕ vorkommen, übereinstimmen, ist

𝔄 ⊧ ϕ[β] ⇔ 𝔄 ⊧ ϕ[γ].

Wenn wir eine Formel in der Form ϕ(x_{1}, …, x_{n}) schreiben, meinen wir:

1. daß die x_{i} paarweise verschiedene Variable sind,

2. daß in ϕ nur Variable aus {x_{1}, …, x_{n}} frei vorkommen. Wenn dann a_{1}, …, a_{n} Elemente der Struktur 𝔄 sind, ist wegen 2.2.2

𝔄 ⊧ ϕ[a_{1}, …, a_{n}]

durch 𝔄 ⊧ ϕ[β] für eine Belegung β mit β(x_{i}) = a_{i} wohldefiniert. Definition. Eine Aussage ϕ ist eine Formel ohne freie Variable. Wir schreiben 𝔄 ⊧ ϕ, wenn 𝔄 ⊧ ϕ[β] für ein (alle) β.

Sprechweisen:

• ϕ gilt in 𝔄.

• ϕ ist wahr in 𝔄.

• 𝔄 ist Modell von ϕ.

• 𝔄 erfüllt ϕ.

Zwei L–Strukturen 𝔄 und 𝔅 heißen elementar äquivalent, wenn in ihnen die gleichen Aussagen gelten. Lemma 2.2.3. Isomorphe Strukturen sind elementar äquivalent.

Sei x eine Variable und s ein Term. Dann entsteht der Term

t\frac{s}{x}

aus t durch Ersetzen aller Vorkommen von x durch s.

Lemma 2.2.4 (Substitutionslemma für Terme). Sei x eine Variable, s ein Term und β eine Belegung mit Werten in der Struktur 𝔄. Dann ist für jeden Term T

(t\frac{s}{x})^{𝔄}[β] = t^{𝔄}[β \frac{s^{𝔄}[β]}{x}].

Sei t = t(x_{1}, …, x_{n}), und s = s(x_{1}, …, x_{n}). Dann kann man das Substitutionslemma schreiben als

t(s, x_{2}, …, x_{n})^{𝔄}[a_{1}, …, a_{n}] = t^{𝔄}[s^{𝔄}[a_{1}, …, a_{n}], a_{2}, …, a_{n}].

Die Formel

ϕ\frac{s}{x}

entsteht aus ϕ durch Ersetzen aller freien Vorkommen von x durch s.

Die rekursive Definition von ϕ\frac{s}{x} ist

(t_{1} =^{.} t_{n})\frac{s}{x} = t_{1} \frac{s}{x} =^{.} t_{2} \frac{s}{x}
(Rt_{1} ⋯ t_{n})\frac{s}{x} = Rt_{1} \frac{s}{x} ⋯ t_{n} \frac{s}{x}
(¬ψ)\frac{s}{x} = ¬(ψ \frac{s}{x})
(ψ_{1} ∧ ψ_{2})\frac{s}{x} = (ψ_{1} \frac{s}{x} ∧ ψ_{2} \frac{s}{x})
(∃yψ)\frac{s}{x} = ∃y(ψ \frac{s}{x}), wenn x ≠ y
= ∃yψ, wenn x = y.

Definition. x heißt frei für s in ϕ, wenn kein freies Vorkommen von x in ϕ im Wirkungsbereich eines Quantors ist, der eine Variable von s bindet.

Rekursive Definition: x ist frei für s in ϕ, wenn x nicht frei in ϕ ist oder wenn x frei in ϕ ist und einer der folgenden Fälle zutrifft

ϕ = t_{1} =^{.} t_{n}
ϕ = Rt_{1} ⋯ t_{n}
ϕ = ¬ψ und x frei für s in ψ
ϕ = (ψ_{1} ∧ ψ_{2}) und x frei für s in ψ_{1} und ψ_{2},
ϕ = ∃yψ, x frei für s in ψ und y kommt nicht in s vor.

Lemma 2.2.5 (Substitutionslemma für Formeln). Sei x eine Variable, s ein Term und β eine Belegung mit Werten in der Struktur 𝔄. Wenn x frei für s in der Formel ϕ, ist

𝔄 ⊧ ϕ\frac{s}{x}[β] ⟺ 𝔄 ⊧ ϕ[β \frac{s^{𝔄}[β]}{x}],

KAPITEL 2. PRÄDIKATENLOGIK 19

Sei ϕ = ϕ(x_{1}, …, x_{n}) und s = s(x_{1}, …, x_{n}). Dann kann man das Substitutionslemma schreiben als

𝔄 ⊧ ϕ(s, x_{2}, …, x_{n})[a_{1}, …, a_{n}] ⟺ 𝔄 ⊧ ϕ[s^{𝔄}[a_{1}, …, a_{n}], a_{2}, …, a_{n}].

2.3 Allgemeingültige Formeln

Definition. Eine Formel ϕ heißt allgemeingültig, wenn sie für alle Belegungen β in allen Strukturen^{1} 𝔄 gilt. Wir schreiben dafür

⊧ ϕ.

ϕ(x_{1}, …, , x_{n}) ist genau dann allgemeingültig, wenn die Aussage ∀x_{1} … x_{n}ϕ(x_{1}, …, x_{n}) allgemeingültig ist.

Definition. Eine (prädikatenlogische) Tautologie entsteht aus einer aussagenlogischen Tautologie durch Ersetzen der Aussagenvariablen durch L–Formeln.

Lemma 2.3.1. Tautologien sind allgemeingültig.

Lemma 2.3.2 (Axiome der Gleichheit). Die folgenden L–Aussagen sind allgemeingültig.

Reflexivität ∀x x =^{.} x
Symmetrie ∀x, y x =^{.} y → y =^{.} x
Transitivität ∀x, y, z x =^{.} y ∧ y =^{.} z → x =^{.} z

∀x_{1}, …, x_{n}, y_{1}, … y_{n} x_{1} =^{.} y_{1} ∧ ⋯ ∧ x_{n} =^{.} y_{n}

⟶ fx_{1} … x_{n} =^{.} fy_{1} … y_{n}

∀x_{1}, …, x_{n}, y_{1}, … y_{n} x_{1} =^{.} y_{1} ∧ ⋯ ∧ x_{n} =^{.} y_{n}

⟶ (Rx_{1} … x_{n} ↔ Ry_{1} … y_{n})

Dabei sind die f n–stellige Funktionszeichen und die R n–stellige Relationszeichen aus L.

Die ersten drei Aussagen drücken aus, daß = eine Äquivalenzrelation ist. Die beiden letzten bedeuten, daß = eine Kongruenzrelation ist.

Lemma 2.3.3 (∃–Quantorenaxiome). ϕ sei eine L–Formel, t ein L–Term und x frei für t in ϕ. Dann ist

ϕ\frac{t}{x} ⟶ ∃xϕ

allgemeingültig.

Lemma 2.3.4 (Modus Ponens). Wenn ϕ und (ϕ → ψ) allgemeingültig sind, dann auch ψ.

Lemma 2.3.5 (∃–Einführung). Wenn x nicht frei in ψ vorkommt, dann ist mit ϕ → ψ auch ∃xϕ → ψ allgemeingültig.^{2}

1Wenn ϕ eine L–Formel ist, sind L–Strukturen gemeint. Der Begriff hängt von der Wahl von L nicht ab.

2Man spricht von Existenzeinführung.

2.4 Der Gödelsche Vollständigkeitssatz

Definition (Der Hilbertkalkül). L sei eine Sprache. Eine L–Formel ist beweisbar, wenn sie

B1 eine Tautologie ist,

B2 ein Gleichheitsaxiom ist,

B3 ein ∃–Quantorenaxiom ist,

B4 sich mit Hilfe der Modus Ponens Regel aus zwei beweisbaren L–Formeln ergibt,

B5 oder wenn sie sich mit der Regel der ∃–Einführung aus einer beweisbaren L–Formel ergibt.

B1-B3 sind die Axiome , B4-B5 die Schlußregeln des Hilbertkalküls.

Eine Formel ϕ ist also genau dann beweisbar, wenn sie eine Beweis hat, das heißt, eine Folge

ϕ_{0}, …, ϕ_{n} = ϕ

von L–Formeln ϕ_{i}, die entweder Axiome sind oder mit einer der beiden Schlußregel aus Formeln ϕ_{j} (j < i) folgen. Wir schreiben:

⊢_{L} ϕ

Satz 2.4.1 (Gödelscher Vollständigkeitssatz). Ein Formel ist genau dann allgemeingültig, wenn sie beweisbar ist:^{3}

⊧ ϕ ⟺ ⊢_{L} ϕ

Die die Richtung ⇐ folgt aus 2.3.1, 2.3.2, 2.3.3, 2.3.4 und 2.3.5. Zum Beweis der Umkehrung macht man Gebrauch von den folgenden abgeleiteten Axiome und Regeln.

Lemma 2.4.2. 1. (Aussagenlogik) Wenn ϕ_{1},…,ϕ_{n} beweisbar sind und (ϕ_{1} ∧ ⋯ ∧ ϕ_{n}) → ψ eine Tautologie ist, ist auch ψ beweisbar.

2. (∀–Quantorenaxiome) Wenn x frei für t in ϕ, ist

⊢_{L} ∀xϕ → ϕ\frac{t}{x}.

3. (∀–Einführung) Wenn x nicht frei in ϕ ist, dann folgt aus der Beweisbarkeit von ϕ → ψ die Beweisbarkeit von ϕ → ∀xψ. Insbesondere folgt aus der Beweisbarkeit von ψ die Beweisbarkeit von ∀xψ.

3Es folgt, daß ⊢_{L} ϕ von der Sprachumgebung unabhängig ist. Wir verwenden darum später die Notation ⊢ ϕ.

Beweisschema des Gödelschen Vollständigkeitssatzes Nehmen wir an ϕ(x̄) sei nicht beweisbar. Wir müssen eine Struktur 𝔄 und Elemente ā ∈ A finden mit 𝔄 ⊧ ¬ϕ[ā].

Schritt 1) Wir wählen eine Folge c̄ von neuen Konstanten. Dann ist ϕ(c̄) ebenfalls nicht beweisbar. (Das folgt aus 2.4.3).

Schritt 2) Wir erweitern {¬ϕ(c̄)} zu einer widerspruchsfreien Henkintheorie mit Konstantenmenge C. (Die Definitionen folgen unten.)

Schritt 3) Wir erweitern T^{+} zu einer vollständigen Henkintheorie T^{∗}.

Schritt 4) Wir konstruieren ein Modell^{4} (𝔄, a_{c})_{c∈C} von T^{∗}.

In 𝔄 gilt ¬ϕ[ac̄].

Lemma 2.4.3. Sei ϕ(x_{1}, …, x_{n}) eine L–Formel, C eine Menge von neuen Konstanten und c_{1}, …, c_{n} eine Folge von paarweise verschiedenen Elementen von C. Dann ist

⊢_{L∪C} ϕ(c_{1}, …, c_{n}) ⟺ ⊢_{L} ϕ(x_{1}, …, x_{n}).

Definition. Eine L–Theorie ist eine Menge von L–Aussagen. Eine Aussage ϕ ist in T beweisbar,

T ⊢ ϕ,

wenn es Axiome ψ_{1}, …, ψ_{n} aus T gibt für die ⊢_{L} ψ_{1} ∧ ⋯ ∧ ψ_{n} → ϕ.^{5}

Definition. Eine L–Theorie T heißt widerspruchsfrei oder konsistent, wenn ⊥ nicht in T beweisbar ist.^{6} T ist vollständig, wenn T widerspruchsfrei ist und T ⊢ ϕ oder T ⊢ ¬ϕ für alle L–Aussagen ϕ.

Definition. Sei C eine Menge von Konstanten. Eine L ∪ C–Theorie T^{+} heißt Henkintheorie mit Konstantenmenge C, wenn es zu jeder L ∪ C–Formel ϕ(x) eine Konstante c ∈ C mit

T^{+} ⊢ ∃xϕ(x) → ϕ(c)

gibt.

Definition. Ein Modell von T ist eine L–Struktur, in der alle Aussagen aus T gelten.

Der skizzierte Beweis zeigt die folgende Verschärfung von 2.4.1.

∃x ¬x =^{.} x.

4Die Konstruktion liefert A = {a_{c}|c ∈ C}. Solche Modelle aus Konstanten sind durch T^{∗} bis auf Isomorphie eindeutig bestimmt.

5Man beachte, daß es wegen 2.4.2.1 auf die Klammerung und Reihenfolge der ϕ_{i} nicht ankommt.

6Wir nehmen für ⊥ irgendeine L–Aussage, deren Negation allgemeingültig ist. Zum Beispiel

Satz 2.4.4. Eine Theorie hat genau dann ein Modell, wenn sie widerspruchsfrei ist.

Definition. Die Aussage ϕ folgt logisch aus T,

T ⊧ ϕ,

wenn ϕ in allen Modellen von T gilt.

Folgerung 2.4.5.

T ⊢ ϕ  ⇔  T ⊧ ϕ

Folgerung 2.4.6 (Kompaktheitssatz). Eine Theorie hat genau dann ein Modell, wenn jede endliche Teilmenge ein Modell hat.

Den Kompaktheitssatz könnte man den ersten Hauptsatz der Modelltheorie nennen. Der zweite Hauptsatz wäre der Satz von Löwenheim-Skolem, aus dem Beweis von 2.4.4 folgt.

Folgerung 2.4.7 (Löwenheim-Skolem). Wenn eine Theorie mit höchstens abzählbarer Sprache eine Modell hat, hat sie ein abzählbares Modell

Folgerung 2.4.8 (aus 2.4.1). Sei L eine endlichen Sprache, dann ist die Menge der allgemeingültigen L–Aussagen effektiv aufzählbar.

Die Folgerung gilt auch für effektiv aufgezählte Sprachen.

2.5 Der Herbrandsche Satz und automatisches Beweisen

Definition. Eine Formel ist in pränexer Normalform, wenn alle Quantoren am Anfang der Formel stehen, wenn also die Formel die Gestalt

Q_{1}x_{1}Q_{2}x_{2} … Q_{n}x_{n}ψ

hat, mit quantorenfreiem ψ und Q_{i} ∈ {∃, ∀}.

Lemma 2.5.1 (Pränexe Normalform). Jede Formel läßt sich in eine äquivalente^{7} pränexe Formel umwandeln.

Definition. Eine universelle Formel hat die Form

∀x_{1} … ∀x_{n}ψ,

wobei ψ eine quantorenfreie Formel ist. Existentielle Formeln beginnen mit Existenzquantoren.

Satz 2.5.2 (Skolem–Normalform). Zu jeder L–Aussage ϕ kann man eine Spracherweiterung L^{∗} und einen universellen L^{∗}–Satz ϕ^{∗} angeben, derart, daß ϕ in einer L–Struktur 𝔄 genau dann gilt, wenn sich 𝔄 zu einem Modell von ϕ^{∗} expandieren läßt. ϕ ist also genau dann erfüllbar, wenn ϕ^{∗} erfüllbar ist.

Man nennt die im Beweis von 2.5.2 neu eingeführten Konstanten und Funktionszeichen in L^{∗} Skolemfunktionen.

Folgerung 2.5.3 (Herbrand–Normalform). Zu jeder L–Aussage ϕ kann man eine Spracherweiterung L^{∗} und einen existentiellen L^{∗}–Satz ϕ_{∗} angeben, der genau dann allgemeingültig ist, wenn ϕ allgemeingültig ist.

Satz 2.5.4 (Satz von Herbrand). Sei ψ(x_{1}, …, x_{n}) eine quantorenfreie^{8} Formel in einer Sprache L, die mindestens eine Konstante enthält. Dann ist

ϕ = ∃x_{1} … ∃x_{n}ψ(x_{1}, …, x_{n})

genau dann allgemeingültig, wenn es konstante Terme^{9}

t_{1}^{1}, t_{2}^{1}, … t_{n}^{1} … t_{1}^{N}, t_{2}^{N}, … t_{n}^{N}

gibt, für die die quantorenfreie Aussage

⋁_{i=1}^{N} ψ(t^{i}) = ψ(t_{1}^{1}, t_{2}^{1}, … t_{n}^{1}) ∨ ⋯ ∨ ψ(t_{1}^{N}, t_{2}^{N}, … t_{n}^{N})

allgemeingültig ist.

7ϕ und ψ sind äquivalent, wenn ϕ ↔ ψ allgemeingültig ist.

8Der Satz gilt auch für existentielle ψ.

9Ein konstanter Term ist ein Term ohne Variable.

Definition.

S^{1}(x_{1}, …, x_{n}) = (s_{1}^{1}(x_{1}, …, x_{n}), …, s_{k}^{1}(x_{1}, …, x_{n}))

und

S^{2}(x_{1}, …, x_{n}) = (s_{1}^{2}(x_{1}, …, x_{n}), …, s_{k}^{2}(x_{1}, …, x_{n}))

seien zwei gleichlange Folgen von Termen. Eine Termfolge T = (t_{1}, …, t_{n}) unifiziert S^{1} und S^{2}, wenn

S^{1}(t_{1}, …, t_{n}) = S^{2}(t_{1}, …, t_{n}).

Satz 2.5.5 (Unifikation). Wenn S^{1} und S^{2} unifizierbar sind, gibt es eine universelle unifizierende Termfolge U(y_{1}, …, y_{m}). Das heißt, daß eine Termfolge T genau dann S^{1} und S^{2} unifiziert, wenn es Terme r_{1}, …, r_{m} gibt, sodaß

T = U(r_{1}, …, r_{m}).

Man kann U durch ein einfaches Verfahren finden, das gleichzeitig entscheidet, ob S^{1} und S^{2} unifizierbar sind.

Lemma 2.5.6. Sei F (A_{1}, …, A_{n}) eine aussagenlogische Formel, in den paarweise verschiedenen Variablen A_{i}. Für jedes i sei α_{i} ein Primformel der Form^{10} Rt_{1} … t_{m}. Die α_{i} seien paarweise verschieden. Dann ist F (α_{1}, …, α_{n}) genau dann allgemeingütlig, wenn F (A_{1}, …, A_{n}) allgemeingültig ist.

Folgerung 2.5.7. Sei ψ(x_{1}, …, x_{n}) eine quantorenfreie L–Formel ohne Gleichheitszeichen und N eine natürliche Zahl^{11}. Man kann effektiv entscheiden, ob es konstante Terme

t_{1}^{1}, t_{2}^{1}, … t_{n}^{1} … t_{1}^{N}, t_{2}^{N}, … t_{n}^{N}

gibt, für die

⋁_{i=1}^{N} ψ(t^{i}) = ψ(t_{1}^{1}, t_{2}^{1}, … t_{n}^{1}) ∨ ⋯ ∨ ψ(t_{1}^{N}, t_{2}^{N}, … t_{n}^{N})

allgemeingültig ist.

Proposition 2.5.8. Wir finden in 2.5.3 immer ein ϕ_{∗} ohne Gleichheitszeichen.

10Das Lemma gilt für beliebige Primformeln α_{i}.

11Der Fall N = 1 impliziert sofort die Folgerung für beliebiges N. Wir haben diese Formulierung gewählt wegen des Zusammenhangs mit Satz 2.5.4.

Unentscheidbarkeit der Prädikatenkalküls

Wir zeigen in diesem Kapitel, daß es kein Verfahren gibt, das bei vorgelegter Aussage ϕ entscheidet, ob ϕ beweisbar ist.

3.1 Registermaschinen

Eine Registermaschine M arbeitet mit endlichen vielen Registern R_{0}, …, R_{R−1}, in denen Wörter aus einem endlichen Alphabet A = {a_{1}, …, a_{L}} stehen. Die Maschine kann den letzten Buchstaben dieser Wörter lesen, den letzten Buchstaben streichen oder einen Buchstaben anhängen^{1}. Das Programm von M ist eine Folge von Befehlen der folgenden Art.

PUSH(r,l) Wenn l = 0, wird der letzte Buchstabe des Worts in R_{r} gestrichen. Sonst wird das Wort in R_{r} um den Buchstaben a_{l} verlängert. Danach wird der nächste Befehl ausgeführt.

GOTO(r,c_{0},…,c_{L}) Liest das Wort in R_{r}. Wenn das Wort leer ist, führe als nächstes den Befehl mit der Nummer c_{0} aus. Wenn der letzte Buchstabe a_{l} ist, führe als nächstes den Befehl Nummer c_{l} aus.

STOP  Die Maschine stoppt.

Der letzte Befehl des Programms soll immer STOP sein.

1Die Register sind also „ stacks “.

KAPITEL 3. UNENTSCHEIDBARKEIT DER PRÄDIKATENKALKÜLS 27

M berechnet auf folgende Weise ein partielle Funktion

F_{M} : A^{∗} → A^{∗}.

Der Input x steht im Register R_{1}, die anderen Register sind leer. Die Maschine führt, mit dem ersten Befehl beginnend, das Programm solange aus, bis ein STOP–Befehl ausgeführt wird. Der Output F_{M}(x) steht dann in R_{0}. Wenn M nicht stoppt, ist F_{M}(x) undefiniert.

Satz 3.1.1 (Churchs These). Alle berechenbaren Funktionen^{2} A^{∗} → A^{∗} haben die Form F_{M} für eine geeignete Registermaschine M.

Folgerung 3.1.2 (Unlösbarkeit des Halteproblems). Sei A ein endliches Alphabet. Es gibt kein effektives Verfahren, das für alle Maschinen M und Wörter x entscheidet, ob M mit Input x stoppt.

Beweis. Nehmen wir an, daß es eine solches Verfahren gäbe. Dann gäbe es eine Maschine H, die genau dann bei Input M_{1}, M_{2} stoppt, wenn M_{1} mit Input M_{2} nicht stoppt. Sei N die Maschine, die bei Input M so rechnet wie H mit Input M, M. Dann stoppt N mit Input N genau dann, wenn es nicht stoppt. Widerspruch.

Folgerung 3.1.3. Sei A ein endliches Alphabet. Es gibt kein effektives Verfahren, das für alle Maschinen M entscheidet, ob M (mit leerem Input) stoppt.

Der Beweis von Folgerung 3.1.2 ist das gleiche Diagonalargument wie im Beweis des nächsten Satzes.

Satz 3.1.4 (Cantor). Die Menge alle unendlichen 0–1–Folgen ist überabzählbar.

Satz 3.1.5 (Fixpunktsatz von Kleene). Sei H eine berechenbare Funktion, die jedem Programm M ein Programm H(M) zuordnet. Dann gibt es ein Programm M_{0}, das dieselbe n–stellige Funktion berechnet wie H(M_{0}).

2Das gilt auch für „partielle berechenbare“ Funktionen.

3.2 Codierung von Registermaschinen

Satz 3.2.1. Zu jeder Registermaschine M läßt sich ein Aussage ϕ^{M} angeben, die genau dann erfüllbar ist, wenn M (mit leerem Input) nicht stoppt.

Man beachte, daß sowohl die Menge aller M, die stoppen, als auch die Menge aller ϕ, die nicht erfüllbar sind, effektiv aufzählbar sind.

Beweisskizze. Wir nehmen der Einfachheit halber an, daß L = 1, das heißt, daß A = {a_{1}} nur ein Zeichen enthält^{3}. Die Elemente von A^{∗} identifizieren wir mit natürlichen Zahlen. Sei b_{0}, …, b_{N} das Programm von M, R die Zahl der Register. Wir können annehmen,daß b_{N} der einzige Stopbefehl ist.

Sei

L^{M} = {0, f, z_{0}, …, z_{N}},

wobei 0 eine Konstante, f ein einstelliges Funktionszeichen und die z_{c} R–stellige Relationszeichen. Betrachte die folgende L^{M}–Struktur

𝔐^{0} = (ℕ, 0, (x ↦ x + 1), Z_{0}^{0}, …, Z_{N}^{0}),

wobei Z_{c}^{0}(n_{0}, …, n_{R−1}) genau dann, wenn M einen Zustand erreicht, in dem b_{c} der aktuelle Befehl ist und in Register R_{r} die Zahl n_{r} steht.

Man findet eine L^{M}–Aussage μ^{M} mit folgenden Eigenschaften:

• 𝔐^{0} ist ein Modell von μ^{M}.

• Wenn 𝔄 = (A, O, F, Z_{0}, …, Z_{N}) ein Modell von μ^{M} ist, gilt

Z_{c}^{0}(n_{0}, …, n_{R−1}) ⇒ Z_{c}(F^{n_{0}}(O), …, F^{n_{R−1}}(O)).

Man setzt nun ϕ^{M} = μ^{M} ∧ ∀x_{0}, …, x_{R−1}¬z_{N}(x_{0}, …, x_{R−1}).

Folgerung 3.2.2. Es gibt kein Verfahren, das bei vorgelegter Aussage ϕ entscheidet, ob ϕ allgemeingültig ist.

Folgerung 3.2.3 (aus dem Beweis). Es gibt eine endliche Sprache L, für die sich nicht entscheiden läßt, ob eine gegebene L–Aussage allgemeingültig ist.

Beweisskizze. Betrachte ein M, für das sich nicht entscheiden läßt, ob M bei gegebenem Input x stoppt. L = L^{M} sei wie oben gewählt. Konstruiere für jedes x eine Aussage ϕ^{x}, die genau dann erfüllbar ist, wenn M bei Input x nicht stoppt.

Satz 3.2.4. Es gibt eine endliche Sprache L, für die sich nicht entscheiden läßt, ob eine gegebene L–Aussage ein endliches Modell hat.

Beweisskizze. Sei M eine Maschine wie im Beweis von 3.2.3. Wir können annehmen, daß der Inhalt des Registers R_{0} während des Laufs immer größer wird. Wenn man μ^{x}, ähnlich wie im Beweis von 3.2.1, richtig wählt, hat μ^{x} genau dann ein endliches Modell, wenn M bei Input x stoppt.

3Sonst muß man L Funktionszeichen verwenden.

3.3 Turingmaschinen

Wir geben einen alternativen Beweis von 3.2.2 mit Hilfe von Turingmaschinen. Eine Turingmaschine M verwendet als Speicher ein Band von Zellen, auf denen sich ein Lese/Schreibkopf bewegt. Die Zellen sind leer oder enthalten einen Buchstaben aus einem Alphabet A = {a_{1}, …, a_{L}}. Das Programm von M ist eine Folge von Befehlen der folgenden Art.

WRITE(l) Wenn l = 0, wird die aktuelle Zelle gelöscht. Sonst wird der Buchstabe a_{l} in die Zelle geschrieben. Danach wird der nächste Befehl ausgeführt.

LEFT Der Kopf bewegt sich einen Schritt nach links. Danach wird der nächste Befehl ausgeführt.

RIGHT Der Kopf bewegt sich einen Schritt nach rechts. Danach wird der nächste Befehl ausgeführt.

GOTO(c_{0},...,c_{L}) Wenn die aktuelle Zelle leer ist, führe als nächstes den Befehl mit der Nummer c_{0} aus. Wenn die Zelle den Buchstaben a_{l} enthält, führe als nächstes den Befehl Nummer c_{l} aus.

STOP  Die Maschine stoppt.

Der letzte Befehl des Programms soll immer STOP sein

Satz 3.3.1. Registermaschinen lassen sich durch Turingmaschinen simulieren und umgekehrt.

Folgerung 3.3.2 (Unlösbarkeit des Halteproblems für Turingmaschinen). Sei A ein endliches Alphabet. Es gibt kein effektives Verfahren, das für alle Turingaschinen M entscheidet, ob M mit leerem Anfangsband stoppt.

Satz 3.3.3. Zu jeder Turingmaschine M läßt sich ein Aussage ψ^{M} angeben, die genau dann erfüllbar ist, wenn M nicht stoppt.

Beweisskizze. Wir können annehmen, daß L = 1. Sei b_{0}, …, b_{N} das Programm von M, b_{N} der einzige Stopbefehl. Sei

L^{M} = {0, <, z, h, d_{0}, …, d_{N}},

wobei 0 eine Konstante, < und die z zweistellige Relationen sind, h ein einstelliges Funktionszeichen und die d_{c} einstellige Relationszeichen. Betrachte die folgende L^{M}–Struktur

𝔐^{0} = {ℤ, 0, <, Z^{0}, H^{0}, D_{0}^{0}, …, D_{N}^{0}},

wobei • Z^{0}(s, n) genau dann, wenn nach s Schritten von M in der Zelle n ∈ ℤ der

Buchstabe a_{1} steht.

• H^{0}(s) ist die Position des Kopfes nach s Schritten, wenn s ≥ 0, sonst =0.

• D_{c}^{0}(s), wenn nach s Schritten b_{c} der aktuelle Befehl ist.

Wir stellen uns dabei vor, daß die Maschine nach einem Stop-befehl weiterläuft und „auf der Stelle tritt“.

Man findet eine L^{M}–Aussage μ^{M} mit folgenden Eigenschaften:

• 𝔐^{0} ist ein Modell von μ^{M}.

• Wenn 𝔄 = {A, ¯0, <, Z, H, D_{0}, …, D_{N}} ein Modell von μ^{M} ist, ist (M, <) eine lineare Ordnung, in der jedes Element einen unmittelbaren Vorgänger und Nachfolger hat. Sei für jedes n ∈ ℤ das Element n̄ der n–fache Nachfolger^{4} von ¯0. Die Unterstruktur {n̄ | n ∈ ℤ} ist isomorph zu 𝔐^{0}.

Man setzt nun ψ^{M} = μ^{M} ∧ ∀x¬z_{N}(x)

Wie im letzten Abschnitt folgt daraus 3.2.2, die Unentscheidbarkeit des Prädikatenkalküls.

4der −n–fache Vorgänger, wenn n < 0

Änderungen

20.11.2012 • Im Abschnitt 1.3, Beispiel 2, waren ⊤ und ⊥ vertauscht.

• Zwei Druckfehler in Beweis von 3.2.1 korrigiert.

Index

⋁_{i<n}, 2 F_{M}, 27 ⋀_{i<n}, 2 R_{r}, 26 T ⊢ F, 11 𝔄 ⊧ ϕ, 17 𝔄 ⊧ ϕ[β], 16 𝔄 ⊧ ϕ[a_{1}, …, a_{n}], 17 ≡, 5 ↔, 2, 14 A(F), 3 ∀, 14 ∀–Einführung, 21 ∀–Quantorenaxiom, 21 Aut(𝔄), 13 β \frac{a}{x}, 16 ⊢_{L} ϕ, 21 ⊢ ϕ, 21 ∨ ⋯ ∨, 14 ∃, 13 ∃–Einführung, 20 ∃–Quantorenaxiome, 20 ϕ(x_{1}, …, x_{n}), 17 ϕ\frac{s}{x}, 18 ⊥, 2, 22 F (H/A), 5 F^{∗}, 5

=^{.}, 13

→, 14 →, 2 (, 2 ), 2 ∧, 13 ∧ ⋯ ∧, 14 ⊧ ϕ, 20 ⊧, 4 ¬, 2, 3, 13 ∨, 2, 3, 14 𝔓(X), 7 t(x_{1}, …, x_{n}), 16 t\frac{s}{x}, 17 t^{𝔄}[β], 16 t^{𝔄}[a_{1}, …, a_{n}], 16 T ⊢ ϕ, 22 T ⊧ ϕ, 23 ∧, 2, 3 ⊤, 2 x ist frei für s in ϕ, 18

abgeleitete Axiome und Regeln, 21 Absorption, 5 Äquivalenz, 2, 14 äquivalente Formeln, 5, 24 allgemeingültige Formel, 4, 20 Allquantor, 14 Assoziativität, 5 Aussage, 17 aussagenlogische Formel, 2 Automorphismus, 12 Axiome des Hilbertkalküls, 21

Belegung, 3, 16 Beweis, 21 beweisbare Formel, 21 Beweisbarkeit, 21, 22 Bindungsstärke, 14 Boolesche Algebra, 7

Cantorscher Satz, 27 Churchs These, 27 Cookscher Satz, 10

de Morgansche Regeln, 5

Disjunktion, 2, 14 leere, 2 disjunktive Normalform, 6 distributiver Verband, 7 Distributivität, 5 duale Formel, 5

Eindeutige Lesbarkeit von Formeln, 3, 14 von Termen, 13

elementare Äquivalenz, 17 erfüllbare Formel, 4 Ersetzung, 5, siehe Substitution Ersetzungslemma, 5 existentielle Formel, 24 Existenzquantor, 13

färbbarer Graph, 11 Falsch, 2 Folgerung, 11 Formel

äquivalente, 5, 24 allgemeingültige, 4, 20 aussagenlogische, 2 beweisbare, 21 duale, 5 erfüllbare, 4 existentielle, 24 prädikatenlogische, 13 pränexe, 24 Semantik, 16 universelle, 24 Wahrheitswert, 3

freies Vorkommen, 17 Funktionszeichen, 12

Gödelscher Vollständigkeitssatz, 21 Gleichheitsaxiome, 20 Gleichheitszeichen, 13, 25 GOTO(c_{0},…,c_{L}), 29 GOTO(r,c_{0},…,c_{L}), 26 Graph

färbbarer, 11 Grundmenge, 12 Gültigkeit, 17

Halteproblem, 27 für Turingmaschinen, 29 Henkintheorie, 22 Herbrand–Normalform, 24 Herbrandscher Satz, 24 Hilbertkalkül, 21

Idempotenz, 5 Implikation, 2, 14 Isomorphie, 12 Isomorphismus, 12

Junktor, 2, 13

Klammer, 2 Klammern, 13, 14 Klausel, 9 Kommutativität, 5 Kompaktheitssatz

der Aussagenlogik, 11 Komplement, 7 Kongruenzrelation, 20 Konjunktion, 2, 13

leere, 2 konjunktive Normalform, 6 konsistente Theorie, 22 Konstante, 12 konstanter Term, 24

leere Disjunktion, 2 leere Konjunktion, 2

LEFT, 29

L–Formel, 13 Lindenbaumalgebra, 7 Literal, 6 logische Folgerung, 23 logische Zeichen, 13 L–Struktur, 12 L–Term, 13

Modell, 4, 17, 22 Modus Ponens, 20

Negation, 2, 13 nicht-deterministische polynomiale

Maschine, 10

Menge von Wörtern, 10 Normalform

disjunktive, 6 Herbrand–Normalform, 24 konjunktive, 6 pränexe, 24 Skolem–Normalform, 24

NP, 10 NP-Vollständigkeit, 10 NP = P, 10

P, 10 polynomiale

Maschine, 10

Menge von Wörtern, 10 Potenzmengenalgebra, 7 pränexe Normalform, 24 Primformel, 14 PUSH(r,l), 26

Registermaschine, 26 Relationszeichen, 12 Resolutionsmethode, 9 Resultante, 9

RIGHT, 29

SAT, 10 Satz

von Cantor, 27 von Cook, 10 von Gödel, 21 von Herbrand, 24

Schlußregeln des Hilbertkalküls, 21 Semantik

von aussagenlogischen Formeln, 3 von Formeln, 16 von Termen, 16

Skolem–Normalform, 24 Skolemfunktion, 24 Sprache, 12 Stelligkeit, 12 STOP, 26, 29 Struktur, 12 Substitution

in Formeln, 18 in Termen, 17

Substitutionslemma für Formeln, 18 für Terme, 18 Syntax

von aussagenlogischen Formeln, 2 von prädikatenlogischen Formeln,

13 von Termen, 13

L–Theorie, 22 Tautologie

aussagenlogische, 4 prädikatenlogische, 20

Term, 13 konstanter, 24 Semantik, 16 Tertium non datur, 5 Theorie, 22

konsistente, 22 vollständige, 22 widerspruchsfreie, 22

Turingmaschine, 29

Unifikationssatz, 25

unifizierende Termfolge, 25 universelle, 25 universelle Formel, 24

Variable, 13

aussagenlogische, 2 Verband, 7

distributiver, 7 vollständige Theorie, 22 Vollständigkeitssatz, 21

Wahr, 2 Wahrheit, 17 Wahrheitstafel, 3 Wahrheitswert, 3

einer Formel, 3 widerspruchsfreie Theorie, 22 WRITE(l), 29

Zorns Lemma, 11