Four redundant axiomatics