2.9 Exkurs: Mehrsortige Prädikatenlogik erster Stufe

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.9 Exkurs: Mehrsortige Prädikatenlogik erster Stufe

Intuitiv steht eine quantifizierte Formel ∀ xF für eine Aussage der Art ,,für alle Objekte gilt die von F repräsentierte Aussage``(eine genaue Definition findet sich in Kapitel 3). Es ist aber im Alltag und in der Informatik- und sogar Mathematikpraxis fast immer so, dass man nur über ganz bestimmte Objekte quantifizieren will. Wenn F eine Aussage über die Professoren des Instituts für Informatik ist, zum Beispiel, dass ihre Promotionsbetreuer auch Professoren sind, ergibt es keinen Sinn, die Aussage für Java-Programme oder für Primzahlen zu betrachten. Für diese Objekte wäre die Aussage weder wahr noch falsch, sondern unsinnig.

Man würde normalerweise formulieren ,,für alle Professoren ...`` oder ,,für alle Java-Programme ...`` oder ,,für alle Primzahlen ...`` und damit die in Frage kommenden Objekte eingrenzen.

Eine mehrsortige Logik bietet zu diesem Zweck spezielle zusätzliche Sprachkonstrukte an, sogenannte Sorten, die den Variablen und Termen syntaktisch zugeordnet werden und damit eine ,,Typisierung`` ganz ähnlich zu höheren Programmiersprachen erlauben.

Definition 2.9.1 (Sprache [mehrsortige PL1S])
Eine Sprache

der mehrsortigen Prädikatenlogik erster Stufe ist gegeben durch ihre Signatur. Zusätzlich gehören zu

die logischen Symbole der mehrsortigen Prädikatenlogik erster Stufe.

Die logischen Symbole der mehrsortigen Prädikatenlogik erster Stufe sind:
1. Die Menge der Hilfszeichen ) und , und (
2. Die Menge der nullstelligen Junktoren:{T, ⊥}.
  Die Menge der einstelligen Junktoren: {¬}.
  Die Menge der zweistelligen Junktoren: {∧, ∨, ⇒, ⇔}.
3. Die Menge der Quantoren {∀, ∃}.
4. Eine nichtleere (oft endliche) Menge S von Sorten.
5. Für jede Sorte s ∈ S eine abzählbar unendliche Menge von Variablen, notiert u^s, v^s, w^s, x^s, y^s, z^s, ... mit oder ohne Indizes.
6. Für einige s ∈ S kann es ein Gleichheitsrelationssymbol geben.
Die Signatur einer Sprache der mehrsortigen Prädikatenlogik erster Stufe besteht aus folgenden Symbolmengen:
1. Für jede natürliche Zahl n ≥ 0 und jedes n-Tupel (s₁,...s_n) von Sorten eine (eventuell leere) Menge Rel_L^{(s₁,...s_n)} von n-stelligen Relationssymbolen der Sorten (s₁,...s_n).
  0-stellige Relationssymbole heißen auch Aussagenvariablen.
2. Für jede natürliche Zahl n ≥ 0 und jedes (n + 1)-Tupel (s₁,...s_n+1) von Sorten eine (eventuell leere) Menge Fun_L^{(s₁,...s_n,
  s_n+1)} von n-stelligen Funktionssymbolen der Argumentsorten (s₁,...s_n) und der Ergebnissorte s_n+1.
  0-stellige Funktionssymbole heißen auch Konstanten.

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 jeder Sorte enthält.

Bemerkung: Die Voraussetzung, dass es mindestens eine Konstante jeder Sorte gibt, hat nur technische Gründe und könnte aufgegeben werden.

Terme und Formeln einer Sprache der mehrsortigen Prädikatenlogik erster Stufe werden jetzt ganz analog wie für die PL1S definiert. Der entscheidende Unterschied ist jeweils, dass die Sorten in naheliegender Weise zusammenpassen müssen. Ist zum Beispiel c₁ eine Konstante der Sorte s₁ und c₂ eine Konstante der Sorte s₂ und f ein zweistelliges Funktionssymbol der Argumentsorten (s₁, s₂) und der Ergebnissorte s₃, dann ist f(c₁, c₂) ein Term der Sorte s₃, aber f(c₂, c₁) ist syntaktisch nicht zulässig. Damit können unsinnige Gebilde wie ,,das kleinste gemeinsame Vielfache der if-Anweisung und des Prodekans`` nach rein syntaktischen Kriterien ausgeschlossen werden.

Die Definitionen von Teilformeln, freien und gebundenen Variablen usw. werden ebenfalls mit geringfügigen Anpassungen übertragen. Die Eindeutigkeitssätze für Terme und Formeln gelten natürlich ebenfalls ganz analog.

Untersorten.

Es gibt Varianten der mehrsortigen Prädikatenlogik erster Stufe, die zusätzlich erlauben, ,,Untersortenbeziehungen`` zwischen Sorten festzulegen. Ist s₁ eine Untersorte von s₂, dann ist jeder Term der Sorte s₁ automatisch auch Term der Sorte s_2.

Auch diese Erweiterung wurde durch praktische Anforderungen der Wissensrepräsentation motiviert, da viele Bereiche in natürlicher Weise hierarchisch strukturiert werden können. In einer solchen Logik könnte man zum Beispiel eine Sorte für Studenten und eine Sorte für Professoren verwenden, die beide in der Untersortenbeziehung zu einer dritten Sorte für Menschen stehen. Andere geläufige Beispiele ergeben sich aus den verschiedenen aufeinander aufbauenden Arten von Zahlen.

Vergleich mit PL1S.

Obwohl die mehrsortige Prädikatenlogik erster Stufe aus praktischer Sicht viele Vorteile gegenüber der klassischen Prädikatenlogik erster Stufe aufweist, unterscheidet sie sich aus theoretischer Sicht nur unwesentlich davon. Man kann nämlich die Mehrsortigkeit in der klassischen PL1S simulieren.

Dazu codiert man jede Sorte s durch ein einstelliges Relationssymbol und drückt die in der mehrsortigen Signatur enthaltene Information durch Formeln der PL1S aus. Ist zum Beispiel f ein zweistelliges Funktionssymbol der Argumentsorten (s₁, s₂) und der Ergebnissorte s₃ (das heißt, f ∈ Fun_L^{(s₁,s₂,s₃)}), beschreibt man dies durch die Formel

∀x ∀y(₁(x) ∧ ₂(y) ⇒ (₃(f((x, y))).

Quantifizierte Formeln übersetzt man nach den Mustern

∀x^sF wird dargestellt durch ∀x( alt="">(x) ⇒ F)
∃x^sF wird dargestellt durch ∃x( alt="">(x) ∧ F)

Man erkennt hier wieder BQ-Formeln.

Damit lässt sich alles, was in einer mehrsortigen Logik ausgedrückt werden kann, auch in der klassischen Prädikatenlogik erster Stufe ausdrücken. Man verliert nichts an Ausdrucksfähigkeit, wenn man die Sorten aufgibt.

Umgekehrt kann die klassische Prädikatenlogik erster Stufe als eine ,,mehrsortige`` Logik mit einer einzigen Sorte aufgefasst werden (man spricht tatsächlich oft von der ,,einsortigen`` Prädikatenlogik erster Stufe). Auch in der Gegenrichtung ändert sich somit nichts an der Ausdrucksfähigkeit.