Satz von Herbrand - LinkFang.de





Satz von Herbrand


Der Satz von Herbrand ist ein Satz der mathematischen Logik, der 1930 vom französischen Logiker Jacques Herbrand publiziert wurde. Er macht eine Aussage darüber, wann eine prädikatenlogische Formel allgemeingültig oder erfüllbar ist und erlaubt eine Reduktion auf Allgemeingültigkeit oder Erfüllbarkeit in der Aussagenlogik.

Der Satz besagt:

Sei [math]\varphi[/math] eine geschlossene prädikatenlogische Formel.
Dann gibt es eine (aus [math]\varphi[/math] berechenbare) quantorenfreie Formel [math]\psi[/math], sodass gilt: [math]\varphi[/math] ist eine Tautologie genau dann, wenn es variablenfreie Substitutionsinstanzen [math]\psi_1, \psi_2, \dots, \psi_n [/math] von [math]\psi[/math] gibt, sodass
[math]\psi_1 \vee \psi_2 \vee \dots \vee \psi_n [/math]
eine aussagenlogische Tautologie ist.

Beweisskizze

Sei eine geschlossene prädikatenlogische Formel [math]\varphi[/math] gegeben. Diese wird zunächst in eine äquivalente pränexe Normalform [math]\varphi'[/math] umgewandelt. In dieser Formel werden nun, ähnlich zur Skolemisierung, alle Allquantoren eliminiert, indem die gebundene Variable durch einen Term ersetzt wird, der aus einem neuen Funktionszeichen und als Argumenten den gebundenen Variablen aller weiter außen stehenden Existenzquantoren besteht. Wenn beispielsweise die Formel die Form

[math]\varphi' = \exists x_1 \forall x_2 \exists x_3 \forall x_4 \theta(x_1,x_2,x_3,x_4)[/math]

([math]\theta[/math] quantorenfrei) hat, wird sie umgewandelt in

[math]\varphi'' = \exists x_1 \exists x_3 \theta(x_1,f(x_1),x_3,g(x_1,x_3))[/math]

Es lässt sich zeigen, dass [math]\varphi[/math] genau dann eine Tautologie ist, wenn [math]\varphi''[/math] eine Tautologie ist. Sei nun [math]\psi = \theta(x_1,f(x_1),x_3,g(x_1,x_3))[/math]. Offensichtlich ist, wenn eine Disjunktion von Substitutionsinstanzen von [math]\psi[/math] eine Tautologie ist, auch [math]\varphi''[/math] eine Tautologie. Die nicht-triviale Richtung besteht nun darin, zu zeigen, dass aus der Allgemeingültigkeit von [math]\varphi''[/math] schon die Existenz einer allgemeingültigen Disjunktion von Instanzen von [math]\psi[/math] folgt. Angenommen, keine Disjunktion von variablenfreien Instanzen von [math]\psi[/math] ist eine Tautologie. Dann ist die Menge

[math]\{ \neg \sigma |\sigma \text{ ist variablenfreie Instanz von } \psi \}[/math]

konsistent und wird erfüllt durch eine Herbrand-Struktur [math]\mathfrak{M}[/math], deren Elemente genau die Terme in der Sprache von [math]\psi[/math] sind. [math]\mathfrak{M}[/math] ist ein Modell von [math]\neg \varphi''[/math]. Damit ist [math]\varphi''[/math] und ebenso [math]\varphi[/math] keine Tautologie.

Es sind auch andere Beweise bekannt. So lässt sich der Satz beweistheoretisch durch die Vollständigkeit des schnittfreien Sequenzenkalküls zeigen, indem aus einer schnittfreien Herleitung die Einführungen der Quantoren beseitigt werden, sodass man die Herleitung einer Sequenz aus quantorenfreien Instanzen erhält.

Korollare

  • Eine geschlossene Formel ist genau dann erfüllbar, wenn sie ein Herbrand-Modell besitzt.[1]
  • Eine Klauselmenge [math]\Gamma[/math] ist genau dann unerfüllbar, wenn es eine unerfüllbare endliche Menge von Grundinstanzen von Klauseln aus [math]\Gamma[/math] gibt.
  • Eine Formel in Skolemform ist genau dann unerfüllbar, wenn es eine unerfüllbare endliche Konjunktion von Substitutionsinstanzen gibt.

Anwendung des Satzes von Herbrand

