Here is a derivation of the three-base {Syl, Simp, Hilbert} for HI from {Frege', Simp}:

 
 



 

          1. CCpqCCqCqrCpr                                             [Frege']
           2. CpCqp                                                             [Simp]
 D1.1   =  3. CCCCpCpqCrqCCCpCpqCrqsCCrps
 D2.1   =  4. CpCCqrCCrCrsCqs
D1.2   =  5. CCCpqCCpqrCqr
 D2.2   =  6. CpCqCrq
D2.3   =  7. CpCCCCqCqrCsrCCCqCqrCsrtCCsqt
 D2.5   =  8. CpCCCqrCCqrsCrs
 D5.4   =  9. CpCCpCpqCrq
 D3.6   = 10. CCpqCrCCqCqsCps
 D5.7   = 11. CCCCpCpqCrqsCCrps
D5.8   = 12. CCCpqrCqr
 D1.9   = 13. CCCCpCpqCrqCCCpCpqCrqsCps
 D10.9  = 14. CpCCCCqCqrCsrCCCqCqrCsrtCqt
 D11.12 = 15. CCpqCCqrCpr                                             [Syl]
 D13.14 = 16. CCpCpqCpq                                                 [Hilbert]
 
 

 © Dolph Ulrich, 2007