Here's my thirteen-step derivation of CCCpqCCrpCrqCss / {(p→q)→[(r→p)→(r→q)]}→(s→s) from the axioms B, C, and I*:
|
||
1. CCpqCCrpCrq B
(p→q)→[(r→p)→(r→q)] 2. CCpCqrCqCpr C [p→(q→r)]→[q→(p→r)] 3. CCppCqq I* (p→p)→(q→q) D1.1 = 4. CCpCqrCpCCsqCsr [p→(q→r)]→{p→[(s→q)→(s→r)]} D1.2 = 5. CCpCqCrsCpCrCqs {p→[q→(r→s)]}→{p→[r→(q→s)]} D2.1 = 6. CCpqCCqrCpr (p→q)→[(q→r)→(p→r)] D1.3 = 7. CCpCqqCpCrr [p→(q→q)]→[p→(r→r)] D5.5 = 8. CCpCqCrsCrCpCqs {p→[q→(r→s)]}→{r→[p→(q→s)]} D5.4 = 9. CCpCqrCCsqCpCsr [p→(q→r)]→{(s→q)→[p→(s→r)]} D5.7 = 10. CCpCqqCrCpr [p→(q→q)]→[r→(p→r)] D1.7 = 11. CCpCqCrrCpCqCss {p→[q→(r→r)]}→{p→[q→(s→s)]} D6.8 = 12. CCCpCqCrstCCqCrCpst [{p→[q→(r→s)]}→t]→[{q→[r→(p→s)]}→t] D9.9 = 13. CCpCqrCCsCrtCpCsCqt [p→(q→r)]→[[s→(r→t)]→{p→[s→(q→t)]}] D12.10 = 14. CCCpqCpCrqCsCrs {(p→q)→[p→(r→q)]}→[s→(r→s)] D11.13 = 15. CCCpCqrCqsCCpCsrCtt {[p→(q→r)]→(q→s)}→{[p→(s→r)]→(t→t)} D15.14 = 16. CCCpqCCrpCrqCss {(p→q)→[(r→p)→(r→q)]}→(s→s) |
||
|