John Kalman's book on OTTER on page 217 has the following problem:

"In [this newsletter], Morgan essentially proposed the following problem.

Problem 8.6 Use an automatic theorem-prover to find a proof that the propositional formula CpNNp is derivable by the of condensed detachment from the propositional formulas CpCqp, CCpCqrCCpqCpr, and CCpqCNqNp."

This problem isn't solvable.  Let 0 be the designated element.  Suppose we have only two values "0" and "1", and C(0,x)=x, C(1,x)=0, and N(x)=1.  Then, CpCqp, CCpCqrCCpqCpr, and CCpqCNqNp are satisfied, but CpNNp is not.

Axiomatic proofs which prove an alternative basis for a propositional calculus can often get used to extract more axiom sets for that same propositional calculus.  Even proving a single axiom of a distinct basis can tell you about other bases which exist.

For example, let's suppose that we start with the Church-Lukasiewicz basis {CxCyx, CCxCyzCCxyCxz, CCNxNyCyx} and want to derive Lukasiewicz's preferred basis {CCxyCCyzCxz, CCNxxx, CxCNxy}.  OTTER found this proof of Clavius: CCNppp:

Length of proof is 14.  Level of proof is 6.

---------------- PROOF ----------------

1 [] P(C(x,C(y,x))).
2 [] P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
3 [] P(C(C(N(x),N(y)),C(y,x))).
4 [] -P(C(x,y))| -P(x)|P(y).
7 [] -P(C(C(N(p),p),p)).
10 [hyper,4,2,2] P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).
11 [hyper,4,2,1] P(C(C(x,y),C(x,x))).
12 [hyper,4,1,3] P(C(x,C(C(N(y),N(z)),C(z,y)))).
14 [hyper,4,1,1] P(C(x,C(y,C(z,y)))).
17 [hyper,4,11,1] P(C(x,x)).
19 [hyper,4,1,17] P(C(x,C(y,y))).
24 [hyper,4,1,19] P(C(x,C(y,C(z,z)))).
31 [hyper,4,10,14] P(C(C(x,C(C(y,x),z)),C(x,z))).
33 [hyper,4,10,24] P(C(C(x,C(C(y,y),z)),C(x,z))).
38 [hyper,4,2,12] P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).
163 [hyper,4,31,12] P(C(N(x),C(x,y))).
191 [hyper,4,2,163] P(C(C(N(x),x),C(N(x),y))).
357 [hyper,4,38,191] P(C(C(N(x),x),C(y,x))).
371 [hyper,4,33,357] P(C(C(N(x),x),x)).
372 [binary,371.1,7.1] $F.

Since we know that {CCxyCCyzCxz, CCNxxx, CxCNxy} is a basis, and CCNxxx can get derived from formulas 33 and 357 above, we can replace CCNxx by formulas 33 and 357 above to get another basis.  Doing this we find that {P(C(C(x,y),C(C(y,z),C(x,z))))., P(C(x,C(N(x),y)))., P(C(C(N(x),x),C(y,x)))., P(C(C(x,C(C(y,y),z)),C(x,z))).} is a basis.  Furthermore, formula 357 P(C(C(N(x),x),C(y,x))). can get replaced by formulas 38 and 191.  Thus, {P(C(C(x,y),C(C(y,z),C(x,z))))., P(C(x,C(N(x),y)))., P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).,  P(C(C(N(x),x),C(N(x),y)))., P(C(C(x,C(C(y,y),z)),C(x,z))).} is a basis.  Continuing this process we can infer that {P(C(C(x,y),C(C(y,z),C(x,z))))., P(C(x,C(N(x),y)))., P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).,  P(C(N(x),C(x,y)))., P(C(C(x,C(y,z)),C(C(x,y),C(x,z))))., P(C(C(x,C(C(y,y),z)),C(x,z)))}.

For many proofs of an alternative we can ask, what is the first alternative basis that gets derived in the proof?  OTTER found this proof:

Length of proof is 22.  Level of proof is 6.

---------------- PROOF ----------------


