Table of Contents
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.