Sortenlogik

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.

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.^[1] 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.^[2] Darüber hinaus ist Mehrsortigkeit eine Möglichkeit, den mit Typentheorien verbundenen Belangen auf mengentheoretischer Basis Rechnung zu tragen.

Es gibt prinzipiell verschiedene Möglichkeiten, diese Absicht zu realisieren. Den meisten Fällen gemeinsam ist

• es gibt eine Menge T {\displaystyle T} von Sorten (in der Informationstechnologie auch Datentypen genannt) ^[3]
• 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^[4] beschrieben und kann gut als eine Einführung in die Materie dienen.

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.^[5] 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).

• Ein Beispiel bieten Taxa (Gruppen) biologischer Organismen, unter anderem Pflanze {\displaystyle {\textit {Pflanze}}} und Tier {\displaystyle {\textit {Tier}}} . Während eine Funktion Mutter : Tier ⟶ Tier {\displaystyle {\textit {Mutter}}:{\textit {Tier}}\longrightarrow {\textit {Tier}}} sinnvoll ist, würde das für eine ähnliche Funktion Mutter : Pflanze ⟶ Pflanze {\displaystyle {\textit {Mutter}}:{\textit {Pflanze}}\longrightarrow {\textit {Pflanze}}} im Allgemeinen nicht gelten. Sortenlogik erlaubt Terme der Art Mutter ( {\displaystyle {\textit {Mutter}}(} Rex {\displaystyle {\textit {Rex}}} ) {\displaystyle )} , verwirft aber Mutter ( {\displaystyle {\textit {Mutter}}(} Schaeferbuche {\displaystyle {\textit {Schaeferbuche}}} ) {\displaystyle )} 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äume^[6] sind Beispiele für dreisortige Strukturen mit einem Punktraum A {\displaystyle A} und einem Vektorraum mit Trägermenge V {\displaystyle V} über einem Körper K {\displaystyle K} , die Punkte sind mit den Vektoren über eine Parallelverschiebung genannte Operation verknüpft.

Es seien F 0 {\displaystyle {\mathcal {F}}_{0}} und R 0 {\displaystyle {\mathcal {R}}_{0}} disjunkte Mengen von nichtlogischen Zeichen. Sei zudem T {\displaystyle T} eine weitere davon disjunkte endliche und nichtleere Menge nichtlogischer Zeichen. Man nennt dann

• jedes Zeichen in S := F 0 ∪ R 0 {\displaystyle {\mathcal {S}}:={\mathcal {F}}_{0}\cup {\mathcal {R}}_{0}} ein Symbol und S {\displaystyle {\mathcal {S}}} eine Symbolmenge,
• jedes Zeichen in T {\displaystyle T} eine Sorte,

wenn durch eine Abbildung τ {\displaystyle \tau } jedem Symbol als Typ eine Sequenz (Tupel) von Sorten zugeordnet wird, und zwar:

• τ ( f ) ∈ T k + 1 {\displaystyle \tau (f)\in T^{k+1}} für alle f ∈ F 0 {\displaystyle f\in {\mathcal {F}}_{0}} mit Stelligkeit k = σ ( f ) ∈ N 0 {\displaystyle k=\sigma (f)\in \mathbb {N} _{0}} , und
• τ ( R ) ∈ T k {\displaystyle \tau (R)\in T^{k}} für alle R ∈ R 0 {\displaystyle R\in {\mathcal {R}}_{0}} , mit Stelligkeit k = σ ( R ) ∈ N 0 {\displaystyle k=\sigma (R)\in \mathbb {N} _{0}} .

S := ( T , S , τ ) {\displaystyle {\boldsymbol {S}}:=(T,{\mathcal {S}},\tau )} heißt dann eine mehr- oder vielsortige Signatur.^[7]

