first-order logic axiom First-order logic axioms MAY be provided if the term is primitive ('is primitive' is true ) or non-primitive. A construct MAY include more than one first-order logic axiom annotation. logic axiom annotation written in first order logic logic axiom