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.
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 c1 eine Konstante der Sorte s1 und c2 eine Konstante der Sorte s2 und f ein zweistelliges Funktionssymbol der Argumentsorten (s1, s2) und der Ergebnissorte s3, dann ist f(c1, c2) ein Term der Sorte s3, aber f(c2, c1) 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 s1 eine Untersorte von s2, dann ist jeder Term der Sorte s1 automatisch auch Term der Sorte s2.

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 (s1, s2) und der Ergebnissorte s3 (das heißt, fFunL(s1,s2,s3)), beschreibt man dies durch die Formel

xy(1(x) ∧ 2(y) ⇒ (3(f((x, y))).
Quantifizierte Formeln übersetzt man nach den Mustern
xsF     wird dargestellt durch      ∀x( alt="">(x) ⇒ F)     
xsF      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.

Validierung