A form of axiom.

One of the primitive judgments.

Example:

axiom [symmety_r] r(X,Y) -> r(Y,X)

The free variables X and Y in the formula are taken as universally quantified.

The text symmetry_r between brackets is the name for an axiom and is optional.