Do Hypothetical Syllogism and Contraction Come as Sufficient for Self-Distribution?

Question

If we have the following axioms (under detachment)

 1. CCpqCCqrCpr-hypothetical syllogism
 2. CCpCpqCpq-contraction
 3. CpCqp-recursive variable prefixing

Then we can deduce

 4. CCpCqrCCpqCpr-distribution

3. and 4. suffice for The Deduction Metatheorem. I've run the prover Prover9 and the model checker Mace 4 for some 3600 seconds to try and see if 1. and 2. would suffice for distribution or not, but come up with nothing. I suspect that you can't prove distribution from {hypothetical syllogism, contraction}, but if so, what would model satisfies 1. and 2., but not 4.? If not, how do we prove distribution from {hypothetical syllogism, contraction}?

Answer 1

I think (I do remember that my program could prove it)

you can proof self- distribution ( CCpCqrCCpqCpr) from

• one of prefixing (CCpqCCrpCrq) and suffixing (CCpqCCqrCpr)
• one of permutation(CCpCqrCqCpr) and assertion (CpCCpqq) and
• contraction ( CCpCpqCpq )

maybe you also need self implication ( Cpp ) but I doubt that

so in your case i think you need to add permutation(CCpCqrCqCpr) or assertion (CpCCpqq) let me know what happens if you add one of these two. if needed also add Cpp

good luck