Unterabschnitte

© 1999 François Bry
Dieses Lehrmaterial wird ausschließlich zur privaten Verwendung angeboten. Eine nichtprivate Nutzung (z.B. im Unterricht oder eine Veröffentlichung von Kopien oder Übersetzungen) dieses Lehrmaterials bedarf der Erlaubnis des Autors.


2.3 Prädikatenlogik erster Stufe

Die formale Sprache der Prädikatenlogik erster Stufe, abgekürzt PL1S, benutzt dieselben Junktoren T, ⊥, ¬, ∧, ∨, ⇒ und ⇔ wie die formale Sprache der Aussagenlogik, aber sie bietet sprachliche Mittel zur Darstellung der inneren Struktur von elementaren Aussagen.

Elementare Aussagen werden wie in der Aussagenlogik durch atomare Formeln repräsentiert, die aber aus mehreren Bestandteilen zusammengesetzt sein können. Die Prädikatenlogik erster Stufe benutzt sogenannte ,,Terme`` zur syntaktischen Repräsentation von Objekten und ,,Relationssymbole`` zur syntaktischen Repräsentation von Eigenschaften von und Beziehungen zwischen Objekten. Terme können ihrerseits aus mehreren Bestandteilen zusammengesetzt sein.

Zum Beispiel kann die Aussage ,,Franz ist krank`` in der Prädikatenlogik erster Stufe repräsentiert werden durch eine atomare Formel, deren Relationssymbol für die Eigenschaft ,,ist krank`` steht, und die als Argument einen Term hat, der Franz repräsentiert. Die Gemeinsamkeit dieser Aussage mit ,,Hans ist krank`` äußert sich darin, dass die atomaren Formeln, mit denen die Aussagen repräsentiert werden, mit demselben Relationssymbol gebildet sind, aber verschiedene Terme als Argument haben.

Eine andere Erweiterung bilden die Quantoren ∀ (für alle) und ∃ (es gibt), mit denen Aussagen über unbestimmte Objekte repräsentiert werden können. Derartige Objekte werden durch ,,Variablen`` repräsentiert, die eine spezielle Art von Termen sind.

All diese Erweiterungen erfordern natürlich für eine Sprache der Prädikatenlogik erster Stufe mehr Klassen von Symbolen als für eine Sprache der Aussagenlogik, und zwar sowohl bei den logischen Symbolen als auch bei der Signatur, dem anwendungsspezifischen Teil einer Sprache.

Definition 2.3.1 (Sprache [PL1S])
Eine Sprache der Prädikatenlogik erster Stufe ist gegeben durch ihre Signatur. Zusätzlich gehören zu die logischen Symbole der Prädikatenlogik erster Stufe.
Alle erwähnten Mengen sind abzählbar (üblicherweise sogar aufzählbar) und paarweise disjunkt, und kein Symbol einer dieser Mengen besteht aus einer Sequenz von Symbolen, in der ein Symbol aus einer der anderen Mengen vorkommt.
Es wird vorausgesetzt, dass mindestens eine Konstante enthält.

Bemerkungen:  
  1. Die Variablen gehören nicht zur Signatur, obwohl sie syntaktisch in Formeln an Stellen vorkommen dürfen, an denen auch Signaturelemente erlaubt sind.
  2. Es werden unendlich viele Variablen vorausgesetzt, damit Aussagen über beliebig viele Objekte möglich sind und die Länge von Formeln (und Beweisen) nicht dadurch beschränkt ist, dass irgendwann die verfügbaren Variablen ausgehen. Diese Annahme ist unverzichtbar, aber unproblematisch.
  3. Die Voraussetzung, dass es mindestens eine Konstante gibt, hat technische Gründen, die im Abschnitt über Herbrand-Interpretationen klar werden, und wird sonst nirgends gebraucht.
