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.