Conditional Derivations (Carnap Book)

[jagra]

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

[Jim Kingdon]

This is discussed at some length at https://us.metamath.org/mpeuni/mmnatded.html and if you want something shorter, "put everything in deduction form" would be my one sentence summary.

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/c710e4cd-093c-41af-ab90-542a4c125738n%40googlegroups.com.