Definition 2.3.2 (Term [PL1S])
Sei eine Sprache der Prädikatenlogik erster Stufe. Die Menge der -Terme, kurz Terme, ist die kleinste Menge, die die folgenden Bedingungen erfüllt:
  1. Jede Variable von ist ein -Term.
  2. Jede Konstante von ist ein -Term.
  3. Sind t1,...tn -Terme, n ≥ 1, und ist f ein n-stelliges Funktionssymbol von , so ist auch f(t1,...tn) ein -Term.

Satz 2.3.3 (Eindeutigkeitssatz[Term, PL1S])
Sei eine Sprache der Prädikatenlogik erster Stufe. Für jeden -Term t gilt genau eine der folgenden Aussagen:
  1. Es gibt eine eindeutige Variable x von mit t = x.
  2. Es gibt eine eindeutige Konstante c von mit t = c.
  3. Es gibt ein eindeutiges Funktionssymbol f mit Stelligkeit n ≥ 1 und ein eindeutiges n-Tupel (t1,...tn) von -Termen, so dass t = f(t1,...tn).

Beweis: Ähnlich wie der Beweis von Satz 2.1.7.

Die Stelligkeit ist Teil eines Funktionssymbols. Ist es zulässig, in einer Sprache dasselbe Funktionssymbol, zum Beispiel f, mit unterschiedlichen Stelligkeiten n1 und n2 zu verwenden? Die Bemerkung ,,Alle erwähnten Mengen sind ... paarweise disjunkt`` in Definition 2.3.1 verbietet das.

Solange aus dem Kontext eindeutig erkennbar ist, welche Stelligkeit gemeint ist, könnte man ein solches ,,Überladen`` von Funktionssymbolen aber zulassen. Die Programmiersprache Prolog erlaubt es zum Beispiel und bietet die spezielle Notation f/n1 bzw. f/n2 für die Fälle an, in denen man explizit zwischen dem n1-stelligen und dem n2-stelligen Funktionssymbol unterscheiden will. Formal ist es aber nicht ganz einfach, Bedingungen dafür anzugeben, dass die Stelligkeit aus dem Kontext eindeutig erkennbar ist. Deshalb verbieten viele Autoren das ,,Überladen``, so wie es auch durch Definition 2.3.1 ausgeschlossen wird.

Definition 2.3.4 (Formel [PL1S])
Sei eine Sprache der Prädikatenlogik erster Stufe.

Im Fall des Gleichheitsrelationssymbols werden für eine atomare Formel (t1, t1) auch die Notationen (t1 t2) und t1 t2 benutzt. Einige andere zweistellige Relationssymbole und einige zweistellige Funktionssymbole können ebenfalls in Infixform geschrieben werden.

Der Lesbarkeit halber werden oft anstelle der vorgeschriebenen Klammern ( und ) andere Klammern wie etwa [ und ] oder { und } verwendet.

Satz 2.3.5 (Eindeutigkeitssatz[Formel, PL1S])
Sei eine Sprache der Prädikatenlogik erster Stufe. Für jede -Formel F gilt genau eine der folgenden Aussagen:
  1. F = T oder F = ⊥ oder es gibt ein eindeutiges nullstelliges Relationssymbol p mit F = p, oder es gibt ein eindeutiges n-stelliges (n ≥ 1) Relationssymbol p und ein eindeutiges n-Tupel (t1, ...tn) von -Termen mit F = p(t1, ...tn).
  2. Es gibt eine eindeutige -Formel G, so dass F = ¬G.
  3. Es gibt ein eindeutiges Paar (G, H) von -Formeln und einen eindeutigen zweistelligen Junktor θ, so dass F = (G θ H).
  4. Es gibt einen eindeutigen Quantor Q ∈ {∀ ∃}, eine eindeutige Variable x, und eine eindeutige -Formel G, so dass F = QxG.

Beweis: Ähnlich wie der Beweis von Satz 2.1.7.

