Logical Formula of the Day: self-distribution CCpCqrCCpqCpr.

Here's two links on condensed detachment.  If we have two formulas Cab, and "a", condensed detachment produces the most general formula "b".  For instance, if we have

1. CpCqp as "a" and
2. CCpCqrCCpqCpr as "Cab",

we could substitute "r" in CCpCqrCCpqCpr, and thus obtain CCpqCpp from a condensed detachment D2.1.  We could also substitute "r" with "Cqp", and "p" with "Cqp" in  CCpCqrCCpqCpr  with Cqp  obtaining CCCqpCqCqpCCCqppCCqpCqp, and then substitute "p" with "Cqp" in CpCqp obtaining CCqpCqCqp.  Thus, from 1. and 2. we could detach CCCqpqCCqpCqp as a theorem.  However, CCCqpqCCqpCqp is less general than CCpqCpp, since if we substitute "p" with "Cqp" in CCpqCpp, then we obtain CCCqpqCCqpCqp.  So, condensed detachment Da.b obtains a form from which you can obtain every other theorem detachable from a substitution instance of "a" as the major premise and "b" as the minor premise.

Let's look a little at the system {CCpCqrCCpqCpr}

axiom   1 CCpCqrCCpqCpr
D1.1     2 CCCpCqrCpqCCpCqrCpr
D1.2     3 CCCCpCqrCpqCpCqrCCCpCqrCpqCpr
D1.3     4 CCCCCpCqrCpqCpCqrCCpCqrCpqCCCCpCqrCpqCpCqrCpr

Every theorem of this system obtained via condensed detachment has three variables.  This follows, because the axiom has only three variables in the antecedent and the consequent.  Thus, the second theorem has only three variables in the antecedent and the consequent.

If we have CCpCqrCCpqCpr and CpCqp as axioms or theorems, then we have a deduction metatheorem for the system which says "if we have an assumption "a" which leads to a formula "b" under the scope of some set of assumptions "g", then Cab holds under the scope of the assumptions "g" also".  Or more concisely we can write:

Deduction Metatheorem: If {g, a} |- b, then {g}|-Cab.