Processing math: 100%

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


QR Code
QR Code syntax (generated for current page)