1 [] P(C(x,C(y,x))).
2 [] P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).
3 [] P(C(C(N(x),N(y)),C(y,x))).
4 [] -P(C(C(p,q),C(C(q,r),C(p,r))))| -P(C(C(N(p),p),p))| -P(C(p,C(N(p),q)))|$ANS(all).
5 [] -P(C(x,y))| -P(x)|P(y).
8 [hyper,5,2,2] P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))).
9 [hyper,5,2,1] P(C(C(x,y),C(x,x))).
10 [hyper,5,1,3] P(C(x,C(C(N(y),N(z)),C(z,y)))).
11 [hyper,5,1,2] P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))).
12 [hyper,5,1,1] P(C(x,C(y,C(z,y)))).
15 [hyper,5,9,1] P(C(x,x)).
17 [hyper,5,1,15] P(C(x,C(y,y))).
22 [hyper,5,1,17] P(C(x,C(y,C(z,z)))).
25 [hyper,5,1,12] P(C(x,C(y,C(z,C(u,z))))).
29 [hyper,5,8,12] P(C(C(x,C(C(y,x),z)),C(x,z))).
31 [hyper,5,8,22] P(C(C(x,C(C(y,y),z)),C(x,z))).
36 [hyper,5,2,10] P(C(C(x,C(N(y),N(z))),C(x,C(z,y)))).
79 [hyper,5,8,25] P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))).
160 [hyper,5,29,11] P(C(C(x,y),C(C(z,x),C(z,y)))).
161 [hyper,5,29,10] P(C(N(x),C(x,y))).
166 [hyper,5,2,160] P(C(C(C(x,y),C(z,x)),C(C(x,y),C(z,y)))).
189 [hyper,5,2,161] P(C(C(N(x),x),C(N(x),y))).
355 [hyper,5,36,189] P(C(C(N(x),x),C(y,x))).
369 [hyper,5,31,355] P(C(C(N(x),x),x)).
2037 [hyper,5,79,160] P(C(C(C(x,y),z),C(y,z))).
2127 [hyper,5,2037,189] P(C(x,C(N(x),y))).
14555 [hyper,5,2037,166] P(C(C(x,y),C(C(y,z),C(x,z)))).
14837 [hyper,4,14555,369,2127] $ANS(all).

I'll use numerals here.  What is the first basis derived in this proof which doesn't have any members in common with the axiom set?  {14555, 2127, 369} is the targeted basis.  Thus, {2037, 166, 2127, 369} is a basis.  So is {2037, 166, 189, 369}, {79, 160, 166, 189, 369}, {79, 160, 166, 189, 31, 355}, {79, 160, 166, 189, 31, 36}.  We don't replace 189 by its parents, since 2 is in the initial axiom set.  Nor do we replace 166 for the same reason.  {79, 29, 11, 166, 189, 31, 36} is another basis.  {8, 25, 29, 11, 166, 189, 31, 36} is another basis.  36 doesn't get replaced by its parents, but 31 does yielding {8, 25, 29, 11, 166, 189, 22, 36} as a basis.  {8, 25, 12, 11, 166, 189, 22, 36} is another basis.  Consequently, contrary to what I expected when I posed the question above, there exist a few bases which get derived at the same time.  That said, the proof of the sufficiency of the Church-Lukasiewicz basis does happen in a unique number of steps in this proof.  In other words, if we already knew about these bases, then the last 5 steps of the proof above (excluding the step which derives the empty clause) would not come as necessary to derive a distinct basis.

The following gives us a proof of ECpqANpq with an adaptation of an idea in Arthur Prior's Formal Logic p. 65-66.

First formation rules:

1. All lower case letters of the Latin alphabet are formulas.
2. If x is a formula, then δx is a formula.
3. If x is a formula, then Nx is a formula.
4. If x and y are formulas, then C x y is a formula (spaces can get ignored or inserted freely).

Let "0" stand for falsity, and "1" for truth. We have the following matrix for implication "C", disjunction (or equivalently alternation) "A", and negation "N".

C | 0  1|  A| 0  1|  N
----------------------
0 | 1  1|  0| 0  1|  1
1*| 0  1|  1| 1  1|  0

