Formula of the day: CCCpqrCsCCqCrtCqt

The last two formulas of the day were CpCqp and CCpCqrCCpqCpr.  Together these form a set of axioms sufficient for the positive implicational calculus (equivalently they form a "basis" for the positive implicational calculus).  C. A. Meredith figured out that CCCpqrCsCCqCrtCqt itself serves as a basis for the positive implicational calculus of propositions.  To prove that{CpCqp-RVP, CCpCqrCCpqCpr-SD} yields CCCpqrCsCCqCrtCqt we can construct a demonstration as follows, with Ci standing for conditional introduction:

hypothesis  1 ! CCpqr
hypothesis  2 !@ s
hypothesis  3 !@# CqCrt
hypothesis  4 !@#$ q
RVP            5 !@#$ CqCpq
D5.4            6 !@#$ Cpq
D1.6            7 !@#$ r
D3.4            8 !@#$ Crt
D8.7            9 !@#$ t
Ci 4-9        10 !@# Cqt
Ci 3-10      11 !@  CCqCrtCqt
Ci 2-11      12 !     CsCCqCrtCqt
Ci 1-12      13  CCCpqrCsCCqCrtCqt.

We can expand all of this out and write a formal proof of {CCCpqrCsCCqCrtCqt} from the basis {CpCqp-RVP, CCpCqrCCpqCpr-SD} using any decent proof of the deduction metatheorem.  Here the letters a, b, ..., n, o can get substituted by something else, but p, q, ..., y, z cannot.  First we'll take out the "$" lines.

hypothesis   1 ! CCpqr
hypothesis   2 !@ s
hypothesis   3 !@# CqCrt
D[RVP].1    4 !@# CaCCpqr This is C4-1
D[SD].4      5 !@# CCaCpqCar
D5.RVP       6 !@# Cqr  ... C4-7
D[RVP].3    7 !@# CaCqCrt ... C4-3
D[SD].7      8 !@# CCaqCaCrt
D8.[Caa]     9 !@#  CqCrt ... C4-8
D[SD].9    10 !@# CCqrCqt
D10.6        11 !@# Cqt  C4-9
.
.
.

Now for the "#" lines in the above demonstration.  C3-3 and C3-9 match exactly.  C3-10 we can obtain simply from SD just by substitution.

hypothesis   1 ! CCpqr
hypothesis   2 !@ s
theorem       3 !@ CCaCbCcdCaCCbcCbd (we'll use this when we used "SD" above)
D[RVP].1    4 !@ CaCCpqr
D[RVP].4    5 !@ CaCbCCpqr ... C3-4
D3.5            6 !@ CaCCbCpqCbr ... C3-5
theorem       7 !@ CaCbCcb
D[SD].6      8 !@ CCaCbCpqCaCbr
D8.7            9 !@ CaCqr ... C3-6
D3.RVP    10 !@ CCabCCcaCcb  ... C3-8
D[SD].SD 11 !@ CCCaCbcCabCCaCbcCac
D11.9        12 !@ CCqCraCqa  C3-11

Now the "@" lines.

hypothesis    1 ! CCpqr
theorem        2 ! CCaCbCcdCaCCbcCbd
theorem        3 ! CCaCbCcCdeCaCbCCcdCce (we'll use this where we used 3 above)
D[RVP].1     4 ! CaCCpqr   C2-1
D[RVP].4     5 ! CaCbCCpqr  C2-4
D[RVP].5     6 ! CaCbCcCCpqr ... C2-5
D3.6             7 ! CaCbCCcCpqCcr ... C2-6
theorem        8 ! CaCbCcCdc ... C2-7
D2.7             9 ! CaCCbCcCpqCbCcr ... C2-8
D[SD].9     10 ! CCaCbCcCpqCaCbCcr
D10.8         11 ! CaCbCqr ... C2-9
theorem      12 ! CaCbCcb
D3.12         13 ! CaCCbcCCdbCdc  ... C2-10
D[SD].SD  14 ! CCCaCbcCabCCaCbcCac
D[RVP].14 15 ! CaCCCbCcdCbcCCbCcdCbd ... C2-11
D[SD].15   16 ! CCaCCbCcdCbcCaCCbCcdCbd
D16.11       17 ! CaCCqCrbCqr ... C2-12

And now we'll write the formal proof (allowing substitution for all lower case letters):

axiom     1 CpCqp   C1-4
axiom     2 CCpCqrCCpqCpr
D1.2       3 CpCCqCrsCCqrCqs
D2.3       4 CCpCqCrsCpCCqrCqs ... SD above
D1.4       5 CpCCqCrCstCqCCrsCrt
D2.5       6 CCpCqCrCstCpCqCCrsCrt   2 above
D1.6       7 CpCCqCrCsCtuCqCrCCstCsu
D2.7       8 CCpCqCrCsCtuCpCqCrCCstCsu ... 3 above
D1.1       9 CpCqCrq
D2.9     10 CCpqCpCrq
D10.1   11 CpCqCrp ... C1-5
D10.11 12 CpCqCrCsp ... C1-6
D1.9     13 CpCqCrCsr  ... C1-12
D1.13   14 CpCqCrCsCts ... C1-8
D8.12   15 CCpqCrCsCCtpCtq ... C1-7
D6.15   16 CCpqCrCCsCtpCsCtq ... C1-9
D4.16   17 CCpqCCrCsCtpCrCsCtq ... C1-10
D2.17   18 CCCpqCrCsCtpCCpqCrCsCtq
D18.14 19 CCCpqrCsCtCqr ... C1-11
D8.13   20 CpCqCCrsCCtrCts ... C1-13
D4.3     21 CpCCCqCrsCqrCCqCrsCqs ... C1-14
D1.21   22 CpCqCCCrCstCrsCCrCstCrt ... C1-15
D4.22   23 CpCCqCCrCstCrsCqCCrCstCrt ... C1-16
D2.23   24 CCpCqCCrCstCrsCpCqCCrCstCrt
D24.19 25 CCCpqrCsCCqCrtCqt

I'll point out that CCpqCCrpCrq is a theorem of this system as follows:

axiom   1 CpCqp
axiom   2 CCpCqrCCpqCpr
D1.2     3 CpCCqCrsCCqrCqs
D2.3     4 CCpCqCrsCpCCqrCqs
D4.1     5 CCpqCCrpCrq

But, even though it did appear in the set-ups to prove CCCpqrCsCCqCrtCqt, we never produced an actual proof of CCpqCCrpCrq, though we did produce a proof of  CpCqCCrsCCtrCts in which CCpqCrpCrq can get said to qualify as contained within.  I've used Prover9 to find a proof of {CpCqp, CCpCqrCCpqCpr} from {CCCpqrCsCCqCrtCqt}.  Meredith also found that CtCCpqCCCspCqrCpr can also serve as a basis of the positive implicational calculus.  Ted Ulrich has found some other single axioms for this system here.

Both axioms, "CtCCpqCCCspCqrCpr" and "CCCpqrCsCCqCrtCqt" have 17 symbols.  A stronger system, the implicational calculus of propositions, has a single axiom with just 13 symbols.

Also, the conversion procedure I used implicitly here depends on *how* a particular meta-proof of the deduction meta-theorem works.  If we have a different meta-proof of the deduction meta-theorem, we'll have a different conversion procedure.  My May 10th answer here shows the same process via a distinct meta-proof of the meta-deduction theorem.