How Do I Prove the 6 Letter Thesis Cδδ0δp?

Question

There exists a 1951 paper by C. A. Meredith which proves a completeness meta-theorem for the "C, 0, δ, p" system which has as it's sole axiom Cδδ0δp under uniform substitution for propositional variables, uniform substitution for functorial variables [see here] or this part from A. N. Prior's Formal Logic, and detachment. There exists another system of the same type which has as it's axioms:

1. CδC00δ1
2. Cδ0Cδ1δp

I've read through a proof by Lukasiewicz which shows that from those two axioms follows:

3. CδC10δ0
4. CδC01δ1
5. CδC11δ1
6. 1

I know how to prove formulas like CδCpqCδpδq and CCpqCCqpCδpδq from the above 6 theses. And I can tell that if I can prove Cδδ0δ0 and Cδδ0δ1, I can prove Cδδ0δp. But, from the above 6 formulas, how can we prove something which has two δ's on one side and one δ on the other? How can we prove Cδδ0δ0 and Cδδ0δ1? Or can we prove Cδδ0δp without proving those two first?

Answer 1

I don't know why I wrote the above axioms when I didn't really care if they had the form CδCxyδz or CδzδCxy, but I suppose the forms I used might provide for a more instructive proof. Section 2. part I. of Meredith's paper gave me enough hints, along with some previous experience working with this sort of system, to construct a proof. As a special case of a more general metalogical statement in his paper indicates, if we prove CCCp0δ0CCpδC00δp, CCδ00Cδ0δp, and Cδ0CδC00δp we can prove Cδδ0δp in short order. Proving Cδ0CδC00δp can get proved from Cδ1δC00 and Cδ0Cδ1δp. CCδ00Cδ0δp consists of an instance of CCp0Cpq. How to prove CCCp0δ0CCpδC00δp can get seen from the cases CCC00δ0CC0δC00δ0 which reduces to CC1δ0CC0δC00δ0 which reduces to Cδ0CC0δC00δ0 an instance of CpCqp, and CCC10δ0CC1δC00δ1 which reduces to CCC10δ0CδC00δ1 which reduces to CCC10δ0Cδ1δ1 an instance of CpCqq. CδpδC1p will make for a useful lemma also.

1 1 
2 CδC00δ1
3 CδC01δ1
4 CδC10δ0
5 CδC11δ1
6 Cδ0Cδ1δp

First, we'll transform the axioms from having form CδCxyδz to form CδzδCxy. A useful, but strictly unnecessary (study steps 9 through 13 closely), lemma is Cpp.

    6 δ/CδC''δ1 * 7
7 CCδC00δ1CCδC11δ1CδCppδ1
    7 * C2-8
8 CCδC11δ1CδCppδ1
    8 * C5-9
9 CδCppδ1
    9 δ/Cδ'δCpp * 10
10 CCδCppδCppCδ1δCpp
    9 δ/CCδCppδ'Cδ1δCpp * 11
11 CCCδCppδCppCδ1δCppCCδCppδ1Cδ1δCpp
    11 * C10-12
12 CCδCppδ1Cδ1δCpp
    12 * C9-13
13 Cδ1δCpp
    13 δ/' * 14
14 C1Cpp
    1 * C14-15
15 Cpp

Now, using 15 repeatedly as follows we'll transform 2. through 5.:

    15 p/δC00 * 16
16 CδC00δC00
    2 δ/Cδ'δC00 * 17
17 CCδC00δC00Cδ1δC00
    17 * C16-18
18 Cδ1δC00
    15 p/δC01 * 19
19 CδC01δC01
    3 δ/Cδ'δC01 * 20
20 CδC01δC01Cδ1δC01
    20 * C19-21
21 Cδ1δC01
    15 p/δC10 * 22
22 CδC10δC10
    4 δ/Cδ'δC10 * 23
23 CCδC10δC10Cδ0δC10
    23 * C22-24
24 Cδ0δC10
    5 δ/Cδ'δC11 * 25
25 CCδC11δC11Cδ1δC11
    15 p/δC11
26 CδC11δC11
    25 * C26-27
27 Cδ1δC11

Now, we'll prove Cδ0CδC00δp.

    18 δ/Cδ0Cδ'δp * 28
28 CCδ0Cδ1δpCδ0CδC00δp
    28 * C6-29
29 Cδ0CδC00δp

Next up CpCqp.

    21 δ/' * 30
30 C1C01
    24 δ/' * 31
31 C0C10
    27 δ/' * 32
32 C1C11
    6 δ/C1C'1, p/q * 33
33 CC1C01CC1C11C1Cq1
    33 * C30-34
34 CC1C11C1Cq1
    34 * C32-35
35 C1Cq1
    30 * C1-36
