Sortenlogik

Beispiele

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

Definition

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

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

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

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

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

Terme in vielsortiger Logik

Definition

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

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

Die Menge aller Terme ${\displaystyle {\boldsymbol {\mathcal {T}}}_{{\boldsymbol {S}},\nu }}$ ist gegeben durch die disjunkte Vereinigung der ${\displaystyle T_{{\boldsymbol {S}},\nu }(s)}$ über alle nichtlogischen Sorten ${\displaystyle s\in T\setminus \{\operatorname {logical} \}}$. Bei leerer Variablendeklaration kann der Index ${\displaystyle \nu }$ entfallen: ${\displaystyle {\mathcal {T}}_{\boldsymbol {S}}(s),\ {\boldsymbol {\mathcal {T}}}_{\boldsymbol {S}}}$.
Durch die Funktionssymbole werden Verknüpfungen verschiedenen Typs zwischen den Elementen der ${\displaystyle {\boldsymbol {\mathcal {T}}}_{{\boldsymbol {S}},\nu }}$ bzw. ${\displaystyle {\mathcal {T}}_{\boldsymbol {S}}(s)}$ der verschiedenen Sorten ${\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: ${\displaystyle x+1}$ statt ${\displaystyle +(x,1)}$, wie oben. Präfixform: Klammerfreie Polnische Notation, ebenfalls wie oben. Seltener: Postfixnotation.
• Punktnotation ${\displaystyle x.\operatorname {farbe} }$ statt ${\displaystyle \operatorname {farbe} (x)}$, ${\displaystyle x.\operatorname {plus} (y)}$ statt ${\displaystyle x\operatorname {plus} y}$ (wie in der objektorientierten Programmierung).
• Neuerdings gewinnt die Baumdarstellung von Termen zunehmend an Bedeutung.

Ausdrücke in vielsortiger Logik

Definition

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

• ${\displaystyle t_{1}=t_{2}}$ für alle Terme ${\displaystyle t_{1},t_{2}}$ derselben Sorte ${\displaystyle s\in T}$.
• Alle Aussagenvariablen, sofern diese Sorte zugelassen ist.
• ${\displaystyle Rt_{1},\dots t_{k}}$ für alle ${\displaystyle k}$-stelligen Relationssymbole vom Typ ${\displaystyle (s_{1},\dots s_{k})}$, wenn ${\displaystyle t_{1}}$ Term der Sorte ${\displaystyle s_{1}\in T}$, ${\displaystyle t_{2}}$ Term der Sorte ${\displaystyle t_{2}\in T}$, ${\displaystyle \dots }$ ${\displaystyle t_{k}}$ Term der Sorte ${\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.
• ${\displaystyle (\exists x:s\ \varphi )}$ und ${\displaystyle (\forall x:s\ \varphi )}$ sind Ausdrücke, wenn ${\displaystyle s\in T}$ eine Sorte, ${\displaystyle x\in {\mathcal {V}}}$ ein Variablensymbol, und ${\displaystyle \varphi }$ ein Ausdruck ist, in dem die lokale Variable ${\displaystyle x}$ der Sorte ${\displaystyle s}$ vorkommt.

Anmerkung

Relationen können als Prädikate aufgefasst werden, d. h. als (Boolesche) Funktionen mit gleicher Stelligkeit und Argumenttyp sowie dem Wertebereich ${\displaystyle \{\operatorname {falsch} ,\operatorname {wahr} \}}$, d. h. der Bildsorte ${\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 ${\displaystyle \operatorname {logical} }$’.

Interpretation

Semantik einer vielsortigen Signatur

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

• ${\displaystyle \alpha (s)=A_{s}}$ sei für jede Sorte ${\displaystyle s\in T}$ ein Wertebereich (Grundmenge)
• ${\displaystyle \alpha (R)\subseteq A_{\tau (R)_{1}}\times \cdots A_{\tau (R)_{\sigma (R)}}}$ eine Relation für jedes ${\displaystyle R\in {\mathcal {R}}_{0}}$, und
• ${\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 ${\displaystyle f\in {\mathcal {F}}_{0}}$.

Dann nennt man ${\displaystyle \alpha }$ eine Interpretationsfunktion und ${\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 ${\displaystyle {\boldsymbol {S}}}$ oder ${\displaystyle {\boldsymbol {S}}}$-Struktur.

Überladung

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

${\displaystyle \alpha _{\boldsymbol {s}}(R)\subseteq A_{{\boldsymbol {s}}_{1}}\times \cdots A_{{\boldsymbol {s}}_{n}}}$,

${\displaystyle \alpha _{\boldsymbol {s}}(f):A_{{\boldsymbol {s}}_{1}}\times \cdots A_{{\boldsymbol {s}}_{n}}\to A_{s'}}$.

Dabei ist die Stelligkeit ${\displaystyle n}$ hier gegeben ist durch die (Wort-)Länge ${\displaystyle n=|{\boldsymbol {s}}|}$ des Argumenttyps ${\displaystyle {\boldsymbol {s}}}$, und ${\displaystyle s'}$ ist die durch den Argumenttyp eindeutig bestimmte Bildsorte ${\displaystyle s'=\tau (f)_{n+1}.}$
Es handelt sich um partielle Abbildungen, nur für Typen ${\displaystyle {\boldsymbol {s}}}$ mit ${\displaystyle {\boldsymbol {\mathcal {R}}}_{t}\neq \emptyset }$ bzw. ${\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 ${\displaystyle {\mathcal {V}}}$, die deklarierte Variablen ${\displaystyle x}$ aus ${\displaystyle {\mathcal {V}}}$ auf Elemente der zugehörigen Sorte ${\displaystyle \nu _{x}=\nu (x)}$ (d. h. aus dem Wertebereich ${\displaystyle A_{\nu _{x}}}$) abbildet, heißt eine Belegung der vielsortigen ${\displaystyle {\boldsymbol {S}}}$-Struktur ${\displaystyle {\mathcal {A}}}$.

Für eine Interpretation ${\displaystyle {\boldsymbol {I}}}$ der Signatur ${\displaystyle {\boldsymbol {S}}}$ werden jetzt die Komponenten ${\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.

Beispiele

• Im obigen Beispiel wäre etwa

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

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

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

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

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

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

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

und so weiter.

• Modellierung der Verhältnisse bei den Zahlenbereichen:

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

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

• In manchen Programmiersprachen (wie Pascal und Modula-2) dienen ganzzahlige Intervalle als Datentypen: Seien ${\displaystyle m,n\in \mathbb {Z} }$ mit ${\displaystyle m\leq n}$, dann gilt für den Intervall-Datentyp ${\displaystyle m.\!.n\preceq \operatorname {int} }$ 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 ${\displaystyle \operatorname {logical} }$ Überschneidungen mit anderen Sorten hat. Die Wahrheitswerte ${\displaystyle \operatorname {false} }$ und ${\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. In einer Erweiterung könnten die logischen Werte einer dreiwertigen Logik oder einfachen Fuzzy-Logik mit Zahlen aus dem reellen Intervall ${\displaystyle [0,1]}$ gleichgesetzt werden, so dass in allen Fällen gilt: ${\displaystyle \operatorname {logical} \preceq \operatorname {real} }$

Vorgehensweise

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

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

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

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

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

Reguläre Signatur

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

${\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.

Zulässige Signatur

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

• Wenn für ${\displaystyle f:{\boldsymbol {s}}\longrightarrow s'}$ und ${\displaystyle f:{\boldsymbol {w}}\longrightarrow w'}$ mit ${\displaystyle {\boldsymbol {s}},{\boldsymbol {w}}\in T^{*},s',w'\in T}$ gilt ${\displaystyle {\boldsymbol {w}}{\boldsymbol {\preceq }}{\boldsymbol {s}}}$, dann gilt auch ${\displaystyle w\preceq s}$
• Es kann keine unendliche Ketten ${\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 ${\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 ${\displaystyle \operatorname {gcs} (s_{1},s_{2})}$. Notfalls kann aber eine geeignete neue Sorte ${\displaystyle r}$ zum Sortenalphabet ${\displaystyle T}$ hinzugenommen werden, damit dann ${\displaystyle r=\operatorname {gcs} (s_{1},s_{2})}$ erfüllt wird. Auf Objetebene besagt die Bedingung nichts anderes, als dass die Schnittmenge zweier Wertebereiche ${\displaystyle A_{s_{1}}}$ und ${\displaystyle A_{s_{2}}}$ (als größte gemeinsame Teilmenge) entweder leer ist, oder aber Wertebereich zu einer geeigneten Sorte ${\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 ${\displaystyle s_{1},s_{2}\in T}$ mit Ausnahme der Disjunktheit deren ggU ${\displaystyle \operatorname {gcs} (s_{1},s_{2})}$ ebenfalls erklärtes Mitglied der Sortenmenge ${\displaystyle T}$ ist
• Für alle ${\displaystyle s\in T,{\boldsymbol {w}}\in T^{*},f\in {\mathcal {F}}_{0}}$ mit ${\displaystyle f:{\boldsymbol {w}}'\longrightarrow s'}$ ist auch die Menge

  ${\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. Alle Funktions- und Relationssymbole ${\displaystyle +,-,\cdot ,/,\leq ,\dots }$ müssten andernfalls für jeden Zahlenbereich ${\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 ${\displaystyle \mathbb {C} ,\mathbb {A} ,\mathbb {R} ,\mathbb {Q} }$ mit den komplex-algebraischen Zahlen ${\displaystyle \mathbb {A} }$ und den Ketten ${\displaystyle \mathbb {Q} \subseteq \mathbb {R} \subseteq \mathbb {C} }$ und ${\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 ${\displaystyle \mathbb {A} \cap \mathbb {R} }$ eine Menge mit fehlenden Sortenzeichen, was der Vollständigkeit halber nachzutragen wäre.

Variablen in ordnungssortierter Logik

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 ${\displaystyle \nu$ :{\mathcal {V}}\to T} festzulegen.

Termauswertung in ordnungssortierter Logik

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

• für Variablen ${\displaystyle v\in {\mathcal {V}}}$: ${\displaystyle {\mathcal {S}}(v)=\{r\in T|\nu (v)\preceq r\}}$ (Oberhalbmeng von ${\displaystyle \nu (v)}$)
• für Konstanten ${\displaystyle c}$: ${\displaystyle {\mathcal {S}}(c)=\{r\in T|\tau (c)\preceq r\}}$
• für Funktionen ${\displaystyle f}$: ${\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'\}}$

Beispiel

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