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}: |
||
|