[[Syntax]] | [[Terms]] | [[Equations]] | [[Horn formulas]] | [[Universal formulas]] | [[First-order formulas]] | [[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_ &nbsp; 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.