Here is a derivation of the four-base {Syl, Simp, Hilbert, Dummett} for C-pure LC from the single axiom:

 
 



 
                    1. CCCpCqpCCCCCCrstCCCsrttCuCuvCwvxCCwux
D1.1     =  
 2. CCpqCrCsr
D2.1     =   3. CpCqp                                                                                            [Simp]
D1.2     =   4. CCpqCrCCCCCstuCCCtsuuCqCqvCpv
D1.4     =   5. CCpqCCCCCrstCCCsrttCCuvCCuvwCvw
D4.3     = 
 6. CpCCCCCqrsCCCrqssCCtuCCtuvCuv
D5.1     =   7. CCCCCpqrCCCqprrCCstCCstuCtu
D3.6     = 
 8. CpCqCCCCCrstCCCsrttCCuvCCuvwCvw
D7.4     =   9. CCCCCpqrrCCCCpqrrsCCCqprs
D7.8     = 10. CCCpqCCpqrCqr
D9.3     = 11. CCCpqrCCCqprr                                                                       [Dummett]
D3.10   = 12. CpCCCqrCCqrsCrs
D10.11 = 13. Cpp
D10.12 = 14. CCCpqrCqr
D4.13   = 15. CpCCCCCqrsCCCrqssCtCtuCtu
D3.14   = 16. CpCCCqrsCrs
D10.15 = 17. CCpCpqCpq                                                                                 [Hilbert]
D1.16    = 18. CCpqCCqCqrCpr
D18.18 = 19. CCCCpCpqCrqCCCpCpqCrqsCCrps
D19.16 = 20. CCpqCCqrCpr                                                                           [SYL]
 

There is an even shorter derivation of the three-base {Frege', Simp, Dummett}:
space
                    1. CCCpCqpCCCCCCrstCCCsrttCuCuvCwvxCCwux
D1.1     =   2. CCpqCrCsr
D2.1     =   3. CpCqp                                                                                                  [Simp]
D1.2     =   4. CCpqCrCCCCCstuCCCtsuuCqCqvCpv
D1.4     =   5. CCpqCCCCCrstCCCsrttCCuvCCuvwCvw
D4.3     =   6. CpCCCCCqrsCCCrqssCCtuCCtuvCuv
D5.1     =   7. CCCCCpqrCCCqprrCCstCCstuCtu
D3.6     =   8. CpCqCCCCCrstCCCsrttCCuvCCuvwCvw
D7.4     =   9. CCCCCpqrrCCCCpqrrsCCCqprs
D7.8     = 10. CCCpqCCpqrCqr
D9.3     = 11. CCCpqrCCCqprr                                                                           [Dummett]
D3.10   = 12. CpCCCqrCCqrsCrs
D10.12 = 13. CCCpqrCqr
D3.13   = 14. CpCCCqrsCrs
D1.14    = 15. CCpqCCqCqrCpr                                                                          [Frege']
 

 


Dolph Ulrich, 2007