 Universal quantification is often given an alternative axiomatisation using an extra rule of generalisation (see the section on Metatheorems), in which case the rules Q6 and Q7 are redundant.The final axiom schemes are required to work with formulas involving the equality symbol.It is common to include in a Hilbert-style deduction system only axioms for implication and negation.