Sortenlogik entspringt der Intention, das (mengentheoretische) Universum (Grundmenge, Allklasse, bis hin zu einem Grothendieck-Universum) nicht als eine homogene Ansammlung von (mathematischen) Objekten zu betrachten, sondern diese auf verschiedene Klassen oder Typen aufzuteilen, die in diesem Zusammenhang Sorten genannt werden (ähnlich wie die Datentypen in vielen Programmiersprachen und Datenbanksystemen). Jedem Term einer logischen Formel wird eine Sorte zugeordnet. Unifikation von Termen ist nur dann zugelassen, wenn beide Terme von der gleichen Sorte sind; Substitution und Argumentübergabe können ebenfalls nur unter Berücksichtigung dieser Sorten erfolgen. Falsche Sortenzuordnungen werden also bereits als Syntaxfehler ausgewiesen.
Motivation Aus dem Blickwinkel der Prädikatenlogik (ohne Sorten) sind Sorten einstellige Relationen (Sortenprädikate), falsche Sortenzuweisungen erscheinen dann aber nicht mehr als Syntaxfehler, sondern nach Zuweisung einer Semantik als falsch. Die Sortenlogik stellt dagegen für diese Prädikate eine Spezialbehandlung der eben erwähnten Form zur Verfügung.
Im Gegensatz zur Prädikatenlogik zweiter Stufe mit Relationsvariablen bietet die Sortenlogik daher keine Steigerung der Mächtigkeit, etwa in Bezug auf Fragen nach Beweisbarkeit.Näheres siehe A. Oberschelp (1962) S. 297f. Da viele Deduktionschritte aber wegen der Sortenunverträglichkeit nicht in Betracht gezogen werden brauchen, verringert sich der Suchaufwand nach einem Beweis in der Praxis beträchtlich.
Mehrsortige Strukturen bilden ein mengentheoretisches Modell für die Datentypen in der Informationstechnologie, insbesondere bei Datenbanken, weshalb ihnen eine erhebliche praktische Bedeutung zukommt.Beispielsweise können Fehler bei Datentyp-Zuweisungen schnell (zur Compilezeit) als Syntaxfehler erkannt werden. Darüber hinaus ist Mehrsortigkeit eine Möglichkeit, den mit Typentheorien verbundenen Belangen auf mengentheoretischer Basis Rechnung zu tragen.
Einordnung und Abgrenzung Es gibt prinzipiell verschiedene Möglichkeiten, diese Absicht zu realisieren. Den meisten Fällen gemeinsam ist es gibt eine Menge von Sorten (in der Informationstechnologie auch Datentypen genannt) wird gedeutet als ein Alphabet von Sortenbezeichnern, siehe Alphabet (Informatik) und Alphabet (Mathematik). es gibt eine Verallgemeinerung des Begriffs Signatur, um die mit den Sorten verbundene Zusatzinformation zu berücksichtigen. Im gesamten Universum als Zusammenfassung aller Objekte einer Struktur werden dann in die Wertebereiche zu den verschiedenen Sorten abgegrenzt.
Die Algebraisierung der Sortenlogik wird in einem Artikel von Caleiro und Gonçalves beschrieben und kann gut als eine Einführung in die Materie dienen.
Vielsortige Logik In der vielsortigen Logik wird die paarweise Disjunktheit der Wertebereiche (auch Trägermengen genannt) zu den verschiedenen Sorten vorausgesetzt.
Bei vielsortigen Signaturen kommen im Vergleich zu gewöhnlichen einsortigen Signaturen zu den Funktions- und Relations- und ggf. eigens ausgewiesenen Konstantensymbolen noch Bezeichnungen für die Sorten, d. h. die Wertebereiche hinzu. Jedes der Symbole wird jetzt nicht mehr nur durch die Stelligkeit gekennzeichnet, sondern durch die genaue Abfolge der Argumentsorten, und ggf. eine Wert- oder Bildsorte.Unter Sortierung versteht man in diesem Zusammenhang die Zuweisung zu Sorten, siehe Steimann (1991) S. 3. Eine n-stellige Relation ist eine Teilmenge des n-fachen kartesischen Produktes einer Sequenz der Trägermengen. Der Argumentbereich einer n-stelligen Funktion ist ein ebensolches Produkt, dazu kommt noch eine der Trägermengen für das Bild (Funktionswert).
Beispiele Ein Beispiel bieten Taxa (Gruppen) biologischer Organismen, unter anderem und . Während eine Funktion sinnvoll ist, würde das für eine ähnliche Funktion im Allgemeinen nicht gelten. Sortenlogik erlaubt Terme der Art , verwirft aber als syntaktische Fehlkonstruktion.
Vielsortige Strukturen erster Stufe sind beispielsweise folgende heterogene Algebren: Vektorräume über einem Körper (Links-, Rechtsvektorräume bei einem Schiefkörper, Bivektorräume) – mit den Sorten Skalar und Vektor Moduln über einem kommutativen Ring (Links-, Rechtsmoduln bei beliebigem Ring, Bimoduln) – eine Verallgemeinerung des Begriffs (d. h. der Kategorie) Vektorraum Algebren über einem Körper oder kommutativen Ring – als spezielle Vektorräume Lie-Algebren und kommutative Algebren über einem Körper – beides spezielle Algebren über diesem Körper Affine Räumemit dem Spezialfall des euklidischen Raumes sind Beispiele für dreisortige Strukturen mit einem Punktraum und einem Vektorraum mit Trägermenge über einem Körper , die Punkte sind mit den Vektoren über eine Parallelverschiebung genannte Operation verknüpft.
Definition Es seien und disjunkte Mengen von nichtlogischen Zeichen. Sei zudem eine weitere davon disjunkte endliche und nichtleere Menge nichtlogischer Zeichen. Man nennt dann jedes Zeichen in ein Symbol und eine Symbolmenge, jedes Zeichen in eine Sorte, wenn durch eine Abbildung jedem Symbol als Typ eine Sequenz (Tupel) von Sorten zugeordnet wird, und zwar: für alle mit Stelligkeit , und für alle , mit Stelligkeit .
heißt dann eine mehr- oder vielsortige Signatur.Anmerkung: Kruse, Borgelt (2008) S. 3 und S. 9 bezeichnen
die Menge der Sorten mit und die Sorten selbst mit , die Einschränkung von auf die Funktionssymbole mit (eine Menge geordneter Paare), die Einschränkung von auf die Relationssymbole mit , die Variablendeklaration mit (genauer gesagt benutzen die Autoren eine Punktnotation, mit dem Punkt als zusätzlichem technischen Zeichen. Die Variablen werden nur in der Form benutzt mit dem eigentlichen Variablennamen x und einer Sorte s. Als Variablen in dem im Artikel hier gebrauchten Sinn mit Mengenbezeichnung werden dann die Kombinationen, d. h. Zeichenketten mit einer impliziten Variablendeklaration benutzt. Dadurch kann der rohe Name x für mehrere Sorten verwendet werden), die Signatur mit , was im obigen Text entspricht, die Abbildung (kennzeichnend für die -Struktur) mit , und die Variablenbelegung mit .
Anmerkungen Wie im einsortigen Fall wird jedes als Funktionssymbol, jedes als Relationssymbol (oder Prädikatsymbol) bezeichnet. Durch die vielsortige Signatur wird zugeordnet den Relationssymbolen der Stelligkeit ein Typ (Argumenttyp) bestehend aus den Argumentsorten und den Funktionssymbolen der Stelligkeit ein Typ bestehend aus dem Argumenttyp (d. h. den Argumentsorten wie bei den Relationen) und zusätzlich der Bildsorte .
Die Sequenzen (Tupel) der Symboltypen (der Bildwerte von ) lassen sich interpretieren als Wörter (Zeichenketten) über dem Sortenalphabet . Mengentheoretisch handelt es sich um Elemente der Kleeneschen Hülle .. Im Fall der Funktionssymbole, wo mindestens eine Sorte für den Wertebereich benötigt wird, liegen die Werte von in der positiven Hülle . Die Stelligkeit ist die Wortlänge des Typs (minus 1 bei Funktionssymbolen). Die nullstelligen Funktionssymbole werden als Konstantensymbole der Sorte interpretiert. Ggf. vorhandene nullstellige Relationssymbole mit dem leeren kartesischen Mengenprodukt bestehend aus dem leeren Wort (mengentheoretisch identisch mit der Leermenge): werden analog als – aussagenlogische (oder boolesche) Konstantensymbole interpretiert. Ähnlich wie im einsortigen Fall mit der Stelligkeit kann man hier statt der Abbildung , die jedem Symbol seinen Typ aus zuordnet, deren Urbildfasern betrachten. Konkret sind dies die Familien und ; in Funktionschreibweise: ordnet jeder Sequenz von Sorten die Menge der Relationssymbole mit dieser Sequenz als Typ zu (die Länge der Sequenz ist dabei die Stelligkeit); und weist jeder nichtleeren Sequenz von Sorten die Menge der Funktionssymbole zu, wobei die jeweils letzte Sorte der Sequenz die Bildsorte bezeichnet und die anderen vorher den Argumenttyp.
Für die Kennzeichnung der Signatur genügt dann die Angabe des Sortenalphabets zusammen mit diesen beiden Familien .Die beiden Familien definieren sich analog zum einsortigen Fall als die Urbildfasern der Einschränkungen von auf die beiden Symbolmengen und : Stefan Brass 2005 S. 16–19. Der Autor verwendet zur Kennzeichnung der Signatur Faserbündel und teilweise leicht abweichende Bezeichnungen, insbesondere wird das Sortenalphabet mit statt bezeichnet. Statt zur Kennzeichnung des Typs der Funktionssymbole wird auch geschrieben. Bei Verwendung der Schreibweise ist stets zu bedenken, dass hier Bezeichnungen, Symbole, Sorten(bezeichner) gemeint sind, nicht die Objekte, Funktionen, Wertebereiche (Trägermengen) selbst. Die Schreibweise ist insbesondere bei Überladung gültig (die Bildsorte ist durch den Argumenttyp eindeutig bestimmt). Das gleiche Relationssymbol kann für Relationen unterschiedlichen Argumenttyps verwendet werden. Das Gleiche gilt für Funktionssymbole. Man spricht dann von einem überladenen Relationssymbol (Prädikat) bzw. Funktionssymbol. Betrachtet man dei Urbildfasern, dann sind die Menge der Relationssymbole und die Menge der Funktionssymbole zu jeder festen Bildsorte bei Überladung nicht mehr notwendig paarweise disjunkt. Für einen festen Argumenttyp sind jedoch weiterhin die Mengen der Funktionssymbole zu verschiedenen Bildsorten disjunkt: . Folglich bleiben auch in diesem Fall die Menge aller Relationssymbole und die Gesamtheit aller Funktionssymbole für jede Bildsorte paarweise disjunkt.Die Typzuordnung ist bei Überladung eine Multifunktion ( statt ).siehe auch Korrespondenz. Aber auch in diesem Fall hat jedes Symbol bei festgelegtem Argumenttyp höchstens eine Bedeutung: Entweder ist es ein Relationssymbol, oder ein Funktionssymbol zu einer bestimmten Bildsorte .Bezeichnet die Menge aller Funktionssymbole mit einem bestimmten Argumenttyp (also die Vereinigung über alle Bildsorten ), dann sind die Einschränkungen von auf einen bestimmten Argumenttyp als Abbildungen immer eindeutig. Auch im Fall von Überladung ist die Abbildung , die jedem Funktionssymbol die Bildsorte (als letzte Koordinate der Multifunktion , also mit Stelligkeit ) zuordnet, eindeutig.Eine Logik ohne Überladungen heißt strikt.A. Oberschelp (1989/1990) Seite 10. Eine Programmiersprache kann beispielsweise Ganzzahlen (int für integer) und Zeichenketten (string, mit lexikographischer Ordnung) zur Verfügung stellen. Das kann zum Vergleich zweier Ganzzahlen oder zweier Zeichenketten verwendet werden: . Als Beispiele für mehrsortig überladene Funktionssymbole können wieder max und min dienen, die auf verschiedenen Totalordnungen nebeneinander mit gleicher Bezeichnung vorkommen können. Die Funktionssymbole min und max können entweder auf n Argumente vom Datentyp int oder auf n Argumente vom Typ string angewendet werden. Die Bildsorte ist dann durch den Typ der Argumente festgelegt, nämlich gleich der Sorte eines jeden einzelnen Arguments, int oder string. Eine spezielle Bedeutung kommt – wenn vorhanden – der Sorte der logischen Wahrheitswerte zu; übliche Bezeichnungen für diese sind (oder ). Relationen können entsprechend ihrer charakteristischen Funktion als Prädikate aufgefasst werden, siehe Relation, § Relationen und Funktionen. Entsprechend können Relationssymbole als boolesche Funktionssymbole mit Bildsorte gedeutet werden.das ist dann auch die Sorte der logischen Konstanten als nullstelligen Relationen.Relationen lassen sich also als spezielle Funktionen auffassen, umgekehrt sind Funktionen spezielle (linkstotal-rechtseindeutige) Relationen. Dadurch kann eine weitere Vereinfachung erreicht werden. Ein Beispiel ist die Disjunktheitsforderung der Symbolmengen pro Bildsorte bei Überladung (Wegfall der Relationen als Sonderfall). Bei der Definition der Begriffe Term und Ausdruck (auch genannt Formel) und in ihrem Gebrauch kommt der Sorte eine Sonderrolle zu, siehe unten: § Terme in vielsortiger Logik und § Ausdrücke in vielsortiger Logik.
Variablensymbole bei Vielsortigkeit