© 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.
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.
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.
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.
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, f ∈ FunL(s1,s2,s3)), beschreibt man dies durch die Formel
∀x ∀y(1(x) ∧ 2(y) ⇒ (3(f((x, y))).Quantifizierte Formeln übersetzt man nach den Mustern
∀xsF wird dargestellt durch ∀x( alt="">(x) ⇒ F)Man erkennt hier wieder BQ-Formeln.
∃xsF wird dargestellt durch ∃x( alt="">(x) ∧ F)
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.