36 C01
    18 δ/C0' * 37
37 CC01C0C00
    37 * C36-38
38 C0C00
    6 δ/C0C'0, p/q * 39
39 CC0C00CC0C10C0Cq0
    39 * C38-40
40 CC0C10C0Cq0
    40 * C31-41
41 C0Cq0
    6 δ/C'Cq' * 42
42 CC0Cq0CC1Cq1CpCqp
    42 * C41-43
43 CC1Cq1CpCqp
    43 * C35-44
44 CpCqp

To avoid re-numeraling, we'll prove CCδ00Cδ0δ0.

    44 p/Cqq, q/p * 45
45 CCqqCpCqq
    15 p/q * 46
46 Cqq
    45 * C46-47
47 CpCqq
    47 p/Cδ00, q/δ0 * 48
48 CCδ00Cδ0δ0

Now CCp0Cpq.

    18 δ/' * 49
49 C1C00
    18 δ/C'C00 * 50
50 CC1C00CC00C00
    50 * C49-51
51 CC00C00
    18 δ/C'C01 * 52
52 CC1C01CC00C01
    52 * C30-53
53 CC00C01
    6 δ/CC00C0', p/q * 54
54 CCC00C00CCC00C01CC00C0q
    54 * C51-55
55 CCC00C01CC00C0q
    55 * C53-56
56 CC00C0q
    15 p/C10 * 57
57 CC10C10
    47 p/0, q/1 * 58
58 C0C11
    24 δ/C'C11 * 59
59 CC0C11CC10C11
    59 * C58-60
60 CC10C11
    6 δ/CC10C1', p/q * 61
61 CCC10C10CCC10C11CC10C1q
    61 * C57-62
62 CCC10CC11C10C1q
    62 * C60-63
63 CC10C1q
    6 δ/CC'0C'q * 64
64 CCC00C0qCCC10C1qCCp0Cpq
    64 * C56-65
65 CCC10C1qCCp0Cpq
    65 * C63-66
66 CCp0Cpq

Now CδpδC1p

    6 δ/Cδ'δC1' * 67
67 CCδ0δC10CCδ1δC11CδpδC1p
    67 * C24-68
68 CCδ1δC11CδpδC1p
    68 * C27-69
69 CδpδC1p

Now CCC00δ0CC0δC00δ0. Let $\alpha$ stand for a functorial variable of one argument.

    44 p/δ0, q/C0δC00 * 70
70 Cδ0CC0δC00δ0
    69 p/α0 * 71
71 Cδα0δC1α0
    71 δ/C'CC0δC00δ0 * 72
72 CCα0CC0δC00δ0CC1α0CC0δC00δ0
    72 α/δ * 73
73 CCδ0CC0δC00δ0CC1δ0CC0δC00δ0
    73 * C70-74
74 CC1δ0CC0δC00δ0
    18 δ/CC'δ0CC0δC00δ0 * 75
75 CCC1δ0CC0δC00δ0CCC00δ0CC0δC00δ0
    75 * C74-76
76 CCC00δ0CC0δC00δ0

Now CCC10δ0CC1δC00δ1.

    47 p/CC10δ0, q/δ1 * 77
77 CCC10δ0Cδ1δ1
    18 δ/CCC10δ0Cδ'δ1 * 78
78 CCCC10δ0Cδ1δ1CCC10δ0CδC00δ1
    78 * C77-79
79 CCC10δ0CδC00δ1
    71 δ/CCC10δ0C'δ1 * 80
80 CCCC10δ0Cα0δ1CCC10δ0CC1α0δ1
    80 α/δC'0 * 81
81 CCCC10δ0CδC00δ1CCC10δ0CC1δC00δ1
    81 * C79-82
82 CCC10δ0CC1δC00δ1

Now CCCp0δ0CCpδC00δp

    6 δ/CCC'0δ0CC'δC00δ' * 83
83 CCCC00δ0CC0δC00δ0CCCC10δ0CC1δC00δ1CCCp0δ0CCpδC00δp
    83 * C76-84
84 CCCC10δ0CC1δC00δ1CCCp0δ0CCpδC00δp
    84 * C82-85
85 CCCp0δ0CCpδC00δp

Now Cδδ0δp.

    85 δ/Cδ'δq * 86
86 CCCp0Cδ0δqCCpCδC00δqCδpδq
    86 p/δ0 * 87
87 CCCδ00Cδ0δqCCδ0CδC00δqCδδ0δq
    66 p/δ0, q/δq * 88
88 CCδ00Cδ0δq
    87 * C88-89
89 CCδ0CδC00δqCδδ0δq
    89 q/p * 90
90 CCδ0CδC00δpCδδ0δp
    90 * C29-91
91 Cδδ0δp