This is an old revision of the document!


Syntax | Terms | Equations | Quasiequations | Theories

Variables

$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

Connectives

0-ary connectives

Unary connectives

⋄ □

Binary connectives

Infix: and ∧ or ∨ ⇒ ⇔

Mixfix: if_then_ &   ; while_do_

Ternary connectives

if_then_else_

Quadternary connectives

n-ary connectives

ω-ary connectives

κ-ary connectives

∞-ary connectives

Quantifiers

∀ ∃

Delimiters

( ) [ ] { } 〈 〉

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.