  Łukasiewicz formulated several axiomatic bases for the functionally complete propositional calculus, that is PC in which all 16 binary connectives can be defined. The most popular is the N-C system, having as axioms the formulas: CCpqCCqrCpr, CCNppp, CpCNpq, and the usual rules of inference (substitution, detachment). This system is consistent, independent, Post-complete (= semantically complete): Łukasiewicz and his collaborators invented new methods for proving these properties. According to the criteria mentioned in the preceding section, one should look for the simplest axiom bases.