This gives us the equations C00 =1, C01=1, C10=0, C11=1, A00=0, A01=1, A10=1, A11=1, N0=1, N1=0.
δ stands for a functioral variable. Paraphrasing Prior, where x is a formula, δx stands for any truth-function into which δ enters as argument. δa stands for any truth-function of b, such as Nb, Abb, Aab, CNba, CCbcCCabCac. δb can also stand for b itself. Substitution for δ occurs by putting the argument of δ into the position where an " ' " symbol appears. The notation x/y indicates that x is to get substituted with y for all instances of x in the formula in which x appears. For example, the substitution instruction δ/C ' ' in δr yields Crr. δ/C ' A ' p in C δr δp yields C CrArp CpApp. The substitution δ/' in say C δp δ1 just has us dropping δ yielding Cp1. δ/A ' C ' ' in C δp A δq δ Na yields C ApCpp A AqCqq CNaANaNa.
Note that the valuation function "v", v(C x y)=C v(x) v(y). Also, for the valuation function v(δx)=δv(x).
Now it turns out that the following is a meta-theorem.
Meta-Theorem 1: If v(x)=v(y), then v(C δx δy)=1. In other words, if x=y, then C δx δy follows.
Demonstration: Suppose v(x)=v(y). Since v(C00)=1, and v(C11)=1, it follows that for all p, v(Cpp)=1. Substituting p/δx in Cpp we then obtain that v(C δx δx)=1. Since v(C x y)=C v(x) v(y), it then follows that C v(δx) v(δx)=1. Since v(δx)=δv(x), it then follows that C δv(x) δv(x)=1. By the initial supposition, we then obtain that C δv(x) δ v(y)=1. Since v(δx)=δv(x) we then obtain that
C v(δx) v(δy)=1. From v(C x y)=C v(x) v(y) we thus obtain that v(C δx δy)=1. Therefore, if v(x)=v(y), then v(C δx δy)=1.
The upshot here comes as that an equation like Cxy=z gives us C δz δCxy. The suggested formulas from the above equations immediately following the table along with the axioms "C δ0 C δ1 δp" and "1", and "C Cpq C Cqp Epq" give us an axiom set here.
Let the notation 1 x/y * C 2-3 indicate that in formula 1 x gets substituted with y. This matches the formula which starts with C has 2 as its next part, and 3 as its last part. We then detach formula 3. The notation 4 x/y C 5-C 6-7 indicates that 4 matches the formula C5-C6-7. Since we already have formulas 5 and 6, we thus detach formula 7.
To see how the plan of writing the deduction proceeds, I'll write out the following calculation:

                         |-C C00 AN00=C 1 AN00=C 1 A10=C 1 1=1
            |-C C0q AN0q-|
            |            |-C C01 AN01=C 1 AN01=C 1 A11=C 1 1=1
 C Cpq ANpq-|
            |            |-C C10 AN10=C 0 AN10=C 0 A00=C 0 0=1
            |-C C1q AN1q-|
                         |-C C11 AN11=C 1 AN11=C 1 A01=C 1 1=1.

Now, to write out a deduction, we can basically move left to right here. From 1, we'll deduce C11. Then from C11 we'll deduce C 1 A10. Then C 1 AN00. Then C C00 AN00. Once we get C C01 AN01, then since we have C C00 AN00, we can get C C0q AN0q. But, I'll skip some steps here which gives us a simpler proof. Here goes:
1 1.
2 C δ1 δC00.
3 C δ1 δC01.
4 C δ0 δC10.
5 C δ1 δC11.
6 C δ0 δA00.
7 C δ1 δA01.
8 C δ1 δA10.
9 C δ1 δA11.
10 C δ1 δN0.
11 C δ0 δN1.
12 C Cpq C Cqp Epq.
13 C δ0 C δ1 δp. (this is not an axiom or theorem in intuitionistic logic).

2 δ/' * C1-14

14 C00.

3 δ/' * C1-15

15 C01.

13 δ/C0' * C14-C15-16

16 C0p.

5 δ/' * C1-17

17 C11.

13 δ/C'1 * C15-C17-18

18 Cp1.

18 p/C00 * 19

19 C C00 1.

8 δ/C C00 ' * C19-20

20 C C00 A10.

10 δ/C C00 A'0 * 20-21

21 C C00 AN00.

18 p/C01 * 22

22 C C01 1.

9 δ/CC01' * C22-23

23 C C01 A11.

10 δ/C C01 A'1 * C23-24

24 C C01 AN01.

13 δ/ C C0' AN0', p/q * C21-C24-25 

25 C C0q AN0q.

16 p/AN10 * 26

26 C 0 AN10.

4 δ/C ' AN10 * C26-27

27 C C10 AN10.

18 p/C11 * 28

28 C C11 1.

7 δ/C C11 ' * C28-29

29 C C11 A01.

11 δ/C C11 A'1 * C29-30

30 C C11 AN11.

13 δ/C C1' AN1', p/q *C27-C30-31

31 C C1q AN1q.

14 δ/C C'q AN'q * C25-C31-32

32 C Cpq ANpq.

18 p/AN00 * 33

33 C AN00 1.

2 δ/C AN00 ' * C33-34

34 C AN00 C00.

18 p/AN01 * 35

35 C AN01 1.

3 δ/C AN01 ' * C35-36

36 C AN01 C01.

13 δ /C AN0' C0', p/q * C34-C36-37

37 C AN0q C0q.

6 δ/C'0 * C14-38

38 C A00 0.

11 δ/C A'0 0 * C38-39

39 C AN10 0.

4 δ/C AN10 ' * C39-40

40 C AN10 C10.

18 p/AN11 * 41

41 C AN11 1.

5 δ/C AN11 ' * C41-42

42 C AN11 C11.

13 δ/C AN1' C1', p/q * C40-C42-43

43 C AN1q C1q.

37 δ/C AN'q C'q * C37-C43-44

44 C ANpq Cpq.

 12 p/Cpq, q/ANpq * C32-C44-45

