2.3 Axioms

      AXIOM-ITEMS ::= axiom-items AXIOM+     
      AXIOM       ::= FORMULA

A list AXIOM-ITEMS of axioms is written:

axioms F₁; ... F_n;

Each well-formed axiom determines a sentence of the underlying basic specification (closed by universal quantification over all declared variables).

      FORMULA ::= QUANTIFICATION | CONJUNCTION | DISJUNCTION 
                | IMPLICATION | EQUIVALENCE | NEGATION | ATOM

A formula is constructed from atomic formulae of the form ATOM using quantification and the usual logical connectives.

Keywords in formulae and terms are displayed in the same font as identifiers.