Formula of the Day: Recursive Variable Prefixing CpCqp.

When proving that a logical system has a deduction metatheorem, CpCqp proves indispensable.   In fact, CpCqp along with CCpCqrCCpqCpr or CCpqCCpCqrCpr suffices to prove a deduction metatheorem.  Let's consider the system {CpCqp}.  For this system:

Lemma: Every theorem obtainable by condensed detachment for the system {CpCqp} has the form C0C1...CnCpCqp.

Demonstration: The first theorem obtainable by condensed detachment is CpCqCrq.  Now from {CpCqp, CpCqCrq} we can use either thesis as the minor premise, and either one as the major.  If CpCqp is the major, then we will detach Cab where "a" is a variable and "b" consists of the minor premise.  If CpCqCrq is the major premise, then we will obtain CpCqp.  More generally, if we have CpCqp as the major premise and use any theorem "b" as the minor premise, we will obtain Cab upon a condensed detachment.  If Cat, where "a" does not appear in "t" gets used as the major premise, then we will obtain "t" after a condensed detachment.  Thus, any time we use condensed detachment in this system we'll either obtain CpCqp or some theorem which has CpCqp as its last 5 letters.

The above lemma can get argued also via mathematical induction.

Corollary: Every thesis (theorem or axiom) obtainable via condensed detachment for the system {CpCqp} can serve as a sole axiom for a system with the same theses as {CpCqp}.

Demonstration: Since every axiom has form C0C1...CnCpCqp by the above lemma, we can obtain CpCqp as a theorem of the system.  Since CpCqp has C0C1...CnCpCqp as a theorem, it follows that the systems have the exact same theorems.

Consequently it follows that in addition to {CpCqp, CCpCqrCCpqCpr} sufficing to prove the deduction theorem *any* theorem obtainable from the system {CpCqp} solely by condensed detachment can take the place of CpCqp in {CpCqp, CCpCqrCCpqCpr} .