45 E Cpq ANpq.

I looked over Arthur Prior's formal logic tonight.  Let V indicate a functioral variable of one argument.  Prior's book indicates that from the following all 2-valued propositions can get derived.  Actually, 2-5 in the following can get derived form 6. under substitution for V, substitution for variables, and detachment.

1. 1

2. C V 1 C V C00.

3. C V 1 C V C11.

4. C V 0 C V C10.

5. C V 1 C V C01.

6. C V 1 C V 0 V p.

I read about definitions getting expressed via a functioral variable " V " in two-valued logic last year and realized that definitions could get expressed in n-valued or infinite-valued logic via " V ".  For example, we could express the definition of alternation (disjunction) in three-valued logic as follows:

Definition of Alternation: C V Apq V CCpqq.

I wondered if there existed a way to axiomatize a multi-valued logic via a protothetical axiom set such as the one given above by Prior.  Since truth tables work for every single finite-valued logic, it turns out that every single finite-valued logic has a protothetical axiom scheme.  Note that axiom 6 encompasses all truth values of two-valued logic.

For example of a prothetical axiom set of a multi-valued logic, three-valued Lukasiewicz logic has the following table for C and N:

C  0  1  2  N
0   2  2  2  2
1   1  2  2  1
2* 0  1  2  0

Thus, a protothetical axiom set for Lukasiewicz 3-valued logic is the following (compare the last axiom with axiom 6. of the above).

1. 1

2. C V 2 C V C00.

3. C V 2 C V C01.

4. C V 2 C V C02.

5. C V 2 C V N0.

6. C V 1 C V C10.

7. C V 2 C V C11.

8. C V 2 C V C12.

9. C V 1 C V N1.

10. C V 0 C V C20.

11. C V 1 C V C21.

12. C V 2 C V C22.

13. C V 0 C V N0.

14. C V 2 C V 1 C V 0 V p.

I tried to post the following as a question (with previous edits) on the logic section of Mathoverflow.  They've put it on hold as unclear as to what I'm asking.  Is Mathoverflow even open to such a question, which has stood as open for a long time, getting asked in the first place? 

Title:

What is the Shortest Axiom of Classical Conditional-Negation Propositional Calculus?