Bemerkungen:
  1. T und ⊥ sind wie im Fall der Aussagenlogik nicht als atomare Formeln definiert. (Geschmackssache)
  2. Teilformeln können ähnlich wie für die Aussagenlogik definiert werden.
  3. Die Menge aller -Terme ist abzählbar, weil nach Definition alle Symbolmengen von abzählbar sind. Sind diese Mengen darüberhinaus aufzählbar, so ist auch aufzählbar.

    Entsprechendes gilt für die Menge aller -Formeln.

Terme vs. Formeln.

Mit Definition 2.3.2 und Definition 2.3.4 sind zwei verschiedene syntaktische Gebilde eingeführt, zum einen Terme und zum anderen Formeln. Sie müssen trotz ihrer syntaktischen Ähnlichkeiten strikt auseinandergehalten werden. Definiert eine Sprache zum Beispiel a und b als Konstanten, f als zweistelliges Funktionssymbol und p als zweistelliges Relationssymbol, so ist f(a, f(a, b)) ein Term dieser Sprache und p(a, f(a, b)) eine atomare Formel dieser Sprache.

Nach Definition können Terme sowohl in atomaren Formeln als auch in Termen vorkommen (Funktionssymbole dürfen geschachtelt werden). Atomare Formeln können dagegen weder in Termen noch in atomaren Formeln vorkommen (Relationssymbole dürfen nicht geschachtelt werden). Junktoren können Formeln verknüpfen, insbesondere auch atomare Formeln, aber keine Terme. Die atomaren Formeln bilden sozusagen die Schnittstelle zwischen den beiden Arten von syntaktischen Gebilden.

Die strikte Unterscheidung zwischen Termen und Formeln mag rein syntaktisch gesehen willkürlich erscheinen. Sie ist aber wesentlich für die Definitionen zur Semantik (Kapitel 3). Die Grundidee ist, dass Formeln zur Repräsentation von Aussagen dienen, die wahr oder falsch sein können, während Terme zur Repräsentation von Objekten dienen, über die wahre oder falsche Aussagen gemacht werden können, die aber nicht selbst wahr oder falsch sind.

Im obigen Beispiel könnten a und b Zahlen repräsentieren, f eine arithmetische Verknüpfung und p eine arithmetische Vergleichsrelation. Dann repräsentiert der Term f(a, f(a, b)) wieder eine Zahl, die Formel p(a, f(a, b)) aber eine Aussage über zwei Zahlen.

Definition 2.3.6 (Variablen in Term)  
Die Menge var(t) der in einem -Term t vorkommenden Variablen wird wie folgt definiert:
  1. Ist t eine Variable, so var(t) = {t}.
  2. Ist t eine Konstante, so var(t) = Ø.
  3. Hat t die Gestalt f(t1, ...tn), wobei f ein n-stelliges Funktionssymbol ist und t1, ...tn -Terme sind, so
    var(t) = ∪ni = 1 var(ti).
Ist var(t) leer, so heißt t Grundterm oder geschlossener Term.

Definition 2.3.7 (Variablen in Formel)

Bemerkungen:  
  1. Die gleiche Notation var(...) wird für Terme und Formeln verwendet, weil der Kontext Missverständnisse ausschließt.
  2. Für die Wissensmodellierung sind Formeln mit freien Variablen uninteressant. Sie sind aber aus technischen Gründen notwendig, um induktive Definitionen angeben zu können.
  3. var(∀x p(a) ) = var p(a) = var(a) = Ø, und var(∀x p(x) ) = var p(x) = var(x) = {x}.
  4. ,,Grundterm`` und ,,geschlossener Term`` sind Synonyme,
    ,,Grundformel`` und ,,geschlossene Formel`` aber nicht.

    Jede Grundformel ist eine geschlossene Formel, aber nicht umgekehrt.
    p(a) ist eine Grundformel, also auch geschlossen.
    ∀x p(x) ist keine Grundformel, aber geschlossen.
    p(x) ist weder Grundformel noch geschlossen.

Validierung