How do I Prove the Theorems Needed for "The Deduction Meta-Theorem" from CδCpqCpδq? I use Polish notation.  δ stands for a variable function (or functor) of one argument.
A section of Lukasiewicz's book on Aristotle's syllogistic from the modern point of view reads:
"I should like to emphasize that the system based on axiom 51 [CδpCδNpδq] is much richer than the C-N-p-system.  Among asserted consequences containing δ there are such logical law as CCpqCCqpCδpδq, CδCpqCδpδq, CδCpqCpδq, all very important, but unknown to almost all logicians.  The first law [CCpqCCqpCδpδq], for instance, is the principle of extensionality, being equivalent to CQpqCδpδq [Lukasiewicz used Q here the same as he used E in other places], the second may be taken as the sole axiom of the so-called 'implicational' system [CδCpqCδpδq], the third [CδCpqCpδq] as an axiom of the so-called 'positive' logic."
I want to prove the second and third claims.  This question focuses on proving the third claim.  First, I'll try and explain how substitution for δ works.
The rule of uniform substitution includes substitution for δ. To know when you can use a substitution for δ  you can do the following:
1.Assign -1 to the apostrophe symbol '
2.Assign -1 to all lower case letters of the Latin alphabet (or numerically subscripted lower case letters of the Latin alphabet).
3.Assign 1 to all binary connectives.
4.Assign 0 to all unary connectives, including δ.
A uniform substitution for δ  comes as permissible if and only if, it contains at least one apostrophe (or equivalent symbol if you don't like the use of an apostrophe), when you start with 0 before doing any sums and form sums from left to right using the above assignments such a summation process never reaches -2, and such a summation process ends with -1. You could also suppose a "1" in the blank space to the left of the well-formed formula, and consequently, such a summation process will end with 0 and never correspond at any point to -1 if it comes as a permissible substitution.
The third claim made in the above passage implies that from 
CδCpqCpδq. as an axiom using just substitution and detachment {$\vdash$C$\alpha$$\beta$, $\vdash$$\alpha$} -> $\vdash$$\beta$ we can deduce the following two well-formed formulas.
Goal 1 CpCqp.  Recursive Letter Prefixing.
Goal 2 CCpCqrCCpqCpr.  Self-Distribution.
How can we prove this claim?
Thoughts and some of what I have so far (I more theorems, I don't find it too hard to get more, but I don't believe that just getting more theorems will work here):
Hypothesis: It might help to at least prove at least some other well-known theorems of the positive implicational calculus or "deduction logic" such as:
 Contraction   1 CCpCpqCpq.

 Expansion     2 CCpqCpCpq.

 C-suffixing   3 CCpqCCqrCpr.  Or Hypothetical Syllogism.

 C-prefixing   4 CCqrCCpqCpr.  Or Reverse Hypothetical Syllogism.

 Commutation   5 CCpCqrCqCpr.

 GHS           6 CCpCqrCCrsCpCqs.  Or Generalizable Hypothetical Syllogism.

 Interpolation 7 CCpqCpCrq.

 Mid replace   8 CCpCqrCCsqCpCsr.

 Syll-Simp     9 CCCpqrCqr.

 Assertion    10 CpCCpqq.

I have the following.  The "/" stands for a substitution to get made.  * functions as a separator.  C x -y indicates that we have $\vdash$*x*, and we have $\vdash$C x - y, and thus we will detach y.  Substitutions happen simultaneously in the following proofs.
1 CδCpqCpδq.
1 δ/Cr' * 2

2 CCrCpqCpCrq (up to relettering this is commutation)
1 δ/' * 3

3 CCpqCpq
2 r/Cpq * C3-4

4 CpCCpqq.  (this is assertion).
1 δ/C'' * 5

5 CCCpqCpqCpCqq.
5 * C3-6

6 CpCqq.  
2 r/p, p/q * C6-7

7 CqCpq.  (this is recursive letter prefixing, which also gives us expansion via substitution.)
6 p/CpCqq, q/p * C6-8

8 Cpp.
If we can prove some lemmas, then we can get to CCpCqrCCpqCpr in several ways.  For example:
1 δ/CC'CrsCCqrCqs * 9

9 C CC Cpq CrsCCqrCqs C p CCqCrsCCqrCqs.
Now the antecedent is CCCpqCrsCCqrCqs, which has CCpqCrs, Cqr, and q as its "antecedents" in some sense.  If q, since we have CqCpq, then Cpq.  Since we have CCpqCrs and Cpq, Crs follows.  Since we have q and Cqr, we can get r.  Since we have r and Crs, we can then get s.  Thus, if the claim made holds, we could deduce CCCpqCrsCCqrCqs.  Then we can detach CpCCqCrsCCqrCqs.  Then we substitute p/Cpp in that wff (or any theorem that we already have), and we can then detach CCqCrsCCqrCqs.  Or
1 δ/CCrC'sCCrqCrs*10

10 C CCrCCpqsCCrqCrs Cp CCrCqsCCrqCrs.
If CrCCpqs, Crq, and r hold, then we have q, as well as CCpqs by detachment.  Since we have CqCpq when we have The Deduction Theorem, we can then detach Cpq.  Then we can detach s.  So, CCrCCpqsCCrqCrs does hold in the positive implicational calculus, and we have another possible lemma, which if we can prove here, we can get to self-distribution.  Or if we wanted to prove CCpqCCqrCpr we might try the following:
 1 δ/CCr'CC'sCrs * 11

11 C CCrCpqCCCpqsCrs C p CCrqCCqsCrs.
The length of the lemmas suggests to me that proving these lemmas won't really help, but I can't really tell, especially since I found it easier to first prove CCpqCpq before proving Cpp, so would I do better to ignore the length of the lemmas?
If I understand things correctly, we should also have the ability to prove CδCpCqrδCqCpr as well as CδCpCpqδCpq in this calculus.  The first should enable us to move any of the multiple antecedents around via some substitution and detachment, and the second would allow us to "expand" and "contract" fairly easily.
Other ideas on how we might prove CCpCqrCCpqCpr?
Do there exist any theorem provers out there which might help with this sort of problem?
 A: In the Journal of Symbolic Logic Volume 31, Number 1, March 1966 there's a paper by Carew Arthur Meredith called Postulates for Implicational Calculi which contains a proof.  Using that proof (and some of what I had already figured out above) and condensed detachment I write the following:
axiom      1 CδCpqCpδq
1 δ/'      2 CCpqCpq
1 δ/C''    3 CCCpqCpqCpCqq
D3.2       4 CpCqq
1 δ/Cr'    5 CCrCpqCpCrq
D5.4       6 CpCqp* Recursive Letter Prefixing
1 δ/CC'rr  7 CCCCpqrrCpCCqrr
D5.2       8 CpCCpqq  Assertion
D8.8       9 CCCpCCpqqrr
D7.9      10 CpCCCCpqqrr
D5.10     11 CCCCpqqrCpr
D11.7     12 CCpqCpCCqrr
D12.12    13 CCpqCCCpCCqrrss
D5.13     14 CCCpCCqrrsCCpqs
D14.5     15 CCpqCCqrCpr* C-suffixing
1 δ/CC'r' 16 CCCCpqrCpqCpCCqrq
D15.15    17 CCCCqrCprsCCpqs
D17.16    18 CCpCpqCpCCqqq
D5.5      19 CpCCrCpqCrq
D4.4      20 Cpp
D19.20    21 CCpCCqqrCpr
D15.18    22 CCCpCCqqqrCCpCpqr
D22.21    23 CCpCpqCpq* Contraction

Meredith starred 6, 15, and 23 implying {6, 15, 23} sufficient to deduce CCpCqrCCpqCpr.  Using what I've gotten from a version of the program Prover9 that Rob Arthan has referenced, I'll continue the proof as follows:
D5.15     24 CCpqCCrpCrq
D24.23    25 CCpCqCqrCpCqr
D17.25    26 CCpqCCqCprCpr
D5.26     27 CCpCqrCCqpCqr
D17.27    28 CCpqCCpCqrCpr
D5.28     29 CCpCqrCCpqCpr

The upshot here comes as that you can prove that the deduction metatheorem holds for this system.  Since this system has variable functions, if I've gotten things correct here, this means we have corollaries of the deduction metatheorem in the following three statements:


*

*If {$\gamma$, $\delta$p} $\vdash$ $\delta$q, then $\gamma$ $\vdash$ C$\delta$p$\delta$q.

*If {$\gamma$, p} $\vdash$ $\delta$q then $\gamma$ $\vdash$ Cp$\delta$q

*If {$\gamma$, $\delta$p} $\vdash$ q, then $\gamma$ $\vdash$ C$\delta$pq.
Consider the antecedent of the parse tree of 5 and it can change as follows:
      C
     / \
    r*  C
       / \
      p   q

changes to
        C
     /    \
    C      C
   / \    / \
  p   q  p   q

Here the original meaningful expression CCpqCpq just had a new branch which just qualifies as a sub-branch of the original tree.
The substitution of δ in 1 with ' though changes from
             C
           /   \
          δ     C
          |    / \
          C   p   δ
         / \      |
        p   q     q

to:
              C
            /  \
           C   C
          / \ / \
         p  q p  q

Here, nodes just disappear from the tree.
Substituting δ with C'' in 1 yields
             C
            / \
           C      C
          / \    / \
         C   C   p  C
        / \ / \    / \
       p  q p q    q q 

Here subtree of the main tree have changed in more ways than just a variable dropping and some subtree branching off from that spot.