Suppose that we only have propositional variables and connectives. Suppose our rules of inference are detachment {Cαβ, α} ⊢ β, and uniform substitution. Suppose that we have a binary connective "C" and a unary connective "N". In 1953 C. A. Meredith found what is currently the shortest single axiom of classical C-N (Conditional-Negation) propositional calculus [p. 302 of A. N. Prior's Formal Logic indicates this and references Prior's paper " 'Single Axioms for the Systems (C, N), (C, O), and (A, N) of the Two-valued Propositional Calculus' JCS, vol. i, No. 3 (July 1953), pp. 155-64. Systems 1.5, 3.13, 6.13, 6.14.):

CCCCCpqCNrNsrtCCtpCsp.

Or using another prefix notation

→→→→→pq→¬r¬srt→→tp→sp.

So given the first notation, the formation rules are:

1. All lower case letters of the Latin alphabet, as well as any lower case letters of the Latin alphabet sub-scripted by Hindu-Arabic numerals are formulas.
2. If x is a formula, then so is Nx.
3. If x and y are formulas, then so is Cxy.
4. Nothing else is a formula in this context.

To determine what is and what is not a formula the following suffices.

1. Assign -1 to all lower case letters, as well as all lower case letters which are sub-scripted.
2. Assign 0 to N.
3. Assign 1 to C.
4. Sum the assigned numbers as you precede from left to right throughout any given string.
5. A string will qualify as a formula if and only if it either starts and ends with -1, or if it starts with a member of {0, 1} and -1 is only reached at the spot corresponding to the last letter of the string, and that string ends with -1.

Now, via the above it turns out that any formula that starts with "C", has its antecedents corresponding to the longest subformulas which have a "0" corresponding to their last letter. So looking at the above formula, we have

C  C  C  C  C  p  q  C  N  r  N  s  r  t  C  C  t  p  C  s  p
|  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |  |
1  2  3  4  5  4  3  4  4  3  3  2  1  0  1  2  1  0  1  0 -1

The longest subformula which ends with the first "t" is thus CCCCpqCNrNsrt. The longest subformula which ends with the second "p" is thus "Ctp", and "s" is the longest subformula corresponding to the third "0" spot. Thus, the main breaks of the formula can get located by the following "|" marks.

C|CCCCpqCNrNsrt|C|Ctp|C|s|p.

Furthermore, the main breaks of CCCCpqCNrNsrt is given by C|CCCpqCNrNsr|t, and so on.
Suppose we have a 2-valued model of C and N given by the following table:

C  0  1  N
0  1  1  1
1  0  1  0

Does there exist any shorter single axiom, which under the rules above allows us to deduce all tautologies, and only those tautologies in the 2-valued model? Does there exist another single axiom of the same length?
If there exists a unique shortest axiom up to re-symbolization of variables and connectives, what is the shortest axiom which allows us to deduce a known axiom system for classical propositional calculus, such as the following axiom set?

1. CpCqp. [p→(q→p)].
2. CCpCqrCCpqCpr. [(p→(q→r))→((p→q)→(p→r))].
3. CCNpNqCqp. [(¬p→¬q)→(q→p)].

If there exists more than one shortest axiom, what is the set of shortest axioms up to re-symbolization of variables and connectives?

The length of an axiom is defined by the number of symbols it has when fully expressed as a well-formed formula.

I started looking at the following a few days after I read J. A. Kalman's paper on condensed detachment where he uses condensed detachment on non-tautologous formulas.

In some logical systems we can obtain a propositional variable as a theorem.  For instance, if our axiom is CpCqr, then we have the following:

axiom 1 CpCqr.
D1.1   2 Cpq.
D2.2   3 p.

Since p could mean the constant false proposition "0" this means such a system can prove a false proposition.  Most logical systems I've seen can only prove tautologies for some semantics.  It turns out there exist logical systems which have non-tautologous formula, but also can't prove a propositional variable.  Here's one:

axiom 1 CCCpqqp
D1.1   2 Cpp

It turns out that if our only inference rule is condensed detachment, and CCCpqqp is our only axiom, the entire system of theorems is {CCCpqqp, Cpp}.  From Kalman's theorem that everything deducible from substitution and detachment is a substitution of a formula deducible by condensed detachment and conversely, it follows that you can't deduce a falsity just from substitution in this system.

That said, if you were to say join CCCpqqp to a system for classical logic like Lukasiewicz's preferred axiom set, then you could deduce a variable.

axiom 1 CCpqCCqrCpr
axiom 2 CpCNpq
axiom 3 CCNppp
axiom 4 CCCpqqp
D4.3   5 Np
D2.5   6 CNNpq
D6.5   7 p

There's a correspondence between the use of derivable rules of inference and the notation used for condensed detachment.  Let's say our axioms are

1 CCpqCCqrCpr
2 CpCNpq
3 CCNppp

and we have condensed detachment {Cab, a'} |-b' as our rule of inference.  We can write a proof of Cpp as follows:

D1.2  4 CCCNpqrCpr
D4.3  5 Cpp

We could also write:

D1.2       4 CCNpqrCpr
DD1.2.3 5 Cpp

From axiom 1 and having condensed detachment as our rule of inference, we have
{Cab, Cb'c} |- Ca'c' as a rule of inference.  In effect {Cab, Cb'c} |- Ca'c' with "x" as "Cab" and "y" as "Cb'c" produces the same formula as DD1.x.y.  And in general it seems that if a derivable rule of inference comes as derivable just from one formula "f" by the rule generation schema "from |-Cab, we may infer a|-b" that the use of the derivable rule of inference on formulas a, ..., e corresponds to
D...Dfa...e where the number of "D's" equals the number of formulas in the sequence a, ..., e.  For example, if we substituted r/CsCtCCCuvwx in CCpqCCqrCpr we would then have

9 CCpqCCqCsCtCCCuvwxCpCsCtCCCuvwx.  For formulas i1,..., in, formula 9 has derivable rules of inference corresponding to:

DD9.i1.i2  {Cab, Cb'CcCdCCCefgh} |- Ca'Cc'Cd'CCCe'f'g'h'

DDD9.i1.i2.i3 {Cab, Cb'CcCdCCCefgh, a'} |- Cc'Cd'CCCe'f'g'h'

DDDD9.i1.i2.i3.i4 {Cab, Cb'CcCdCCCefgh, a', c'} |- Cd'CCCe'f'g'h'

DDDDD9.i1.i2.i3.i4.i5 {Cab, Cb'CcCdCCCefgh, a', c', d'} |- CCCe'f'g'h'

DDDDDD9.i1.i2.i3.i4.i5.i5 {Cab, Cb'CcCdCCCefgh, a', c', d', CCe'f'g'} |-h'

Consider the following proof of CCpCqrCCsqCpCsr.

axiom             1 CCpqCCqrCCpr
DD1.1.D1.1   2 CCpCqrCCsqCpCsr

We can thus, in effect, work through this proof in different ways.  We could proceed as thus

axiom    1 CCpqCCqrCpr
D1.1      2 CCCCqrCprsCCpqs
D2.2      3 CCpCqrCCsqCpCsr

We could also though proceed by computing D1.1, and thus using the derivable rule of inference {Cab, Cb'c} |- Ca'c', computing DD1.1D1.1.

          CCab   C C   b       c  C a c
                       |   |    |        |   ------
                       |   |   ----   ----   |
                   C C C Cqr   Cpr  s  CCpqs  
           
Thus, b/Cqr, c/Cpr, and s/Cac which turns into b/Cqr, c/Cpr, s/CaCpr.  This proof is simpler than computing D2.2.

         C CCC a      b    Ccb   d     CCcad
                      |       |     ----    |
                     ----  ---     |   --------
            CCC Cqr Cpr   s   CCpqs

Here the diagram suggests a/Cqr, b/Cpr, s/Ccb, d/CCpqs, which turns into a/Cqr, b/Cpr, s/CcCpr, d/CCpqCcCpr.  The substitutions here end up more complex than when using the derivable rule of inference.

I wrote about a way to generate more bases for classical logic about a year ago, when you have either CCpqCCqrCpr or CpCqp upfront in the basis.  Examples of such systems are {CCpqCCqrCpr, CCNppp, CpCNpq}-Lukasiewicz, {CCpqCCqrCpr, CCpCpqCpq, CpCqp, CCNpNqCqp}-Tarski, {CpCqp, CCpCqrCCpqCpr, CCNpqCCNpNqp}-I don't think think I've seen this before, but it's basically implied by a system of Mendelsohn since if any system has [C] CCpCqrCqCpr provable in a proper sub-basis without axioms a, ..., z, of the basis, then a can get replaced by D[C].a, b can get replaced by D[C].b, ... z can get replaced by D[C].z.  For example, for the basis {CCpCqrCCpqCpr, CpCqp, CCNpNqCqp}, [C] can get proved in the sub-basis {CpCqp, CCpCqrCCpqCpr}.  Thus, CCNpNqCqp can get replaced by CpCCNqNpq for the basis {CCpCqrCCpqCpr, CpCqp, CCNpNqCqp}.

The following 4-basis for C-N classical logic is independent:

1. CCCCpqCrqsCCrps
2. CCpqCCNppq
3. CCCNpqrCpr
4. Cpp

Or as a system with fewer symbols, the axioms of the following are independent.

1. CCpqCCqrCpr
2. CCpqCCNppq
3. CpCNpq
4. Cpp

Does there exist a shorter 4-basis with independent axioms for C-N classical logic?

I note also that the following four formulas are not independent

1. CCpqCCqrCpr
2. CCNppp
3. CCCNpqrCpr
4. Cpp

since D3.2 yields Cpp.

Does there exist a 3-basis or a 2-basis for classical logic where one of the axioms is Cpp?

I ran Prover9 [1] with the following inputs:

1.

-P(i(x, y)) | -P(x) | P(y).
P(i(x,i(y,x))). %RVP
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). %SD

2.

-P(i(x, y)) | -P(x) | P(y).
-P(i(x, y)) | -P(i(y, z)) | P(i(x, z)).
P(i(x,i(y,x))). %RVP
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))). %SD

-P(i(x, y)) | -P(i(y, z)) | P(i(x, z)) represents a derivable rule in the first system.  I had the formula P(i(i(x, y), i(i(y, z), i(i(z, u), i(x, u))))) as the goal.  The proof in the 1st system took 7.56 seconds, had 958 givens, generated 835656 formulas, and 23398 formulas kept.  The proof in the 2nd system took 25.72 seconds, had 1450 givens, generated 3835597 formulas, and kept 26067 formulas.  Both proofs took the same number of steps.  The maximum clause weight of the second proof was lower than that of the first proof.  As I understand things, this means that the longest formula of the second proof (excluding parentheses and predicate symbols) was shorter than that of the first proof.  Here's the first proof:

% -------- Comments from original proof --------
% Proof 1 at 7.56 (+ 0.41) seconds.
% Length of proof is 21.
% Level of proof is 10.
% Maximum clause weight is 24.
% Given clauses 958.

1 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))) # label(non_clause) # label(goal).  [goal].
2 -P(i(x,y)) | -P(x) | P(y).  [assumption].
3 P(i(x,i(y,x))).  [assumption].
4 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).  [assumption].
5 -P(i(i(c1,c2),i(i(c2,c3),i(i(c3,c4),i(c1,c4))))).  [deny(1)].
6 P(i(x,i(y,i(z,y)))).  [hyper(2,a,3,a,b,3,a)].
7 P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))).  [hyper(2,a,4,a,b,4,a)].
8 P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))).  [hyper(2,a,3,a,b,4,a)].
11 P(i(x,i(y,i(z,i(u,z))))).  [hyper(2,a,3,a,b,6,a)].
23 P(i(i(x,i(i(y,x),z)),i(x,z))).  [hyper(2,a,7,a,b,6,a)].
39 P(i(i(x,i(i(y,i(z,y)),u)),i(x,u))).  [hyper(2,a,7,a,b,11,a)].
43 P(i(i(i(x,i(y,z)),i(i(i(x,y),i(x,z)),u)),i(i(x,i(y,z)),u))).  [hyper(2,a,7,a,b,8,a)].
126 P(i(i(x,y),i(i(z,x),i(z,y)))).  [hyper(2,a,23,a,b,8,a)].
419 P(i(i(i(x,y),z),i(y,z))).  [hyper(2,a,39,a,b,126,a)].
441 P(i(x,i(i(i(y,z),u),i(z,u)))).  [hyper(2,a,3,a,b,419,a)].
876 P(i(i(x,i(y,z)),i(y,i(x,z)))).  [hyper(2,a,43,a,b,441,a)].
1406 P(i(i(x,y),i(i(y,z),i(x,z)))).  [hyper(2,a,876,a,b,126,a)].
2202 P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).  [hyper(2,a,1406,a,b,1406,a)].
2220 P(i(i(x,i(y,z)),i(x,i(i(z,u),i(y,u))))).  [hyper(2,a,126,a,b,1406,a)].
23399 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))).  [hyper(2,a,2202,a,b,2220,a)].
23400 $F.  [resolve(23399,a,5,a)].


