0

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}?

Doug Spoonwood
  • 11,211

1 Answers1

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

Willemien
  • 6,582
  • Prefixing and assertion alone allow you to prove self-implication. – Doug Spoonwood Apr 23 '14 at 01:59
  • You don't need Cpp. Your assertion that {CCpqCCrpCrq, CCpCqrCqCpr, CCpCpqCpq}, {CCpqCCrpCrq, CpCCpqq, CCpCpqCpq}, {CCpqCCrpCrq, CCpCqrCqCpr, CCpCpqCpq} and {CCpqCCrpCrq, CpCCpqq, CCpCpqCpq} all have CCpCqrCCpqCpr as a theorem is correct. But, not all of them have Cpp as a theorem. – Doug Spoonwood Apr 23 '14 at 02:12