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_ &   ; 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.