Here's the second proof:

% -------- Comments from original proof --------
% Proof 1 at 25.72 (+ 1.89) seconds.
% Length of proof is 21.
% Level of proof is 10.
% Maximum clause weight is 16.
% Given clauses 1450.

1 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))) # label(non_clause) # label(goal).  [goal].
2 -P(i(x,y)) | -P(x) | P(y).  [assumption].
3 -P(i(x,y)) | -P(i(y,z)) | P(i(x,z)).  [assumption].
4 P(i(x,i(y,x))).  [assumption].
5 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).  [assumption].
6 -P(i(i(c1,c2),i(i(c2,c3),i(i(c3,c4),i(c1,c4))))).  [deny(1)].
8 P(i(x,i(y,i(z,y)))).  [hyper(2,a,4,a,b,4,a)].
10 P(i(i(x,y),i(i(z,x),i(z,y)))).  [hyper(3,a,4,a,b,5,a)].
14 P(i(i(x,y),i(x,x))).  [hyper(2,a,5,a,b,4,a)].
31 P(i(x,x)).  [hyper(2,a,14,a,b,8,a)].
33 P(i(i(i(x,y),x),i(i(x,y),y))).  [hyper(2,a,5,a,b,31,a)].
146 P(i(x,i(i(x,y),y))).  [hyper(3,a,4,a,b,33,a)].
166 P(i(i(i(x,i(y,x)),z),z)).  [hyper(2,a,33,a,b,8,a)].
190 P(i(i(x,y),i(x,i(i(y,z),z)))).  [hyper(2,a,10,a,b,146,a)].
344 P(i(i(i(x,y),z),i(y,z))).  [hyper(3,a,10,a,b,166,a)].
601 P(i(i(x,i(y,z)),i(y,i(x,z)))).  [hyper(3,a,5,a,b,344,a)].
3542 P(i(i(x,y),i(i(y,z),i(x,z)))).  [hyper(3,a,190,a,b,601,a)].
5634 P(i(i(x,y),i(i(z,i(y,u)),i(z,i(x,u))))).  [hyper(3,a,3542,a,b,10,a)].
5639 P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).  [hyper(2,a,3542,a,b,3542,a)].
26068 P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))).  [hyper(3,a,5634,a,b,5639,a)].
26069 $F.  [resolve(26068,a,6,a)].

