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.
