Does There Exist A Fourth Independent Axiom Here?

175 Views Asked by At

I use Polish notation.

The implicational calculus of propositions under detachment and uniform substitution has the following axioms as a basis:

1 CpCqp
2 CCpCqrCCpqCpr
3 CCCpqpp

If one joins to this system say

4 CCNpNqCqp or 
5 CCNpNqCCNpqp

one obtains a basis for all C-N tautologies (conditional-negation tautologies... that is all tautologies which only have "C" and "N" connectives can get obtained from such an axiom set). But, if we do such, then the axioms are no longer independent, since both {1, 2, 5} and {1, 2, 4} allow us to deduce CCCpqpp. So, does there exist an axiom which we can join to the above three axioms... the set {1, 2, 3} ... for a basis for C-N calculus which keeps all of the axioms independent?