The above may make it look like derived rules aren't of use.  But I ran another trial looking for proofs of  P(i(i(x, i(y, z)), i(y, i(x, z)))).  For the first system I got the following proof:

% Proof 1 at 0.05 (+ 0.03) seconds.
% Length of proof is 17.
% Level of proof is 7.
% Maximum clause weight is 24.
% Given clauses 75.

1 P(i(i(x,i(y,z)),i(y,i(x,z)))) # label(non_clause) # label(goal).  [goal].
2 -P(i(x,y)) | -P(x) | P(y).  [assumption].
3 P(i(x,i(y,x))).  [assumption].
4 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).  [assumption].
5 -P(i(i(c1,i(c2,c3)),i(c2,i(c1,c3)))).  [deny(1)].
6 P(i(x,i(y,i(z,y)))).  [hyper(2,a,3,a,b,3,a)].
7 P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))).  [hyper(2,a,4,a,b,4,a)].
8 P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))).  [hyper(2,a,3,a,b,4,a)].
11 P(i(x,i(y,i(z,i(u,z))))).  [hyper(2,a,3,a,b,6,a)].
23 P(i(i(x,i(i(y,x),z)),i(x,z))).  [hyper(2,a,7,a,b,6,a)].
39 P(i(i(x,i(i(y,i(z,y)),u)),i(x,u))).  [hyper(2,a,7,a,b,11,a)].
43 P(i(i(i(x,i(y,z)),i(i(i(x,y),i(x,z)),u)),i(i(x,i(y,z)),u))).  [hyper(2,a,7,a,b,8,a)].
126 P(i(i(x,y),i(i(z,x),i(z,y)))).  [hyper(2,a,23,a,b,8,a)].
419 P(i(i(i(x,y),z),i(y,z))).  [hyper(2,a,39,a,b,126,a)].
441 P(i(x,i(i(i(y,z),u),i(z,u)))).  [hyper(2,a,3,a,b,419,a)].
876 P(i(i(x,i(y,z)),i(y,i(x,z)))).  [hyper(2,a,43,a,b,441,a)].
877 $F.  [resolve(876,a,5,a)].