Der Satz bildet die Grundlage eines Semi-Entscheidungsverfahrens für die Unerfüllbarkeit von prädikatenlogischen Formeln. Gesucht ist eine (einfache) Teilklasse von Strukturen/ Modellen, so dass eine Formel genau dann unerfüllbar (bzw. erfüllbar) wird, wenn sie kein (bzw. ein) Modell in dieser Teilklasse hat.

Will man von einer beliebigen prädikatenlogischen Formel F die Unerfüllbarkeit nachweisen, bringt man diese zuerst mittels gebundener Umbenennung in eine bereinigte Form. Anschließend bildet man den Existenzabschluss, um die freien Variablen zu entfernen und so eine geschlossene Formel zu erhalten. Die Quantoren werden nach links umgestellt, sodass man eine Pränex-Normalform erhält. Anschließend werden die Existenzquantoren entfernt, um eine Skolemform zu erhalten. Die Formel F', die man nach diesen Umformungsschritten erhält, ist nicht mehr äquivalent, aber erfüllbarkeitsäquivalent zur Ausgangsformel F. Diese recht schwache Eigenschaft genügt, um Unerfüllbarkeit von F nachzuweisen.

Nun bildet man zur Formel F' ein Herbrand-Universum, eine Herbrand-Struktur und darauf aufbauend eine Herbrand-Expansion. Jedes Element der Expansion lässt sich mittels einer aussagenlogischen Formel identifizieren. Dazu weist man jedem Prädikat eine aussagenlogische Variable zu. Die Belegungsfunktion bel weist einer aussagenlogischen Variable genau dann 1 zu, wenn auch das Prädikat den Wahrheitswert 1 hat. Die aussagenlogische Formel ist somit genau dann erfüllbar, wenn auch die prädikatenlogische Formel F' erfüllbar ist.

Mit dem Algorithmus von Gilmore kann man anschließend die Unerfüllbarkeit von F' und somit auch F zeigen.

Siehe auch

Literatur

  • Peter G. Hinman: Fundamentals of Mathematical Logic. A K Peters, 2005.
  • Joseph R. Shoenfield: Mathematical Logic. Addison-Wesley, 1967.
  • Jacques Herbrand: Recherches sur la theorie de la demonstration. In: Travaux de la Societe des Sciences et des Lettres de Varsovie, Class III, Sciences Mathematiques et Physiques. Nr. 33, 1930.

Einzelnachweise

  1. Gerhard Goos, Wolf Zimmermann: Vorlesungen über Informatik: Band 1: Grundlagen Und Funktionales Programmieren. ISBN 3540244050. S. 203.

Kategorien: Mathematische Logik | Satz (Mathematik)

Quelle: Wikipedia - http://de.wikipedia.org/wiki/Satz von Herbrand (Vollständige Liste der Autoren des Textes [Versionsgeschichte])    Lizenz: CC-by-sa-3.0

Änderungen: Alle Bilder mit den meisten Bildunterschriften wurden entfernt. Ebenso alle zu nicht-existierenden Artikeln/Kategorien gehenden internen Wikipedia-Links (Bsp. Portal-Links, Redlinks, Bearbeiten-Links). Entfernung von Navigationsframes, Geo & Normdaten, Mediadateien, gesprochene Versionen, z.T. ID&Class-Namen, Style von Div-Containern, Metadaten, Vorlagen, wie lesenwerte Artikel. Ansonsten sind keine Inhaltsänderungen vorgenommen worden. Weiterhin kann es durch die maschinelle Bearbeitung des Inhalts zu Fehlern gerade in der Darstellung kommen. Darum würden wir jeden Besucher unserer Seite darum bitten uns diese Fehler über den Support mittels einer Nachricht mit Link zu melden. Vielen Dank!

Stand der Informationen: August 201& - Wichtiger Hinweis: Da die Inhalte maschinell von Wikipedia übernommen wurden, ist eine manuelle Überprüfung nicht möglich. Somit garantiert LinkFang.de nicht die Richtigkeit und Aktualität der übernommenen Inhalte. Sollten die Informationen mittlerweile fehlerhaft sein, bitten wir Sie darum uns per Support oder E-Mail zu kontaktieren. Wir werden uns dann innerhalb von spätestens 10 Tagen um Ihr Anliegen kümmern. Auch ohne Anliegen erfolgt mindestens alle drei Monate ein Update der gesamten Inhalte.