This is an old revision of the document!

Syntax | Terms | Equations | Quasiequations | Theories


$x$ $y$ $z$ $u$ $v$ $w$ $x_0$ $x_1$ $x_2$ …

Operation symbols

Constant symbols

$a$ $b$ $c$ $d$ $e$ $\bot$ $\top$ $\emptyset$ $\infty$ $0$-$9$ $\alpha-\omega$

Unary operation symbols

Prefix: $f$ $g$ $h$ $-$ $\neg$ $\sim$

Postfix: $'$ ${}^{-1}$ ${}^{\cup}$

Binary operation symbols

Prefix: $f$ $g$ $h$

Infix: $+$ $-$ $*$ $\cdot$ $\times$ $\div$ $/$ $\backslash$ $\circ$ $\oplus$ $\otimes$ $\odot$ $\wedge$ $\vee$ $\to$

Ternary operation symbols

Prefix: $t$

Quadternary operation symbols

Prefix: $q$

$n$-ary operation symbols

Prefix: $\sum_n$ $\prod_n$

Mixfix: {_} [_] (_)

$\omega$-ary operation symbols

$\sum_\omega$ $\prod_\omega $\kappa$**-ary operation symbols** $\sum_\kappa$ $\prod_\kappa

$\infty$-ary operation symbols

$\sum$ $\prod$ $\bigcap$ $\bigcup$ $\bigwedge$ $\bigvee$ = Relation symbols =

0-ary relation symbols

Propositions ⊥ ⊤ T F

Unary relation symbols

Prefix: P Q

Binary relation symbols

Prefix: R

Infix: = ≠ ≤ < ≥ > ⪯ ≺ ⪰ ≻ ≡ ≅ ≈ ∈ ∉

Ternary relation symbols

Quadternary relation symbols

n-ary relation symbols

ω-ary relation symbols

κ-ary relation symbols

∞-ary relation symbols


0-ary connectives

Unary connectives

⋄ □

Binary connectives

Infix: and ∧ or ∨ ⇒ ⇔

Mixfix: if_then_ &   ; while_do_

Ternary connectives


Quadternary connectives

n-ary connectives

ω-ary connectives

κ-ary connectives

∞-ary connectives


∀ ∃


( ) [ ] { } 〈 〉

Signatures / Languages

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.