Syntax | Terms | Equations | Horn formulas | Universal formulas | First-order formulas | Theories
$x$ $y$ $z$ $u$ $v$ $w$ $x_0$ $x_1$ $x_2$ …
A signature or language is a sequence of operation symbols, relation symbols and connectives.
Prefix symbols always apply first. Infix symbols and postfix symbols can
In a typed (or multisorted) language the input/output slots of operation symbols and relation symbols are associated to a specific type.
In an order-sorted language the types form a partially ordered set that determines the subtyping relation.