Greetings, Carnap book chapter 4 (https://carnap.io/book/4) talks about Conditional Derivations. Was trying to come up with a way to do it in metamath but am stuck.
An example is: For the argument *P* → *Q*, *Q* → *R* ⊢ *P* → *R*, we can derive: 1. Show:P->R 2. P :AS 3. P->Q :PR 4. Q->R :PR 5. Q :MP 2,3 6. R :MP 4,5 7. :CD 6 It assumes (AS) P on step 2, introduces premises (PR), applies Modus Ponens (MP) and concludes the proof of P -> R with a conditional derivation. All seems very similar to metamath way of doing things except (?) from the :AS part. Is this translatable directly to metamath somehow? Best regards, JA -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/c710e4cd-093c-41af-ab90-542a4c125738n%40googlegroups.com.
