−Table of Contents
Syntax | Terms | Equations | Horn formulas | Universal formulas | First-order formulas | Theories
Variables
x y z u v w x0 x1 x2 …
Operation symbols
- Constant symbols
- a b c d e ⊥ ⊤ ∅ ∞ 0-9 α−ω
- Unary operation symbols
- Prefix: f g h − ¬ ∼
- Postfix: ′ −1 ∪
- Binary operation symbols
- Prefix: f g h
- Infix: + − ∗ ⋅ × ÷ / ∖ ∘ ⊕ ⊗ ⊙ ∧ ∨ →
- Ternary operation symbols
- Prefix: t
- Quadternary operation symbols
- Prefix: q
- n-ary operation symbols
- Prefix: ∑n ∏n
- Mixfix: { } [ ] ( )
- ω-ary operation symbols
- ∑ω ∏ω
- κ-ary operation symbols
- ∑κ ∏κ
- ∞-ary operation symbols
- ∑ ∏ ⋂ ⋃ ⋀ ⋁
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.