Entscheidbarkeit in der Prädikatenlogik

Im Allgemeinen ist es ja unentscheidbar, ob eine prädikatenlogische Formel eine Tautologie ist. Wäre dies immer entscheidbar, so könnte auch entschieden werden, ob eine Instanz des Postschen Korrespondezproblems lösbar ist (indem für die Instanz eine prädikatenlogische Formel gebaut wird, die genau dann eine Tautologie ist, wenn die Instanz lösbar ist). Das das Postsche Korrespondezproblem ja unentscheidbar ist, gibt es folglich auch prädikatenlogische Formeln, für die nicht entscheiden werden kann, ob sie Tautologien sind.

Die prädikatenlogischen Formeln lassen sich jedoch etwa mit dem System F aufzählen. Es gibt außerdem Teilmengen prädikatenlogischer Formeln, für die es sogar entscheidbar ist, ob sie Tautologien sind. Hiemrmit und mit der Tablaumethode werde ich mich im Folgenden beschäftigen.

Tableaumethode in der Prädikatenlogik

Mit der Tableaumethode lassen sich auch in der Prädikatenlogik Beweise für verschiedene Eigenschaften von Formeln führen. Dies führe ich nun mit einem Beispiel für einen Erfüllbarkeitsbeweis und mit einem Beispiel für einen Tautologiebeweis vor. Zur besseren Lesbarkeit werde ich die Formeln nummeriert statt in einem Baum aufschreiben.

Erfüllbarkeit

An der Formel ∀ z ∃ x ∃ y p(x, y, z) zeige ich nun, wie man einen Erfüllbarkeitsbeweis mittels Tableau führen kann.

1. ∀ z ∃ x ∃ y p(x, y, z)
2. ∃ x ∃ y p(x, y, a) (a wurde für z in 1. eingesetzt)
3. ∃ x ∃ y p(a, y, a) (a wurde für x in 2. eingesetzt)
4. p(a, a, a) (a wurde für y in 3. eingesetzt)

Die Formel lässt sich mit der Domäne {a} erfüllen mit einer Struktur, die ein Modell für p(a, a, a) ist (also p(a, a, a) erfüllt).

Tautologie

Auch Beweise, dass Formeln wie etwa ∀ x ∀ y ((p(x,y) ∧ q(x)) → ∃ y q(y)) Tautologien sind, lassen sich mit Tableau führen. Hierzu muss die gegebene Formel zunächst negiert werden:

1. ¬∀ x ∀ y ((p(x,y) ∧ q(x)) → ∃ y q(y)) (Negation der gegebenen Formel)
2. ¬∀ y ((p(a,y) ∧ q(a)) → ∃ y q(y)) (a für x in 1. eingesetzt)
3. ¬((p(a,b) ∧ q(a)) → ∃ y q(y)) (b für das y des äußeren Quantors in 2. eingesetzt)
4. p(a,b) ∧ q(a) (aus 3.)
5. ¬∃ y q(y) (aus .3)
6. p(a,b)(aus 4.)
7. q(a) (aus 4.)
8. ¬q(a) (a für das y in 5. eingesetzt)

Da 4. und 5. widersprüchlich sind, ist das Tableau abgeschlossen und die negierte Formel unerfüllbar. Daher ist die ursprüngliche Formel eine Tautologie.

Entscheidbare Theorien

Vor geraumer Zeit hatte ich ja etwas zu Theorien geschrieben. Es gibt hierzu noch eine weitere Erkenntnis, die zu Entscheidbarkeit und Aufzählbarkeit passt: Ist eine Theorie entscheidbar, so ist sie auch aufzählbar axiomatisierbar.

Nun warum ist das so? Eine Theorie ist ja aufzählbar axiomatisierbar, wenn sie sich mit einem aufzählbaren Axiomensystem erzeugen lässt. Da jede Theorie Σ gegen Folgerung abgeschlossen ist, ist die aus der Theorie erzeugte Theorie T_Σ = Σ. Da eine entscheidbare Menge auch semi-entscheidbar, also aufzählbar, ist, ist die entscheidbare Theorie Σ zugleich ein aufzählbares Axiomensystem für sich selbst.

Folgerungen im System F

Mit System F lassen sich in der Prädikatenlogik Beweise für Folgerungen führen. Dies führe ich nun an zwei Beispielen vor.

∀ x p(x,y), y=z ⊢_F ∀ x p(x,z)

1. ∀ x p(x,y) (gegeben)
2. y=z (gegeben)
3. y=z → (∀ x p(x,y) → ∀ x p(x,z) ) (Axiom 6)
4. (∀ x p(x,y) → ∀ x p(x,z) ) (Modus Ponens 2. und 3)
5. (∀ x p(x,z) ) (Modus Ponens 1. und 4.)

∀ x [p(x) → q(x)], ∀ x [p(x)] ⊢_F q(f(a))

1. ∀ x [p(x) → q(x)] (gegeben)
2. ∀ x [p(x)] (gegeben)
3. ∀ x [p(x) → q(x)] → (∀ x [p(x)] → ∀ x [q(x)]) (Axiom 3)
4. ∀ x [p(x)] → ∀ x[q(x)] (Modus Ponens 1. und 3.)
5. ∀ x [q(x)] (Modus Ponens 2. und 4.)
6. ∀ x [q(x)] → q(f(a)) (Axiom 2)
7. q(f(a)) (Modus Ponens 5. und 6.)

Entscheidbarkeit der Theorie der Gleichheit

Zum Abschluss möchte ich nun ein Beispiel für entscheidbare Mengen liefern. Betrachten wie die Theorie der Gleichheit T_ΣE. Diese sei durch das Axiomensystem Σ_E gegeben, das Folgendes für das Gleichheitssymbol fordert: Reflexivität, Symmetrie, Transitivität und Beibehaltung der Gleichheit durch Funktionen (also: sind die Parameter zweier Funktionsaufrufe gleich, dann bilden beide auf gleiche Elemente ab). Die verwendete Signatur enthalte keine Prädikate.

Nun lässt sich ein Algorithmus finden, der für geschlossene, quantorenfreie, prädikatenfreie Formeln entscheidet, ob diese in dieser Theorie sind. Der Algorithmus arbeitet so:

• Bringe die Formel in Disjunktive Normalform
• Für jede Co-Klausel:
  • Bilde einen Graphen mit Knoten für jeden Term, der in der Co-Klausel vorkommt
  • Füge alle Selbstkanten sowie Kanten für alle unnegierten Gleichheiten aus der Co-Klausel ein
  • Bis keine neuen Kanten hinzu kommen: Bilde die transitive Hülle und füge Kanten bei Funktionaufrufen (etwa f(a₁, … , a_n) ↔ f(b₁, … , b_n)) ein, wenn schon zwischen den Parametern Kanten bestehen (also a₁ ↔ b₁ … a_n ↔ b_n)
  • Gibt es keine negierte Gleichheiten in der Formel zwischen solchen Termen, die durch Kanten verbunden sind, gib erfüllbar aus. Andernfalls ist diese Co-Klausel unerfüllbar. Probiere die nächste
• Wurde für keine der Co-Klauseln erfüllbar ausgegeben, gib unerfüllbar aus

---

---