1. Wie im einsortigen Fall wird jedes f ∈ F 0 {\displaystyle f\in {\mathcal {F}}_{0}} als Funktionssymbol, jedes R ∈ R 0 {\displaystyle R\in {\mathcal {R}}_{0}} als Relationssymbol (oder Prädikatsymbol) bezeichnet.
2. Durch die vielsortige Signatur S {\displaystyle {\boldsymbol {S}}} wird zugeordnet
   • den Relationssymbolen R {\displaystyle R} der Stelligkeit k = σ ( R ) {\displaystyle k=\sigma (R)} ein Typ (Argumenttyp) τ ( R ) = s = ( s 1 , … s k ) ∈ T k {\displaystyle \tau (R)={\boldsymbol {s}}=({\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k})\in T^{k}} bestehend aus den k {\displaystyle k} Argumentsorten s 1 , … s k {\displaystyle {\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k}} und
   • den Funktionssymbolen f {\displaystyle f} der Stelligkeit k = σ ( f ) {\displaystyle k=\sigma (f)} ein Typ τ ( f ) = ( s ; s ′ ) = ( s 1 , … s k ; s ′ ) ∈ T k + 1 {\displaystyle \tau (f)=({\boldsymbol {s}};s')=({\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k};s')\in T^{k+1}} bestehend aus dem Argumenttyp s {\displaystyle {\boldsymbol {s}}} (d. h. den k {\displaystyle k} Argumentsorten wie bei den Relationen) und zusätzlich der Bildsorte s ′ = τ ( f ) n + 1 {\displaystyle s'=\tau (f)_{n+1}} .

Die Sequenzen (Tupel) der Symboltypen (der Bildwerte von τ {\displaystyle \tau } ) lassen sich interpretieren als Wörter (Zeichenketten) über dem Sortenalphabet T {\displaystyle T} . Mengentheoretisch handelt es sich um Elemente der Kleeneschen Hülle T ∗ {\displaystyle T^{*}} .^[8]

2. Die nullstelligen Funktionssymbole c ∈ C := { f ∈ F 0 | τ ( f ) ∈ T } {\displaystyle c\in {\mathcal {C}}:=\{f\in {\mathcal {F}}_{0}|\tau (f)\in T\}} werden als Konstantensymbole der Sorte τ ( f ) {\displaystyle \tau (f)} interpretiert.
3. Ggf. vorhandene nullstellige Relationssymbole b ∈ B := { R ∈ T 0 | τ ( R ) = ϵ } {\displaystyle b\in {\mathcal {B}}:=\{R\in {\mathcal {T}}_{0}|\tau (R)=\epsilon \}} ^[9] werden analog als – aussagenlogische (oder boolesche) Konstantensymbole interpretiert.^[10.1]
4. Ähnlich wie im einsortigen Fall mit der Stelligkeit kann man hier statt der Abbildung τ {\displaystyle \tau } , die jedem Symbol seinen Typ aus T ∗ {\displaystyle T^{*}} zuordnet, deren Urbildfasern betrachten. Konkret sind dies die Familien R = ( R s ) s ∈ T ∗ {\displaystyle {\boldsymbol {\mathcal {R}}}=({\boldsymbol {\mathcal {R}}}_{s})_{s\in {T^{*}}}} und F = ( F s , s ′ ) s ∈ T ∗ , s ′ ∈ T {\displaystyle {\boldsymbol {\mathcal {F}}}=({\boldsymbol {\mathcal {F}}}_{s,s'})_{s\in {T^{*}},s'\in {T}}}  ; in Funktionschreibweise:
   • R : T ∗ → R 0 {\displaystyle {\boldsymbol {\mathcal {R}}}:T^{*}\to {\mathcal {R}}_{0}} 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
   • F : T + → F 0 {\displaystyle {\boldsymbol {\mathcal {F}}}:T^{+}\to {\mathcal {F}}_{0}} 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 S = ( T , R , F ) {\displaystyle {\boldsymbol {\mathcal {S}}}=(T,{\boldsymbol {\mathcal {R}}},{\boldsymbol {\mathcal {F}}})} .^[11][12]

2. Statt τ ( f ) = ( s 1 , … s k ; s ′ ) ∈ T k + 1 {\displaystyle \tau (f)=({\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k};s')\in T^{k+1}} zur Kennzeichnung des Typs der Funktionssymbole wird auch f : s 1 , … s k ⟶ s ′ {\displaystyle f:{\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k}\longrightarrow s'} geschrieben.^[13.1] 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).
3. 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.^[10.2] Betrachtet man dei Urbildfasern, dann sind die Menge der Relationssymbole und die Menge der Funktionssymbole zu jeder festen Bildsorte s ′ {\displaystyle s'} bei Überladung nicht mehr notwendig paarweise disjunkt. Für einen festen Argumenttyp s ∈ T ∗ {\displaystyle {\boldsymbol {s}}\in T^{*}} sind jedoch weiterhin die Mengen der Funktionssymbole zu verschiedenen Bildsorten s 1 ′ , s 2 ′ ∈ T {\displaystyle s'_{1},s'_{2}\in T} disjunkt: F s , s 1 ′ ∩ F s , s 2 ′ = ∅ {\displaystyle {\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},s'_{1}}\cap {\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},s'_{2}}=\emptyset } . Folglich bleiben auch in diesem Fall die Menge aller Relationssymbole R 0 {\displaystyle {\mathcal {R}}_{0}} und die Gesamtheit aller Funktionssymbole F ∗ , s := ⋃ s ∈ T ∗ F s , s ′ = ⋃ { F s , s ′ | s ∈ T ∗ } {\displaystyle {\boldsymbol {\mathcal {F}}}_{*,s}:=\bigcup _{{\boldsymbol {s}}\in {T}^{*}}{\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},s'}=\bigcup \{{\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},s'}|{\boldsymbol {s}}\in {T}^{*}\}} für jede Bildsorte s ′ ∈ T {\displaystyle s'\in T} paarweise disjunkt.
   Die Typzuordnung τ {\displaystyle \tau } ist bei Überladung eine Multifunktion ( τ : S ⊸ T ∗ {\displaystyle \tau :{\mathcal {S}}\multimap T^{*}} statt τ : S → T ∗ {\displaystyle \tau :{\mathcal {S}}\to T^{*}} ).^[14] 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 s ′ {\displaystyle s'} .
   Bezeichnet F s , ∗ {\displaystyle {\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},*}} die Menge aller Funktionssymbole mit einem bestimmten Argumenttyp s {\displaystyle {\boldsymbol {s}}} (also die Vereinigung über alle Bildsorten ⋃ { F s , s ′ | s ′ ∈ T } {\displaystyle \bigcup \{{\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},s'}|s'\in T\}} ), dann sind die Einschränkungen von τ {\displaystyle \tau } auf einen bestimmten Argumenttyp ( τ t := τ | R s ∪ F s , ∗ {\displaystyle \tau _{t}:=\tau |_{{\boldsymbol {\mathcal {R}}}_{\boldsymbol {s}}\cup {\boldsymbol {\mathcal {F}}}_{{\boldsymbol {s}},*}}} ) als Abbildungen immer eindeutig. Auch im Fall von Überladung ist die Abbildung τ ′ {\displaystyle \tau '} , die jedem Funktionssymbol die Bildsorte (als letzte Koordinate der Multifunktion τ {\displaystyle \tau } , also τ ( f ) n + 1 {\displaystyle \tau (f)_{n+1}} mit Stelligkeit n = σ ( f ) {\displaystyle n=\sigma (f)} ) zuordnet, eindeutig.
   Eine Logik ohne Überladungen heißt strikt.^[15]
4. Eine Programmiersprache kann beispielsweise Ganzzahlen (int für integer) und Zeichenketten (string, mit lexikographischer Ordnung) zur Verfügung stellen. Das Kleinerzeichen < kann zum Vergleich zweier Ganzzahlen oder zweier Zeichenketten verwendet werden: <∈ R int ⁡ int , <∈ R string ⁡ string {\displaystyle <\in {\boldsymbol {\mathcal {R}}}_{\operatorname {int} \operatorname {int} },<\in {\boldsymbol {\mathcal {R}}}_{\operatorname {string} \operatorname {string} }} .^[10.2] 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.
5. Eine spezielle Bedeutung kommt – wenn vorhanden – der Sorte der logischen Wahrheitswerte { false , true } {\displaystyle \{\operatorname {false} ,\operatorname {true} \}} zu; übliche Bezeichnungen für diese sind logical {\displaystyle \operatorname {logical} } (oder boolean {\displaystyle \operatorname {boolean} } ). 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 logical {\displaystyle \operatorname {logical} } gedeutet werden.^[16][17] 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 logical {\displaystyle \operatorname {logical} } eine Sonderrolle zu, siehe unten: § Terme in vielsortiger Logik und § Ausdrücke in vielsortiger Logik.

Auch für die Variablen muss eine Sorte spezifiziert werden. In der Literatur finden sich im Wesentlichen zwei Vorgehensweisen:

1. Es wird eine einzige Variablenmenge V {\displaystyle {\mathcal {V}}} vorgesehen. Eine (ggf. nur partielle) Abbildung ν : V ↛ T {\displaystyle \nu :{\mathcal {V}}\not \to T} , die Variablenbezeichnern eine Sorte zuordnet, heißt Variablendeklaration;^[10.3] eine Variable aus dem Definitionsbereich der Variablendeklaration heißt deklariert. Bei der Interpretation kann diese im Skopus (Wirkungsbereich) des jeweiligen Quantors ersetzt werden durch eine lokale Variante (lokal modifizierte Variablendeklaration) ν ′ = ν ⟨ x ↦ s ⟩ {\displaystyle \nu '=\nu _{\langle x\mapsto s\rangle }} mit beliebigen x ∈ V , s ∈ T {\displaystyle x\in {\mathcal {V}},s\in T} und

ν ′ ( y ) = ν ⟨ x ↦ s ⟩ ( y ) := { s wenn   y = x , ν ( y ) sonst (auf dem ursprünglichen Definitionsbereich von   ν ) ; {\displaystyle \nu '(y)=\nu _{\langle x\mapsto s\rangle }(y):={\begin{cases}s&{\text{wenn}}\ y=x,\\\nu (y)&{\text{sonst (auf dem ursprünglichen Definitionsbereich von}}\ \nu {\text{)}};\end{cases}}} ^[10.4] [18]

2. Andere Autoren grenzen dagegen die Symbolmengen für die Variablen verschiedener Sorten streng voneinander ab und benutzen jeweils für jede Sorte eine eigene Menge an Variablensymbolen. Die Variablen werden z. B. durch einen Sortenindex gekennzeichnet. Die Zuweisung ν {\displaystyle \nu } einer Sorte zu einer Variablen ist fest und wird nicht lokal modifiziert.^[19]

Die Zugehörigkeit einer Variable zu einer bestimmten Sorte ( ν ( v ) = s {\displaystyle \nu (v)=s} ) wird in Anklang an das Typenurteil der Typentheorie syntaktisch als v : s {\displaystyle v:s} notiert.^[13.2]

Variablensymbole der Prädikatenlogik zweiter Stufe

• In der Prädikatenlogik zweiter Stufe gibt es zusätzlich Relationsvariablen und ggf. auch Funktionsvariablen. Bereits im einsortigen Fall muss diesen eine Stelligkeit zugeschrieben werden, im Fall der Vielsortigkeit ist diese wie bei den Raltions- und Funktionssymbolen zu einem Typ erweitert. In der Literatur werden (im einsortigen Fall) meist feste Zuordnungen (Stelligkeit) gewählt.^[20][21][22] Entsprechend der Praxis in der Informationstechnologie sind aber auch (Stelligkeits- bzw.) Typdeklarationen mit lokalen Varianten möglich. Die Variablendeklaration ν {\displaystyle \nu } ist dann entsprechend zu erweitern mit Wertebereich T ∗ {\displaystyle T^{*}} statt T {\displaystyle T} .
• Die Relationsvariablen der Prädikatenlogik zweiter Stufe lassen sich als Funktionsvariablen mit Bildsorte logical {\displaystyle \operatorname {logical} } interpretieren.
• Die Variablen der Sorte logical {\displaystyle \operatorname {logical} } – wenn vorhanden – nennt man Aussagenvariablen.^[23.1] Sie entsprechen nullstelligen Relationsvariablen.
• In der monadischen Prädikatenlogik zweiter Stufe sind nur einstellige Relationsvariablen zugelassen. Im vielsortigen Fall sind diese durch die (einzige) Argumentsorte zu kennzeichnen.

Definition

Bei gegebener Signatur S {\displaystyle {\boldsymbol {S}}} und Variablendeklaration ν {\displaystyle \nu } wird die Menge T S , ν ( s ) {\displaystyle {\mathcal {T}}_{{\boldsymbol {S}},\nu }(s)} der Terme der (nichtlogischn) Sorte s {\displaystyle s} dann rekursiv definiert wie folgt:

1. Jedes Variablensymbol v {\displaystyle v} einer Sorte ν ( v ) = s {\displaystyle \nu (v)=s} ist per Deklaration ein Term der Sorte s {\displaystyle s}
2. Ist f {\displaystyle f} ein ( k {\displaystyle k} -stelliges) Funktionssymbol vom Typ ( s 1 , … s k ; s ′ ) {\displaystyle ({\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k};s')} , und ist weiter t 1 {\displaystyle t_{1}} ein Term der Sorte s 1 {\displaystyle {\boldsymbol {s}}_{1}} , t 2 {\displaystyle t_{2}} ein Term der Sorte s 2 {\displaystyle {\boldsymbol {s}}_{2}} , … {\displaystyle \dots } t k {\displaystyle t_{k}} ein Term der Sorte s k {\displaystyle {\boldsymbol {s}}_{k}} , so ist f ( s 1 , … s k ) {\displaystyle f({\boldsymbol {s}}_{1},\dots {\boldsymbol {s}}_{k})} ein Term der Sorte s ′ {\displaystyle s'} ,^[10.5] insbesondere:
   • Jede Konstante c {\displaystyle c} der Sorte τ ( c ) = s {\displaystyle \tau (c)=s} ist per Signatur ein Term der Sorte s {\displaystyle s}

Die Menge aller Terme T S , ν {\displaystyle {\boldsymbol {\mathcal {T}}}_{{\boldsymbol {S}},\nu }} ist gegeben durch die disjunkte Vereinigung der T S , ν ( s ) {\displaystyle T_{{\boldsymbol {S}},\nu }(s)} über alle nichtlogischen Sorten s ∈ T ∖ { logical } {\displaystyle s\in T\setminus \{\operatorname {logical} \}} . Bei leerer Variablendeklaration kann der Index ν {\displaystyle \nu } entfallen: T S ( s ) ,   T S {\displaystyle {\mathcal {T}}_{\boldsymbol {S}}(s),\ {\boldsymbol {\mathcal {T}}}_{\boldsymbol {S}}} .^[24.1]
Durch die Funktionssymbole werden Verknüpfungen verschiedenen Typs zwischen den Elementen der T S , ν {\displaystyle {\boldsymbol {\mathcal {T}}}_{{\boldsymbol {S}},\nu }} bzw. T S ( s ) {\displaystyle {\mathcal {T}}_{\boldsymbol {S}}(s)} der verschiedenen Sorten s {\displaystyle s} induziert, mit denen diese verschiedensortigen Mengen von Zeichenketten selbst zu einer heterogenen Algebra als Termalgebra bzw. Grundtermalgebra werden.

Anmerkungen

• Infix-Notation bei zweistelligen Funktionen: x + 1 {\displaystyle x+1} statt + ( x , 1 ) {\displaystyle +(x,1)} , wie oben. Präfixform: Klammerfreie Polnische Notation, ebenfalls wie oben. Seltener: Postfixnotation.^[25]
• Punktnotation x . farbe {\displaystyle x.\operatorname {farbe} } statt farbe ⁡ ( x ) {\displaystyle \operatorname {farbe} (x)} , x . plus ⁡ ( y ) {\displaystyle x.\operatorname {plus} (y)} statt x plus ⁡ y {\displaystyle x\operatorname {plus} y} (wie in der objektorientierten Programmierung).
• Neuerdings gewinnt die Baumdarstellung von Termen zunehmend an Bedeutung.^[26]

Definition

Sei gegeben eine Signatur S {\displaystyle {\boldsymbol {S}}} und eine Variablendeklaration ν {\displaystyle \nu } . Eine atomare Formel (auch atomarer Ausdruck) ist

• t 1 = t 2 {\displaystyle t_{1}=t_{2}} für alle Terme t 1 , t 2 {\displaystyle t_{1},t_{2}} derselben Sorte s ∈ T {\displaystyle s\in T} .
• Alle Aussagenvariablen, sofern diese Sorte zugelassen ist.^[23.2]
• R t 1 , … t k {\displaystyle Rt_{1},\dots t_{k}} für alle k {\displaystyle k} -stelligen Relationssymbole vom Typ ( s 1 , … s k ) {\displaystyle (s_{1},\dots s_{k})} , wenn t 1 {\displaystyle t_{1}} Term der Sorte s 1 ∈ T {\displaystyle s_{1}\in T} , t 2 {\displaystyle t_{2}} Term der Sorte t 2 ∈ T {\displaystyle t_{2}\in T} , … {\displaystyle \dots } t k {\displaystyle t_{k}} Term der Sorte t k ∈ T {\displaystyle t_{k}\in T} ist.
• Nullstellige Relationssymbole (logische Konstanten), sofern zugelassen.

Ausdrücke (bzw. Formeln) allgemein sind in der mehrsortigen Logik wie folgt rekursiv definiert:

• Jeder atomare Ausdruck ist ein Ausdruck.
• Sind φ {\displaystyle \varphi } und ψ {\displaystyle \psi } Ausdrücke, so sind auch ( φ ∧ ψ ) {\displaystyle (\varphi \land \psi )} , ( φ ∨ ψ ) {\displaystyle (\varphi \lor \psi )} , ( φ → ψ ) {\displaystyle (\varphi \rightarrow \psi )} , ( φ ↔ ψ ) {\displaystyle (\varphi \leftrightarrow \psi )} Ausdrücke.
• ( ∃ x : s   φ ) {\displaystyle (\exists x:s\ \varphi )} und ( ∀ x : s   φ ) {\displaystyle (\forall x:s\ \varphi )} sind Ausdrücke, wenn s ∈ T {\displaystyle s\in T} eine Sorte, x ∈ V {\displaystyle x\in {\mathcal {V}}} ein Variablensymbol, und φ {\displaystyle \varphi } ein Ausdruck ist, in dem die lokale Variable x {\displaystyle x} der Sorte s {\displaystyle s} vorkommt.^[27][10.6]

Anmerkung

Relationen können als Prädikate aufgefasst werden, d. h. als (Boolesche) Funktionen mit gleicher Stelligkeit und Argumenttyp sowie dem Wertebereich { falsch , wahr } {\displaystyle \{\operatorname {falsch} ,\operatorname {wahr} \}} , d. h. der Bildsorte logical {\displaystyle \operatorname {logical} } (siehe Relation, § Relationen und Funktionen). Werden die Junktoren als Symbole für ein- und zweistellige Boolesche Funktionen (in Präfix- bzw. Infix-Notation) aufgefasst, dann sind Ausdrücke – abgesehen von solchen mit Qantoren – quasi ‚Terme der Sorte logical {\displaystyle \operatorname {logical} } ’.

Semantik einer vielsortigen Signatur

S := ( T , S , τ ) {\displaystyle {\boldsymbol {S}}:=(T,{\mathcal {S}},\tau )} sei eine vielsortige Signatur mit der Menge F 0 {\displaystyle {\mathcal {F}}_{0}} der Funktionssymbole (Konstanten als nullstellige Funktionen) und der Menge R 0 {\displaystyle {\mathcal {R}}_{0}} der Relationssymbole (ggf. auch nullstellige, d. h. logische Konstanten).
Sei A := { A s | s ∈ T } ∪ ⋃ t ∈ T ∗ P ( ∏ A ∘ t ) {\displaystyle {\boldsymbol {A}}:=\{A_{s}|s\in T\}\cup \textstyle \bigcup _{t\in T^{*}}{\mathcal {P}}(\textstyle \prod A\circ t)} ^[28]  und α {\displaystyle \alpha } eine Abbildung mit folgenden Maßgaben:

• α ( s ) = A s {\displaystyle \alpha (s)=A_{s}} sei für jede Sorte s ∈ T {\displaystyle s\in T} ein Wertebereich (Grundmenge)
• α ( R ) ⊆ A τ ( R ) 1 × ⋯ A τ ( R ) σ ( R ) {\displaystyle \alpha (R)\subseteq A_{\tau (R)_{1}}\times \cdots A_{\tau (R)_{\sigma (R)}}} eine Relation für jedes R ∈ R 0 {\displaystyle R\in {\mathcal {R}}_{0}} ,^[29] und
• α ( f ) : A τ ( f ) 1 × ⋯ A τ ( f ) σ ( f ) → A τ ( f ) σ ( f ) + 1 {\displaystyle \alpha (f):A_{\tau (f)_{1}}\times \cdots A_{\tau (f)_{\sigma (f)}}\to A_{\tau (f)_{\sigma (f)+1}}} eine Funktion (Verknüpfung) für jedes f ∈ F 0 {\displaystyle f\in {\mathcal {F}}_{0}} .^[30]

Dann nennt man α {\displaystyle \alpha } eine Interpretationsfunktion und A := ( ( A s ) s ∈ T , α | F 0 ∪ α | R 0 ) = ( α | T , α | F 0 ∪ α | R 0 ) {\displaystyle {\mathcal {A}}:=((A_{s})_{s\in T},\alpha |_{{\mathcal {F}}_{0}}\cup \alpha |_{{\mathcal {R}}_{0}})=(\alpha |_{T},\alpha |_{{\mathcal {F}}_{0}}\cup \alpha |_{{\mathcal {R}}_{0}})} eine vielsortige Struktur der Signatur S {\displaystyle {\boldsymbol {S}}} oder S {\displaystyle {\boldsymbol {S}}} -Struktur.^[31]

Überladung

Im Fall von Überladung wird Eindeutigkeit hergestellt, indem zum Relations- bzw. Funktionssymbol noch der Argumenttyp angegeben wird:

α s ( R ) ⊆ A s 1 × ⋯ A s n {\displaystyle \alpha _{\boldsymbol {s}}(R)\subseteq A_{{\boldsymbol {s}}_{1}}\times \cdots A_{{\boldsymbol {s}}_{n}}} ,

α s ( f ) : A s 1 × ⋯ A s n → A s ′ {\displaystyle \alpha _{\boldsymbol {s}}(f):A_{{\boldsymbol {s}}_{1}}\times \cdots A_{{\boldsymbol {s}}_{n}}\to A_{s'}} .

Dabei ist die Stelligkeit n {\displaystyle n} hier gegeben ist durch die (Wort-)Länge n = | s | {\displaystyle n=|{\boldsymbol {s}}|} des Argumenttyps s {\displaystyle {\boldsymbol {s}}} , und s ′ {\displaystyle s'} ist die durch den Argumenttyp eindeutig bestimmte Bildsorte s ′ = τ ( f ) n + 1 . {\displaystyle s'=\tau (f)_{n+1}.}
Es handelt sich um partielle Abbildungen, nur für Typen s {\displaystyle {\boldsymbol {s}}} mit R t ≠ ∅ {\displaystyle {\boldsymbol {\mathcal {R}}}_{t}\neq \emptyset } bzw. F t ≠ ∅ {\displaystyle {\boldsymbol {\mathcal {F}}}_{t}\neq \emptyset } kann es überhaupt Zuweisungen der Symbole zu Relationen bzw. Funktionen gegeben.

Interpretation

Eine (ggf. nur partielle) Abbildung β {\displaystyle \beta } auf V {\displaystyle {\mathcal {V}}} , die deklarierte Variablen x {\displaystyle x} aus V {\displaystyle {\mathcal {V}}} auf Elemente der zugehörigen Sorte ν x = ν ( x ) {\displaystyle \nu _{x}=\nu (x)} (d. h. aus dem Wertebereich A ν x {\displaystyle A_{\nu _{x}}} ) abbildet, heißt eine Belegung der vielsortigen S {\displaystyle {\boldsymbol {S}}} -Struktur A {\displaystyle {\mathcal {A}}} .^[32][24.2]

Für eine Interpretation I {\displaystyle {\boldsymbol {I}}} der Signatur S {\displaystyle {\boldsymbol {S}}} werden jetzt die Komponenten T , A , ν , β {\displaystyle T,{\mathcal {A}},\nu ,\beta } benötigt.

Bei vorhandener Interpretation und Variablenbelgung (was ggf. eine Variablendeklaration voraussetzt) kann dann Sorte und Wert der Terme bestimmt werden (siehe Term, § Termauswertung), sowie die Gültigkeit logischer Ausdrücke beurteilt werden (siehe Term, § Gültigkeit von Ausdrücken).

Termauswertung und Gültigkeit von Ausdrücken (Formeln)

• Zur Auswertung nichtlogischer Terme siehe Hauptartikel Term, § Termauswertung,
• zur Gültigkeit von logischen Ausdrücken (Formeln) siehe Hauptartikel Term, § Gültigkeit von Ausdrücken.

In der ordnungssortierten Logik sind die den Sorten s ∈ T {\displaystyle s\in T} zugeordneten Wertebereiche A s {\displaystyle A_{s}} im Gegensatz zur vielsortigen Logik nicht notwendig disjunkt. Stattdessen ist die Menge der Sorten T {\displaystyle T} mit einer partiellen Ordnung ⪯ {\displaystyle \preceq } versehen,^[33] so dass für alle Sorten s 1 , s 2 {\displaystyle s_{1},s_{2}} gilt: Wenn s 1 ⪯ s 2 {\displaystyle s_{1}\preceq s_{2}} , dann A s 1 ⊆ A s 2 {\displaystyle A_{s_{1}}\subseteq A_{s_{2}}} . Dadurch wird die Sorte s 1 {\displaystyle s_{1}} zu einer Untersorte der Sorte s 2 {\displaystyle s_{2}} (Obersorte) erklärt.^[13.1] [34] Diese Logik ist Grundlage der Vererbung von Klassen (Klassenhierarchie) in der objektorientierten Programmierung.

Ordnungssortierte Logik kann wie vielsortige Logik in gewöhnliche einsortige Logik umgesetzt werden. Die Sortenzugehörigkeit t : s {\displaystyle t:s} wird wieder übersetzt in ein einstelliges Prädikat P s ( t ) {\displaystyle P_{s}(t)} , zusätzlich kommt für jede Untersortenbeziehung s ⪯ s ′ {\displaystyle s\preceq s'} ein Axiom ∀ x : ( P s ( t ) → P s ′ ( t ) ) {\displaystyle \forall x:(P_{s}(t)\to P_{s'}(t))} hinzu.

Der umgekehrte Ansatz war erfolgreich in einem automatisierten Theorembeweis: 1985 konnte Christoph Walther ein Benchmark-Problem lösen, indem er es in ordnungssortierter Logik formulierte und dadurch den Aufwand um Größenordnungen reduzierte, da viele einstelligen Prädikate zu Sortierungen wurden.^[35]

• Im obigen Beispiel wäre etwa

Hund   ⪯   Fleischfresser {\displaystyle {\textit {Hund}}\ \preceq \ {\textit {Fleischfresser}}} ,

Hund   ⪯   Wirbeltier {\displaystyle {\textit {Hund}}\ \preceq \ {\textit {Wirbeltier}}} ,

Raubtier   ⪯   Tier {\displaystyle {\textit {Raubtier}}\ \preceq \ {\textit {Tier}}} ,

Wirbeltier   ⪯   Tier {\displaystyle {\textit {Wirbeltier}}\ \preceq \ {\textit {Tier}}} ,

Tier   ⪯   Organismus {\displaystyle {\textit {Tier}}\ \preceq \ {\textit {Organismus}}} ,

Buche   ⪯   Pflanze {\displaystyle {\textit {Buche}}\ \preceq \ {\textit {Pflanze}}} ,

Pflanze   ⪯   Organismus {\displaystyle {\textit {Pflanze}}\ \preceq \ {\textit {Organismus}}} ,

und so weiter.

• Modellierung der Verhältnisse bei den Zahlenbereichen:

Z {\displaystyle \mathbb {Z} } (ganze Zahlen) ⊆ Q {\displaystyle \subseteq \mathbb {Q} } (rationale Zahlen) ⊆ R {\displaystyle \subseteq \mathbb {R} } (reelle Zahlen) ⊆ C {\displaystyle \subseteq \mathbb {C} } (komplexe Zahlen) ⊆ H {\displaystyle \subseteq \mathbb {H} } (Quaternionen) ⊆ O {\displaystyle \subseteq \mathbb {O} } (Oktonionen) ⊆ S {\displaystyle \subseteq \mathbb {S} } (Sedenionen),

Q ⊆ A {\displaystyle \mathbb {Q} \subseteq \mathbb {A} } (algebraische Zahlen) ⊆ C {\displaystyle \subseteq \mathbb {C} } .

• In manchen Programmiersprachen (wie Pascal und Modula-2) dienen ganzzahlige Intervalle als Datentypen: Seien m , n ∈ Z {\displaystyle m,n\in \mathbb {Z} } mit m ≤ n {\displaystyle m\leq n} , dann gilt für den Intervall-Datentyp m . . n ⪯ int {\displaystyle m.\!.n\preceq \operatorname {int} } ^[36] Die (ungeprüfte) Zuweisung von beliebig ganzzahligen Werten an diesen Datentyp kann als syntaktisch falsch eingestuft werden.

• Eine besondere Situation ergibt sich, wenn die Sorte logical {\displaystyle \operatorname {logical} } Überschneidungen mit anderen Sorten hat. Die Wahrheitswerte false {\displaystyle \operatorname {false} } und true {\displaystyle \operatorname {true} } können als 0 ins 1 gedeutet werden. Dann stehen diese für Relationen wie ≤ {\displaystyle \leq } und Funktionen (Verknüpfungen) wie + , − , ⋅ {\displaystyle +,-,\cdot } und / {\displaystyle /} zur Verfügung. Ein Beispiel dafür in der Informationstechnologie ist C-Language.^[37] In einer Erweiterung könnten die logischen Werte einer dreiwertigen Logik oder einfachen Fuzzy-Logik mit Zahlen aus dem reellen Intervall [ 0 , 1 ] {\displaystyle [0,1]} gleichgesetzt werden, so dass in allen Fällen gilt: logical ⪯ real {\displaystyle \operatorname {logical} \preceq \operatorname {real} }

Durch ( T , ⪯ ) {\displaystyle (T,\preceq )} wird dann eine Sortenstruktur erzeugt mit einer nochmals erweiterten ordnungsorientierten Signatur, etwa ( T , ⪯ , τ | F 0 , τ | R 0 ) {\displaystyle (T,\preceq ,\tau |_{{\mathcal {F}}_{0}},\tau |_{{\mathcal {R}}_{0}})} ^[38][39] Beispiele für ordnungssortierte Strukturen in der Mathematik sind

• Q {\displaystyle \mathbb {Q} } , A {\displaystyle \mathbb {A} } , R {\displaystyle \mathbb {R} } und C {\displaystyle \mathbb {C} } als kommutative und assoziative Algebren über dem Ring der ganzen Zahlen Z {\displaystyle \mathbb {Z} } (d. h. als spezielle Z {\displaystyle \mathbb {Z} } -Moduln), da Z {\displaystyle \mathbb {Z} } Teilmenge dieser Zahlenbereiche ist,
• R {\displaystyle \mathbb {R} } als unendlich-dimensionale assoziative und kommutative Algebra über dem Körper der rationalen Zahlen Q {\displaystyle \mathbb {Q} } (d. h. als spezieller R {\displaystyle \mathbb {R} } -Vektorraum mit Hamel-Basis), da Q ⊆ R {\displaystyle \mathbb {Q} \subseteq \mathbb {R} } ,^[40]
• C {\displaystyle \mathbb {C} } als zweidimensionale assoziative und kommutative Algebra über dem Körper R {\displaystyle \mathbb {R} } (d. h. als spezieller R {\displaystyle \mathbb {R} } -Vektorraum), da R ⊆ C {\displaystyle \mathbb {R} \subseteq \mathbb {C} }
• Ein weiteres Beispiel bilden die verschiedenen Bereiche hyperkomplexer Zahlen, wie die Quaternionen H {\displaystyle \mathbb {H} } (respektive Oktonionen O {\displaystyle \mathbb {O} } bzw. Sedenionen S {\displaystyle \mathbb {S} } ), etwa als vierdimensionale assoziative nicht-kommutative Algebra (respektive acht- bzw. 16-dimensionale nicht-assoziative nicht-kommutative Algebra) über dem Körper R {\displaystyle \mathbb {R} } , der wie schon bei C {\displaystyle \mathbb {C} } eine Teilmenge darstellt.

Die Halbordnung ⪯ {\displaystyle \preceq } wird auf kanonische Weise fortgesetzt auf T ∗ {\displaystyle T^{*}} wie folgt:

s 1 ⪯ s 2 {\displaystyle {\boldsymbol {s}}_{1}{\boldsymbol {\preceq }}{\boldsymbol {s}}_{2}} genau dann, wenn

• s 1 {\displaystyle {\boldsymbol {s}}_{1}} und s 2 {\displaystyle {\boldsymbol {s}}_{2}} haben die gleiche Stelligkeit (d. h. Tupel- oder Wortlänge), hier bezeichnet mit k {\displaystyle k}
• für alle i = 1 … k {\displaystyle i=1\dots {k}} gilt s 1 i ⪯ s 2 i {\displaystyle {\boldsymbol {s}}_{1_{i}}\preceq {\boldsymbol {s}}_{2_{i}}}

Eine ordnungsorientierte Signatur heißt regulär genau dann, wenn für jedes Funktionssymbol f ∈ F 0 {\displaystyle f\in {\mathcal {F}}_{0}} und jedes w ∈ T ∗ {\displaystyle {\boldsymbol {w}}\in T^{*}} die Menge

{ s ′ ∈ T | ∃ s ∈ T ∗   m i t   w ⪯ s : τ ( f ) = ( s , s ′ ) } = { s ∈ T | ∃ s ∈ T ∗   m i t   w ⪯ s :   f : s ⟶ s ′ } {\displaystyle \{s'\in T|\exists {\boldsymbol {s}}\in T^{*}\ \textstyle {mit}\ {\boldsymbol {w}}{\boldsymbol {\preceq }}{\boldsymbol {s}}:\tau (f)=({\boldsymbol {s}},s')\}=\{s\in T|\exists {\boldsymbol {s}}\in T^{*}\ \textstyle {mit}\ {\boldsymbol {w}}{\boldsymbol {\preceq }}{\boldsymbol {s}}:\ \;f:{\boldsymbol {s}}\longrightarrow s'\}}

leer ist oder ein eindeutig bestimmtes kleinstes Element hat.^[13.3]

Eine reguläre Signatur heiß zulässig, wenn die folgenden Bedingungen erfüllt sind:^[13.4]

• Wenn für f : s ⟶ s ′ {\displaystyle f:{\boldsymbol {s}}\longrightarrow s'} und f : w ⟶ w ′ {\displaystyle f:{\boldsymbol {w}}\longrightarrow w'} mit s , w ∈ T ∗ , s ′ , w ′ ∈ T {\displaystyle {\boldsymbol {s}},{\boldsymbol {w}}\in T^{*},s',w'\in T} gilt w ⪯ s {\displaystyle {\boldsymbol {w}}{\boldsymbol {\preceq }}{\boldsymbol {s}}} , dann gilt auch w ⪯ s {\displaystyle w\preceq s} ^[13.3]
• Es kann keine unendliche Ketten … s 3 ⪯ s 2 ⪯ s 1 {\displaystyle \dots s_{3}\preceq s_{2}\preceq s_{1}} geben. Falls die Sorten- und Symbolmengen endlich sind (endliche Signatur), ist das stets gewährleistet.
• Abwärtsvollständigkeit: Wenn zwei Sorten s 1 , s 2 ∈ T {\displaystyle s_{1},s_{2}\in T} gemeinsame Untersorten haben, dann gibt es eine größte gemeinsame Untersorte (ggU, engl.: greatest common subset), in Zeichen gcs ⁡ ( s 1 , s 2 ) {\displaystyle \operatorname {gcs} (s_{1},s_{2})} .^[41] Notfalls kann aber eine geeignete neue Sorte r {\displaystyle r} zum Sortenalphabet T {\displaystyle T} hinzugenommen werden, damit dann r = gcs ⁡ ( s 1 , s 2 ) {\displaystyle r=\operatorname {gcs} (s_{1},s_{2})} erfüllt wird. Auf Objetebene besagt die Bedingung nichts anderes, als dass die Schnittmenge zweier Wertebereiche A s 1 {\displaystyle A_{s_{1}}} und A s 2 {\displaystyle A_{s_{2}}} (als größte gemeinsame Teilmenge) entweder leer ist, oder aber Wertebereich zu einer geeigneten Sorte r ∈ T {\displaystyle r\in T} sein muss.
  Um ordnungssortierte Logik in einen satzbasierten automatischen Theorembeweiser zu integrieren, ist ein entsprechender ordnungssortierter Unifikation-Algorithmus notwendig. Dies erfordert, dass für zwei erklärte Sorten s 1 , s 2 ∈ T {\displaystyle s_{1},s_{2}\in T} mit Ausnahme der Disjunktheit deren ggU gcs ⁡ ( s 1 , s 2 ) {\displaystyle \operatorname {gcs} (s_{1},s_{2})} ebenfalls erklärtes Mitglied der Sortenmenge T {\displaystyle T} ist
• Für alle s ∈ T , w ∈ T ∗ , f ∈ F 0 {\displaystyle s\in T,{\boldsymbol {w}}\in T^{*},f\in {\mathcal {F}}_{0}} mit f : w ′ ⟶ s ′ {\displaystyle f:{\boldsymbol {w}}'\longrightarrow s'} ^[42] ist auch die Menge

  { v ∈ T ∗ | ∃ v ′ ∈ T ∗ , r ∈ T : f : v ′ ⟶ r , r ⪯ s , v , ⪯ w , v ⪯ v ′ } {\displaystyle \{{\boldsymbol {v}}\in T^{*}|\exists {\boldsymbol {v}}'\in T^{*},r\in T:f:{\boldsymbol {v}}'\longrightarrow r,r\preceq s,{\boldsymbol {v}},{\boldsymbol {\preceq }}w,{\boldsymbol {v}}{\boldsymbol {\preceq }}{\boldsymbol {v}}'\}}

entweder leer oder hat ein größtes Element. Die Kombination dieser Forderung mit der Abwärtsvollständigkeit heißt Abwärtseindeutigkeit.

Aus praktischen Gründen ist Überladung der Normalfall.^[13.2] Alle Funktions- und Relationssymbole + , − , ⋅ , / , ≤ , … {\displaystyle +,-,\cdot ,/,\leq ,\dots } müssten andernfalls für jeden Zahlenbereich N , Z , Q , R A , C {\displaystyle \mathbb {N} ,\mathbb {Z} ,\mathbb {Q} ,\mathbb {R} \mathbb {A} ,\mathbb {C} } unterschiedlich sein und diesen z. B. als Index mitführen. Die Zahlenbereiche C , A , R , Q {\displaystyle \mathbb {C} ,\mathbb {A} ,\mathbb {R} ,\mathbb {Q} } mit den komplex-algebraischen Zahlen A {\displaystyle \mathbb {A} } und den Ketten Q ⊆ R ⊆ C {\displaystyle \mathbb {Q} \subseteq \mathbb {R} \subseteq \mathbb {C} } und Q ⊆ A ⊆ C {\displaystyle \mathbb {Q} \subseteq \mathbb {A} \subseteq \mathbb {C} } bilden auch ein Beispiel für (fehlende) Abwärtsvollständigkeit: Als Schnittmenge zweier Sorten-Wertebereiche sind die reell-algrbraischen Zahlen A ∩ R {\displaystyle \mathbb {A} \cap \mathbb {R} } eine Menge mit fehlenden Sortenzeichen, was der Vollständigkeit halber nachzutragen wäre.

Wie bei der vielsortigen Logik gibt es die Möglichkeit, die Variablen in Mengen mit fester Sorte zuzuordnen, oder die Sortenzughöigkeit nachträglich und lokal modifizierbar per Deklaration ν : V → T {\displaystyle \nu :{\mathcal {V}}\to T} festzulegen.

Die Termauswertung auf Basis der Variablendeklaration und des Typs der Funktionen (einschließlich der Konstanten) ordnet den Termen t {\displaystyle t} abhängig von der Signatur und der Variablendeklaration rekursiv soweit möglich einen Sortemenge S ( t ) {\displaystyle {\mathcal {S}}(t)} (Überladungen!) und einen Wert [ [ t ] ] {\displaystyle [\![t]\!]} zu.

• für Variablen v ∈ V {\displaystyle v\in {\mathcal {V}}} : S ( v ) = { r ∈ T | ν ( v ) ⪯ r } {\displaystyle {\mathcal {S}}(v)=\{r\in T|\nu (v)\preceq r\}} (Oberhalbmeng von ν ( v ) {\displaystyle \nu (v)} )
• für Konstanten c {\displaystyle c} : S ( c ) = { r ∈ T | τ ( c ) ⪯ r } {\displaystyle {\mathcal {S}}(c)=\{r\in T|\tau (c)\preceq r\}}
• für Funktionen f {\displaystyle f} : S ( f ) = { ( r , r ′ ) ∈ T + | ∃ s ∈ T ∗ , s ′ ∈ T : f : s ⟶ s ′ ∧ s ⪯ r ∧ s ′ ⪯ r ′ } {\displaystyle {\mathcal {S}}(f)=\{({\boldsymbol {r}},r')\in T^{+}|\exists {\boldsymbol {s}}\in T^{*},s'\in T:f:{\boldsymbol {s}}\longrightarrow s'\land {\boldsymbol {s}}{\boldsymbol {\preceq }}{\boldsymbol {r}}\land s'\preceq r'\}} ^[43]

Beispiel

Wenn x 1 {\displaystyle x_{1}} und x 2 {\displaystyle x_{2}} Variablen des Typs s 1 {\displaystyle s_{1}} bzw. s 2 {\displaystyle s_{2}} sind, dann hat die Gleichung x 1 = x 2 {\displaystyle x_{1}=x_{2}} die Lösung { x 1 = x , x 2 = x } {\displaystyle \{x_{1}=x,\;x_{2}=x\}} , wobei x : gcs ⁡ ( s 1 , s 2 ) {\displaystyle x:\operatorname {gcs} (s_{1},s_{2})} gilt.

Gert Smolka verallgemeinerte die ordnungssortierte Logik, um parametrischen Polymorphismus (engl. parametric polymorphism) zu erlauben.^[44] In seiner Arbeit werden Untersortenbeziehungen zu komplexen Typ-Ausdrücken weiterentwickelt. In einem Programmierbeispiel kann eine parametrisierte Sorte list ( X ) {\displaystyle {\textit {list}}(X)} deklariert werden (wobei X {\displaystyle X} > ein Typparameter ist wie in einem C++ Template). Aus der Untersortenbeziehung int ⊆ float {\displaystyle {\textit {int}}\subseteq {\textit {float}}} kann die Relation list ( int ) ⊆ list ( float ) {\displaystyle {\textit {list}}({\textit {int}})\subseteq {\textit {list}}({\textit {float}})} automatisch abgeleitet werden, was bedeutet, dass jede Liste von Ganzzahlen auch eine Liste von Gleitkommazahlen ( float {\displaystyle {\textit {float}}} ) ist.

Schmidt-Schauß verallgemeinerte die ordnungssortierte Logik um Termdeklarationen zu erlauben.^[45] Beispielsweise erlauben die Untersortenbeziehungen even ⪯ int {\displaystyle {\textit {even}}\preceq {\textit {int}}} und odd ⪯ int {\displaystyle {\textit {odd}}\preceq {\textit {int}}} und eine Termdeklaration wie ∀ i : int . ( i + i ) : even {\displaystyle \forall i:{\textit {int}}.\;(i+i):{\textit {even}}} eine Eigenschaft der Ganzzahladdition zu erklären, wie sie mit gewöhnlicher Überladung nicht ausgedrückt werden kann.

Schließlich lässt sich die ordnungssortierte Logik noch in Richtung Feature-Logik erweitern. Die Argumente von Funktionen und Relationen werden mit Namen versehen (statt oder zusätzlich zur Positionsnummer).^[46] Dies erlaubt es, neben oder anstatt der üblichen Stellungs- oder Positionsparameter Schlüsselwortparameter zu verwenden. Das Verfahren ist einerseits in der Informationstechnologie weit verbreitet, eröffnet andererseits aber theoretische Zusammenhänge mit Dependenzgrammatiken.^[13]

• Signatur (Modelltheorie)
• Termauswertung und Gültigkeit von Ausdrücken (Formeln)

• Wolfgang Bibel, Steffen Hölldobler, Torsten Schaub: Wissensrepräsentation und Inferenz. Eine grundlegende Einführung. Springer-Verlag, 2013, ISBN 3-322-86814-1, S. 99–100 (books.google.de). 
• François Bry: Exkurs: Mehrsortige Prädikatenlogik erster Stufe. Band 2.9. LMU, Institut für Informatik, Lehr- und Forschungseinheit für Programmier- und Modellierungssprachen (pms), München 1999 (en.pms.ifi.lmu.de). 
• François Bry: Exkurs:Prädikatenlogik zweiter Stufe. Band 2.10. LMU, Institut für Informatik, Lehr- und Forschungseinheit für Programmier- und Modellierungssprachen (pms), München 1999 (en.pms.ifi.lmu.de). 
• P.C. Gilmore: An addition to “Logic of many-sorted theories”. In: Compositio Mathematica. 13. Jahrgang, 1958, S. 277–281 (numdam.org [PDF]). 
• Klaus Gloede: Skriptum zur Vorlesung Mengenlehre. SS 2004. Universitär Heidelberg, Mathematisches Institut, S. 181.  PDF, Bei DOCZZ, Bei Yumpu
• R. Hartwig: Syntax Semantik Spezifikation. Grundlagen de Informatik. WS 2009/2010. Universität Leipzig, Institut für Informatik, Leipzig, S. 219 (informatik.uni-leipzig.de [PDF]). 
• M. Huber, I. Varšek: Extended Prolog with Order-Sorted Resolution.4th IEEE Symposium of Logic Programming. San Francisco 1987, S. 34–45. 
• H. Kleine Büning,: Sorten und Terme. Wintersemester 2015. Mod. 05 Teil 1. Universität Paderborn, 2015, S. 15. 
• Reinhold Letz: Prädikatenlogik. WS 2004/2005. Technische Universität München, Fakultät für Informatik, Lehrstuhl Informatik IV, München, S. 47 (tcs.ifi.lmu.de [PDF]). 
• Carsten Lutz: Logik Teil 4: Prädikatenlogik zweiter Stufe. Universität Bremen, AG Theorie der künstlichen Intelligenz, 2010, S. 65 (informatik.uni-bremen.de [PDF] Vorlesung im Wintersemester 2010). 
• Arnold Oberschelp: Untersuchungen zur mehrsortigen Quantorenlogik, Nummer 4. In: Mathematische Annalen. 145. Jahrgang, 1962, ISSN 0025-5831; 1432-1807/e, S. 297–333, doi:10.1007/bf01396685 (englisch, eudml.org). 
• Arnold Oberschelp: Order Sorted Predicate Logic. Lecture Notes in Computer Science (LNCS). Hrsg.: Bläsius, Karl Hans; Hedtstück, Ulrich; Rollinger, Claus-Rainer. Band 418: Sorts and Types in Artificial Intelligence, Workshop, Eringerfeld, FRG, April 24–26, 1989 Proceedings. Springer-Verlag, Berlin / Heidelberg 1990, ISBN 978-3-540-52337-6, S. 307, doi:10.1007/3-540-52337-6. 
• F. Jeffry Pelletier: Sortal Quantification and Restricted Quantification. In: Philosophical Studies. 23. Jahrgang, 1972, S. 400–404, doi:10.1007/bf00355532 (englisch, sfu.ca [PDF]). 
• Esther Ramharter, Günther Eder: Prädikatenlogik zweiter Stufe. In: Memo Seki-85-11-KL. Universität Kaiserslautern, Fachbereich Informatik, 1985 (homepage.univie.ac.at [PDF]). 
• Manfred Schmidt-Schauß: A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. SE Modallogik und andere philosophisch relevante Logiken. WS 2015/2016. Universität Wien, S. 22. 
• Christoph Walther: A Mechanical Solution of Schubert’s Steamroller by Many-Sorted Resolution. In: Artif. Intell. 26 (2). Jahrgang, 1985, S. 217–224, doi:10.1016/0004-3702(85)90029-3 (englisch, tu-darmstadt.de [PDF]). 
• Christoph Walther: A Many-Sorted Calculus Based on Resolution and Paramodulation. In: Research Notes in Artificial Intelligence. Pitman, London 1987. 
• Hao Wang: Logic of many-sorted theories. In: Journal of Symbolic Logic. 17. Jahrgang, 1952, S. 105–116, doi:10.2307/2266241 (englisch). , Teil der Sammlung Computation, Logic, Philosophy. A Collection of Essays. Science Press, Beijing / Kluwer Academic, Dordrecht 1990.

1. ↑ Näheres siehe A. Oberschelp (1962) S. 297f.
2. ↑ Beispielsweise können Fehler bei Datentyp-Zuweisungen schnell (zur Compilezeit) als Syntaxfehler erkannt werden.
3. ↑ T {\displaystyle T} wird gedeutet als ein Alphabet von Sortenbezeichnern, siehe Alphabet (Informatik) und Alphabet (Mathematik).
4. ↑ Carlos Caleiro, Ricardo Gonçalves: Proc. 18th int. conf. on Recent trends in algebraic development techniques (WADT). Springer, 2006, ISBN 978-3-540-71997-7, On the algebraization of many-sorted logics, S. 21–36 (englisch, utl.pt [PDF]). 
5. ↑ Unter Sortierung versteht man in diesem Zusammenhang die Zuweisung zu Sorten, siehe Steimann (1991) S. 3.
6. ↑ mit dem Spezialfall des euklidischen Raumes
7. ↑ Anmerkung: Kruse, Borgelt (2008) S. 3 und S. 9 bezeichnen
   • die Menge der Sorten T {\displaystyle T} mit Θ {\displaystyle \Theta } und die Sorten selbst mit A , B , … {\displaystyle A,B,\dots } ,
   • die Einschränkung τ | F 0 {\displaystyle \tau |_{{\mathcal {F}}_{0}}} von τ {\displaystyle \tau } auf die Funktionssymbole mit Δ {\displaystyle \Delta } (eine Menge geordneter Paare),
   • die Einschränkung τ | R 0 {\displaystyle \tau |_{{\mathcal {R}}_{0}}} von τ {\displaystyle \tau } auf die Relationssymbole mit Π {\displaystyle \Pi } ,
   • die Variablendeklaration ν {\displaystyle \nu } mit Ω {\displaystyle \Omega } (genauer gesagt benutzen die Autoren eine Punktnotation, mit dem Punkt als zusätzlichem technischen Zeichen. Die Variablen werden nur in der Form x . s {\displaystyle x.s} benutzt mit dem eigentlichen Variablennamen x und einer Sorte s. Als Variablen in dem im Artikel hier gebrauchten Sinn mit Mengenbezeichnung V {\displaystyle {\mathcal {V}}} werden dann die Kombinationen, d. h. Zeichenketten x . s {\displaystyle x.s} mit einer impliziten Variablendeklaration β ( x . s ) = s {\displaystyle \beta (x.s)=s} benutzt. Dadurch kann der rohe Name x für mehrere Sorten verwendet werden),
   • die Signatur mit Σ = ( Θ , Δ , Π ) {\displaystyle \Sigma =(\Theta ,\Delta ,\Pi )} , was im obigen Text ( T , τ | F 0 , τ | R 0 ) {\displaystyle (T,\tau |_{{\mathcal {F}}_{0}},\tau |_{{\mathcal {R}}_{0}})} entspricht,
   • die Abbildung α {\displaystyle \alpha } (kennzeichnend für die S {\displaystyle {\boldsymbol {S}}} -Struktur) mit I {\displaystyle I} , und
   • die Variablenbelegung ν {\displaystyle \nu } mit β {\displaystyle \beta } .
8. ↑ T ∗ = ⋃ { T n | n ∈ N 0 } {\displaystyle T^{*}=\bigcup \{T^{n}|n\in \mathbb {N} _{0}\}} . Im Fall der Funktionssymbole, wo mindestens eine Sorte für den Wertebereich benötigt wird, liegen die Werte von τ {\displaystyle \tau } in der positiven Hülle T + = T ∗ ∖ { ∅ } = T ∗ ∖ ϵ {\displaystyle T^{+}=T^{*}\setminus \{\emptyset \}=T^{*}\setminus \epsilon } . Die Stelligkeit σ {\displaystyle \sigma } ist die Wortlänge des Typs τ {\displaystyle \tau } (minus 1 bei Funktionssymbolen).
9. ↑ mit dem leeren kartesischen Mengenprodukt bestehend aus dem leeren Wort (mengentheoretisch identisch mit der Leermenge): T 0 = { ∅ } = { ϵ } {\displaystyle T^{0}=\{\emptyset \}=\{\epsilon \}}
10. ↑ Brass, Stefan: Mathematische Logik mit Datenbank-Anwendungen. Martin-Luther-Universität Halle-Wittenberg, Institut für Informatik, Halle 2005, S. 176 (informatik.uni-halle.de [PDF]). 
    1. ↑ S. 16–19
    2. ↑ ^{a b} S. 20
    3. ↑ S. 54
    4. ↑ S. 56
    5. ↑ S. 59
    6. ↑ S. 66–68
11. ↑ Die beiden Familien definieren sich analog zum einsortigen Fall als die Urbildfasern der Einschränkungen von α {\displaystyle \alpha } auf die beiden Symbolmengen R 0 {\displaystyle {\mathcal {R}}_{0}} und F 0 {\displaystyle {\mathcal {F}}_{0}} : R s = ( α | R 0 ) − 1 ( { s } ) , F s , s ′ = ( α | F 0 ) − 1 ( { ( s , s ′ ) } ) {\displaystyle {\boldsymbol {\mathcal {R}}}_{s}=(\alpha |_{{\mathcal {R}}_{0}})^{-1}(\{s\}),\;{\boldsymbol {\mathcal {F}}}_{s,s'}=(\alpha |_{{\mathcal {F}}_{0}})^{-1}(\{(s,s')\})}
12. ↑ 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 S {\displaystyle {\mathcal {S}}} statt T {\displaystyle T} bezeichnet.
13. ↑ Steimann, Friedrich: Ordnungssortierte Feature-Logik und Dependenzgrammatiken in der Computerlinguistik. Monographien. FernUni, Fakultät Mathematik und Informatik, LG Programmiersysteme, Hagen 31. Januar 2011, S. 104 (fernuni-hagen.de – Diplomarbeit). , bei: fernuni-hagen.de (PDF; 6,3 MB). Original bei: Universität Karlsruhe 1992, Institut für Logik, Komplexität und Deduktionssysteme. Der Autor beschreibt über das Thema hier hinausgehend eine ordnungssortierte Feature-Logik erster Stufe, d. h. Argumente haben Namen und können als Schlüsselwortparameter referenziert werden.
    1. ↑ ^{a b} S. 5
    2. ↑ ^{a b} S. 7
    3. ↑ ^{a b} S. 6
    4. ↑ S. 6 f
14. ↑ siehe auch Korrespondenz.
15. ↑ A. Oberschelp (1989/1990) Seite 10.
16. ↑ das ist dann auch die Sorte der logischen Konstanten als nullstelligen Relationen.
17. ↑ Relationen lassen sich also als spezielle Funktionen auffassen, umgekehrt sind Funktionen spezielle (linkstotal-rechtseindeutige) Relationen.
18. ↑ Zur hier verwendeten Maplet-Schreibweise ν ⟨ x ↦ s ⟩ {\displaystyle \nu _{\langle x\mapsto s\rangle }} (anstelle des von S. Brass verwendeten Schrägstrichs ν ⟨ x / s ⟩ {\displaystyle \nu \langle {x/s}\rangle } oder ν s x {\displaystyle \nu {\frac {s}{x}}} ) siehe Klaus Grue (1995) S. 11.
19. ↑ A. Oberschelp (1989/1990) Seite 9ff.
20. ↑ F. Bry (1999/2.10) Def. 2.10.1.
21. ↑ C. Lutz (2010) S. 6 und 8.
22. ↑ Ramharter, Eder (2015/16) S. 17. Die Autoren kennzeichnen die Stelligkeit der Relationsvariablen mit einem Index.
23. ↑ Grädel, Erich: Mathematische Logik. Mathematische Grundlagen der Informatik. SS 2009. RWTH, Aachen, S. 129 (cs.uni-dortmund.de [PDF]). 
    1. ↑ S. 1
    2. ↑ S. 1 f
24. ↑ Kruse, Stefan; Borgelt, C.: Grundbegriffe der Prädikatenlogik. Computational Intelligence. Otto-von-Guericke Universität, Magdeburg 2008, S. 14 (fuzzy.cs.ovgu.de [PDF]). 
    1. ↑ S. 4
    2. ↑ S. 9
25. ↑ Kleine Büning (2015), S. 5 ff.
26. ↑ Ausführliche Darstellung: Kleine Büning (2015), S. 8–15.
27. ↑ D. h. im Skopus (Wirkungsbereich) des jeweiligen Quantors gilt eine lokal modifizierte Variablendeklaration (auch ( x {\displaystyle x} -)Variante genannt) ν ′ = ν ⟨ x ↦ s ⟩ {\displaystyle \nu '=\nu _{\langle x\mapsto s\rangle }} mit beliebigen x ∈ V , s ∈ T {\displaystyle x\in {\mathcal {V}},s\in T} und

    ν ′ ( y ) = ν ⟨ x ↦ s ⟩ ( y ) := { s wenn   y = x , ν ( y ) sonst (auf dem ursprünglichen Definitionsbereich von   ν ) ; {\displaystyle \nu '(y)=\nu _{\langle x\mapsto s\rangle }(y):={\begin{cases}s&{\text{wenn}}\ y=x,\\\nu (y)&{\text{sonst (auf dem ursprünglichen Definitionsbereich von}}\ \nu {\text{)}};\end{cases}}}

    Siehe Stefan Brass (2005) S. 56, sowie Ramharter, Eder (2015/16) S. 17. Für den Fall, dass x {\displaystyle x} bereits außerhalb der Quantoren deklariert ist, d. h. wenn x {\displaystyle x} bereits im ursprünglichen Definitionsbereich der Deklaration ν {\displaystyle \nu } enthalten ist, wird diese lokal überschrieben. Eine Variable im Skopus eines Quantors (wie hier x {\displaystyle x} ) nennt man eine gebundene Variable.
28. ↑ mit A ∘ t = ( A t i ) i ∈ { 1 … n } {\displaystyle A\circ t=(A_{t_{i}})_{i\in \{1\dots n\}}} (Familienschreibweise), ∏ A ∘ t = ∏ i ∈ { 1 … n } A t i {\displaystyle \textstyle \prod A\circ t=\textstyle \prod _{i\in \{1\dots n\}}A_{t_{i}}} , wobei n := | t | {\displaystyle n:=|t|} (Wort- oder Tupellänge von t {\displaystyle t} ).
29. ↑ Siehe Stefan Brass (2005), S. 29; der Autor benutzt die Notation I {\displaystyle {\mathcal {I}}} statt α {\displaystyle \alpha } . σ ( R ) {\displaystyle \sigma (R)} bezeichnet wie im einsortigen Fall die Stelligkeit von R {\displaystyle R} , hier gegeben durch die (Wort-)länge des Typs τ ( R ) {\displaystyle \tau (R)} . Vereinfacht: ohne Überladung.
30. ↑ Konstanten sind hier als nullstellige Funktionen aufgefasst. Ansonsten käme zum Wertebereich A {\displaystyle {\boldsymbol {A}}} von α {\displaystyle \alpha } noch ein weiterer Anteil ⋃ s ∈ T A s {\displaystyle \textstyle \bigcup _{s\in T}A_{s}} hinzu (dieser entspricht A {\displaystyle A} im einsortigen Fall).
31. ↑ Tatsächlich ist wegen der Disjunktheit von T {\displaystyle T} , F 0 {\displaystyle {\mathcal {F}}_{0}} und R 0 {\displaystyle {\mathcal {R}}_{0}} egal, ob man die einzelnen Abschnitte mit Komma oder ∪ {\displaystyle \cup } trennt. Ein Tupel von Familien mit disjunkten Indexmengen ist isomorph zu einer Familie mit der vereinigten Indexmenge. In diesem Sinn ist die S {\displaystyle {\boldsymbol {S}}} -Struktur A {\displaystyle {\mathcal {A}}} bis auf Isomorphie identisch mit der Interpretationsfunktion (Familie) α {\displaystyle \alpha } oder mit ( α | T , α | F 0 , α | R 0 ) {\displaystyle (\alpha |_{T},\alpha |_{{\mathcal {F}}_{0}},\alpha |_{{\mathcal {R}}_{0}})} . Siehe auch Einschränkung, § Verträglichkeitsregeln.
32. ↑ Werden die Variablen, die gemäß Deklaration ν {\displaystyle \nu } einer Sorte s ∈ T {\displaystyle s\in T} zugeordnet sind, mit V ν , s {\displaystyle {\mathcal {V}}_{\nu ,s}} bezeichnet (= Urbildfaser von s {\displaystyle s} unter ν {\displaystyle \nu } ), dann ist die Einschränkung der Belegung β {\displaystyle \beta } auf diese Variablen eine (ggf. partielle) Abbildung V ν , s ↛ A s {\displaystyle {\mathcal {V}}_{\nu ,s}\not \to A_{s}}
33. ↑ alternative Bezeichnungen: ⊆ {\displaystyle \subseteq } , ⊑ {\displaystyle \sqsubseteq }
34. ↑ A. Oberschelp (1989) Seite 11ff.
35. ↑ Christoph Walter (1985).
36. ↑ int steht für integer, Wertebereich ist ⟨ m , n ⟩ = { m , m + 1 , … n − 1 , n } {\displaystyle \langle m,n\rangle =\{m,m+1,\dots n-1,n\}} , für n = m {\displaystyle n=m} einfach { m } {\displaystyle \{m\}} . Siehe Folge, § Formale Definition: endliche Folgen.
37. ↑ Umgekehrt wird in C bei der if-Abfrage jedes Argument ungleich 0 als wahr, und nur 0 als falsch gewertet.
38. ↑ A. Oberschelp (1989/1990) Seite 11ff.
39. ↑ Steimann 1992, S. 5. Der Autor bezeichnet das Sortenalphabet als S {\displaystyle \operatorname {S} } mit Halbordnung ≤ {\displaystyle \leq } , die Symbolmenge mit Σ {\displaystyle \Sigma } und die ordnungssortierte Signatur entsprechend mit ( S , ≤ , Σ ) . {\displaystyle (\operatorname {S} ,\leq ,\Sigma ).}
40. ↑ Gloede, Mengenlehre, 2004.
41. ↑ oder s 1 ∩ s 2 {\displaystyle s_{1}\cap s_{2}} , s 1 ⊓ s 2 {\displaystyle s_{1}\sqcap s_{2}}
42. ↑ d. h. falls keine Überladung vorliegt ist ( w ′ , s ′ ) := τ ( f ) {\displaystyle ({\boldsymbol {w}}',s'):=\tau (f)}
43. ↑ Oberschelp 1989/90 S. 14 f.
44. ↑ Smolka, Gert: Logic Programming over Polymorphically Order-Sorted Types. Universität Kaiserslautern, Mai 1989. 
45. ↑ Schmidt-Schauß, Manfred: Computational Aspects of an Order-Sorted Logic with Term Declarations (= LNAI. Band 395). Springer, April 1988. 
46. ↑ Siehe Parameter, § Unterschiedliche Parameter-Begriffe.