one may replace the three axioms FALSE, NOT-1', and NOT-2' with the two axioms
* NOT-1:
* NOT-2: as at . Alternatives to NOT-1 are or .

Equivalence

The connective for equivalence may be treated as an abbreviation, with standing for . Alternatively, one may add the axioms

* IFF-1:
* IFF-2:
* IFF-3:

IFF-1 and IFF-2 can, if desired, be combined into a single axiom using conjunction.

Sequent calculus