For the second system I got the following proof:

% -------- Comments from original proof --------
% Proof 1 at 0.03 (+ 0.01) seconds.
% Length of proof is 15.
% Level of proof is 7.
% Maximum clause weight is 14.
% Given clauses 38.

1 P(i(i(x,i(y,z)),i(y,i(x,z)))) # label(non_clause) # label(goal).  [goal].
2 -P(i(x,y)) | -P(x) | P(y).  [assumption].
3 -P(i(x,y)) | -P(i(y,z)) | P(i(x,z)).  [assumption].
4 P(i(x,i(y,x))).  [assumption].
5 P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).  [assumption].
6 -P(i(i(c1,i(c2,c3)),i(c2,i(c1,c3)))).  [deny(1)].
8 P(i(x,i(y,i(z,y)))).  [hyper(2,a,4,a,b,4,a)].
10 P(i(i(x,y),i(i(z,x),i(z,y)))).  [hyper(3,a,4,a,b,5,a)].
14 P(i(i(x,y),i(x,x))).  [hyper(2,a,5,a,b,4,a)].
31 P(i(x,x)).  [hyper(2,a,14,a,b,8,a)].
33 P(i(i(i(x,y),x),i(i(x,y),y))).  [hyper(2,a,5,a,b,31,a)].
166 P(i(i(i(x,i(y,x)),z),z)).  [hyper(2,a,33,a,b,8,a)].
344 P(i(i(i(x,y),z),i(y,z))).  [hyper(3,a,10,a,b,166,a)].
601 P(i(i(x,i(y,z)),i(y,i(x,z)))).  [hyper(3,a,5,a,b,344,a)].
602 $F.  [resolve(601,a,6,a)].

Since the second proof here took some 602 formulas in comparison to 877 formulas of the first proof, the second proof has length of 15 in comparison to length 17 of the first proof, the clause weight is 14 in comparison to 24, the given clauses is 38 in comparison to 75, and it took slightly less time this suggest that *sometimes* using derived rules might make it easier for Prover9 to find a proof.

[1] W. McCune, "Prover9 and Mace4", http://www.cs.unm.edu/~mccune/Prover9, 2005-2010.

Professor Ulrich asks "Can a fully-automated proof of the sufficiency of Meredith's 21-character single axiom,  CCCCCpqCNrNsrtCCtpCsp / ((((p⊃q)⊃(~r⊃~s))⊃r)⊃t)⊃((t⊃p)⊃(s⊃p)), for classical logic in C and N be found that equals (or shortens) Meredith's own derivation of Syl = CCpqCCqrCpr / ((p⊃q)⊃((q⊃r)⊃(p⊃r)), Scotus = CpCNpq / p⊃(~p⊃q),  and Clavius = CCNppp / (~p⊃p)⊃p using just 41 condensed detachments? 
UPDATE: Larry Wos has (with OTTER) now discovered a proof using only 38 applications of condensed detachment.  See Automated reasoning and the discovery of missing and elegant proofs, L. Wos and G. Peiper, Rinton, Paramus, 2003, sections 3.1 through 3.3."

The question seems local to the derivation of {CCpqCCqrCpr, CpCNpq, CCNppp}.  One might ask "Can a fully-automated proof of the sufficiency of Meredith's 21-character single axiom,  CCCCCpqCNrNsrtCCtpCsp / ((((p⊃q)⊃(~r⊃~s))⊃r)⊃t)⊃((t⊃p)⊃(s⊃p)), for classical logic in C and N be found that requires less than 38 condensed detachments to get to the axioms for any distinct basis of C-N classical logic?"

It takes no more than 5 condensed detachments to get to CpCqp.